aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Removing addptrofs draft, next will be mergingLéo Gourdin2021-04-091-2/+0
* Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-061-1/+2
* a more general way to manage special registers before introducing SPLéo Gourdin2021-03-301-28/+28
* Now a more general way to perform imm operationsLéo Gourdin2021-03-301-0/+1
* Asmcondexp branche useful to benchmark expansionsLéo Gourdin2021-03-021-18/+146
* Merge conflicts solved and cleaning in Asmgenproof after expansionLéo Gourdin2021-03-021-146/+18
* [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proofLéo Gourdin2021-02-111-0/+8
* [Admitted checker] Checker expansion for reg Ocmp (without scratch)Léo Gourdin2021-02-101-7/+7
* cond and branches expandedLéo Gourdin2021-02-061-8/+20
* All Ocmp expanded in RTLLéo Gourdin2021-02-031-3/+3
* Ccomp for longLéo Gourdin2021-02-031-3/+7
* Ccompu expansionLéo Gourdin2021-02-021-0/+1
* Expansion of Ccompimm in RTL [Admitted checker]Léo Gourdin2021-02-021-0/+3
* 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
generated by cgit (git 2.34.1) at 2024-06-02 22:01:46 +0000