aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Expand "j_s symb" to "jump symb, x31" assembly pseudo-instructionXavier Leroy2022-06-241-0/+1
* Register X1 is destroyed by some built-in functionsXavier Leroy2021-05-131-2/+4
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-6/+6
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-011-2/+2
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+1028