aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc...David Monniaux2019-09-2010-54/+148
|\
| * Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...David Monniaux2019-09-2010-54/+148
| |\
| | * Reworked json export.Bernhard Schommer2019-09-123-29/+37
| | * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
| | * AArch64 portXavier Leroy2019-08-087-37/+97
| | * Asmgenproof0: add predicate exec_straight0Xavier Leroy2019-08-071-0/+26
| | * Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+0
* | | missing fileDavid Monniaux2019-09-091-0/+26
* | | proof for AllnontrapDavid Monniaux2019-09-091-0/+215
* | | finished the proofs for non-trapping loadsDavid Monniaux2019-09-081-10/+21
* | | fixes for compiling on other platformsDavid Monniaux2019-09-074-8/+8
* | | fixes for ARMDavid Monniaux2019-09-074-21/+12
* | | notrap works on x86David Monniaux2019-09-071-12/+3
* | | more for passing notrap through x86David Monniaux2019-09-071-2/+10
* | | ONE "admitted" and things compileDavid Monniaux2019-09-0611-46/+83
* | | progress in proofDavid Monniaux2019-09-051-14/+27
* | | BSload notrap1David Monniaux2019-09-051-1/+19
* | | moving forward with proofsDavid Monniaux2019-09-052-29/+29
* | | more proofsDavid Monniaux2019-09-051-0/+39
* | | more on notrapDavid Monniaux2019-09-052-5/+18
* | | more proofDavid Monniaux2019-09-051-0/+16
* | | some more proofs on notrapDavid Monniaux2019-09-051-0/+12
* | | more proofs going throughDavid Monniaux2019-09-059-26/+95
* | | LinearizeProof for non trapping loadsDavid Monniaux2019-09-051-16/+32
* | | CSEproof for non trapping loadsDavid Monniaux2019-09-053-19/+89
* | | going forwardDavid Monniaux2019-09-041-41/+50
* | | stuck in CSEproofDavid Monniaux2019-09-041-1/+10
* | | ca avanceDavid Monniaux2019-09-041-2/+11
* | | begin CSE proof for notrap loadDavid Monniaux2019-09-041-3/+85
* | | begin CSEDavid Monniaux2019-09-044-18/+23
* | | moved trapping_mode to a more appropriate placeDavid Monniaux2019-09-031-2/+0
* | | Dead code proof for non trapping loadsDavid Monniaux2019-09-031-0/+77
* | | finished Constopproof for non trapping loadsDavid Monniaux2019-09-031-1/+41
* | | advancing in constant propagationDavid Monniaux2019-09-032-2/+22
* | | Value analysis for non trapping loadsDavid Monniaux2019-09-032-4/+38
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-0319-134/+439
|\| |
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-08-281-2/+0
| |\ \
| | * | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-051-2/+0
| | |/
| * | various fixesDavid Monniaux2019-07-193-24/+4
| * | helpers broke compilationDavid Monniaux2019-07-192-11/+0
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-1917-128/+466
| |\|
| | * Improve CSE for known built-in functionsXavier Leroy2019-07-172-7/+14
| | * Perform constant propagation for known built-in functionsXavier Leroy2019-07-174-16/+168
| | * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-112/+231
| | * Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-086-7/+6
| | * Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-051-3/+3
| | * Extended asm: print register names according to their typesXavier Leroy2019-06-171-9/+14
* | | progress on non trapping loadsDavid Monniaux2019-09-031-0/+54
* | | progress on non trapping loadsDavid Monniaux2019-09-021-8/+32
* | | avancement (il faut utiliser Vundef visiblement)David Monniaux2019-09-0218-41/+114
|/ /
generated by cgit (git 2.34.1) at 2024-07-12 03:56:15 +0000