aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/SelectOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* fix riscv merge?Léo Gourdin2021-03-291-0/+1093
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-1093/+0
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-17/+17
* | detect redundant cmovDavid Monniaux2021-02-021-0/+22
* | Cmov TsingleDavid Monniaux2021-02-021-33/+26
* | PselectdDavid Monniaux2021-02-021-0/+19
* | cmov on integersDavid Monniaux2021-02-021-9/+80
* | begin synthesizing selectDavid Monniaux2021-02-021-1/+11
* | adding builtinsDavid Monniaux2021-02-011-1/+4
* | risc-V now without trapping instructionsDavid Monniaux2020-09-211-0/+8
* | maketotal mod & divDavid Monniaux2020-09-211-32/+30
* | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...David Monniaux2019-09-201-2/+2
|\|
| * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
* | helpers broke compilationDavid Monniaux2019-07-191-4/+1
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-191-12/+19
|\|
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-12/+16
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-031-2/+17
|\|
| * 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
* | Risc-V works again (32/64).David Monniaux2019-03-221-2/+27
|/
* 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
generated by cgit (git 2.34.1) at 2024-05-09 03:50:57 +0000