aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/SelectOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* 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-06-02 17:10:52 +0000