aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/SelectOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-17/+17
* Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-12/+16
* Provide a default "select" operation for the RiscV portXavier Leroy2019-05-201-0/+14
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-2/+3
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-061-6/+16
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+915