aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-2/+2
|\
| * 64-bit signed division by two codeDavid Monniaux2020-01-141-1/+1
| * rv32: 3-instruction signed divide-by-two sequence (as opposed to 4)David Monniaux2020-01-141-1/+1
* | fix for Risc-VDavid Monniaux2019-09-071-1/+7
|/
* 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