aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into kvx-workCyril SIX2021-06-011-2/+4
|\
| * Register X1 is destroyed by some built-in functionsXavier Leroy2021-05-131-2/+4
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-18/+146
|\ \
| * | Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-191-3/+159
| * | Removing expansions from AsmgenLéo Gourdin2021-04-091-159/+3
| * | 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 branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-6/+6
|\ \ \ | |/ / |/| / | |/
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-6/+6
* | 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-05-09 13:29:20 +0000