Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | missing file | David Monniaux | 2019-09-09 | 1 | -0/+26 |
* | proof for Allnontrap | David Monniaux | 2019-09-09 | 1 | -0/+215 |
* | finished the proofs for non-trapping loads | David Monniaux | 2019-09-08 | 1 | -10/+21 |
* | fixes for compiling on other platforms | David Monniaux | 2019-09-07 | 4 | -8/+8 |
* | fixes for ARM | David Monniaux | 2019-09-07 | 4 | -21/+12 |
* | notrap works on x86 | David Monniaux | 2019-09-07 | 1 | -12/+3 |
* | more for passing notrap through x86 | David Monniaux | 2019-09-07 | 1 | -2/+10 |
* | ONE "admitted" and things compile | David Monniaux | 2019-09-06 | 11 | -46/+83 |
* | progress in proof | David Monniaux | 2019-09-05 | 1 | -14/+27 |
* | BSload notrap1 | David Monniaux | 2019-09-05 | 1 | -1/+19 |
* | moving forward with proofs | David Monniaux | 2019-09-05 | 2 | -29/+29 |
* | more proofs | David Monniaux | 2019-09-05 | 1 | -0/+39 |
* | more on notrap | David Monniaux | 2019-09-05 | 2 | -5/+18 |
* | more proof | David Monniaux | 2019-09-05 | 1 | -0/+16 |
* | some more proofs on notrap | David Monniaux | 2019-09-05 | 1 | -0/+12 |
* | more proofs going through | David Monniaux | 2019-09-05 | 9 | -26/+95 |
* | LinearizeProof for non trapping loads | David Monniaux | 2019-09-05 | 1 | -16/+32 |
* | CSEproof for non trapping loads | David Monniaux | 2019-09-05 | 3 | -19/+89 |
* | going forward | David Monniaux | 2019-09-04 | 1 | -41/+50 |
* | stuck in CSEproof | David Monniaux | 2019-09-04 | 1 | -1/+10 |
* | ca avance | David Monniaux | 2019-09-04 | 1 | -2/+11 |
* | begin CSE proof for notrap load | David Monniaux | 2019-09-04 | 1 | -3/+85 |
* | begin CSE | David Monniaux | 2019-09-04 | 4 | -18/+23 |
* | moved trapping_mode to a more appropriate place | David Monniaux | 2019-09-03 | 1 | -2/+0 |
* | Dead code proof for non trapping loads | David Monniaux | 2019-09-03 | 1 | -0/+77 |
* | finished Constopproof for non trapping loads | David Monniaux | 2019-09-03 | 1 | -1/+41 |
* | advancing in constant propagation | David Monniaux | 2019-09-03 | 2 | -2/+22 |
* | Value analysis for non trapping loads | David Monniaux | 2019-09-03 | 2 | -4/+38 |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-09-03 | 19 | -134/+439 |
|\ | |||||
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2019-08-28 | 1 | -2/+0 |
| |\ | |||||
| | * | Coq 8.10 compatibility: make explicit the "core" hint database | Xavier Leroy | 2019-08-05 | 1 | -2/+0 |
| * | | various fixes | David Monniaux | 2019-07-19 | 3 | -24/+4 |
| * | | helpers broke compilation | David Monniaux | 2019-07-19 | 2 | -11/+0 |
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2019-07-19 | 17 | -128/+466 |
| |\| | |||||
| | * | Improve CSE for known built-in functions | Xavier Leroy | 2019-07-17 | 2 | -7/+14 |
| | * | Perform constant propagation for known built-in functions | Xavier Leroy | 2019-07-17 | 4 | -16/+168 |
| | * | Give formal semantics to some built-in functions and run-time functions | Xavier Leroy | 2019-07-17 | 3 | -112/+231 |
| | * | Compatibility with OCaml 4.08 (#302) | Xavier Leroy | 2019-07-08 | 6 | -7/+6 |
| | * | Rename option `-ffavor-branchless` into `-Obranchless` | Xavier Leroy | 2019-07-05 | 1 | -3/+3 |
| | * | Extended asm: print register names according to their types | Xavier Leroy | 2019-06-17 | 1 | -9/+14 |
* | | | progress on non trapping loads | David Monniaux | 2019-09-03 | 1 | -0/+54 |
* | | | progress on non trapping loads | David Monniaux | 2019-09-02 | 1 | -8/+32 |
* | | | avancement (il faut utiliser Vundef visiblement) | David Monniaux | 2019-09-02 | 18 | -41/+114 |
|/ / | |||||
* | | finish merging master branch (fixes problems in glpk colamd) | David Monniaux | 2019-06-06 | 3 | -43/+0 |
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work | David Monniaux | 2019-06-06 | 3 | -5/+59 |
|\| | |||||
| * | Cminortyping: relax typechecking of function calls | Xavier Leroy | 2019-06-06 | 1 | -12/+15 |
| * | If-conversion optimization | Xavier Leroy | 2019-06-06 | 4 | -72/+584 |
| * | Type inference and type checking for Cminor | Xavier Leroy | 2019-06-06 | 1 | -0/+797 |
* | | start to have whole path if-conversion? | David Monniaux | 2019-06-04 | 1 | -1/+1 |
* | | rm old select/selectl/selectf/selectfs | David Monniaux | 2019-06-03 | 2 | -64/+3 |