aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-1610-51/+146
|\
| * 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
* | Finished Duplicate proof.Cyril SIX2019-10-072-36/+58
* | IcondCyril SIX2019-10-072-0/+26
* | Fixing identity PTree in Duplicateaux oracleCyril SIX2019-10-071-2/+8
* | ItailcallCyril SIX2019-10-072-2/+17
* | IreturnCyril SIX2019-10-072-1/+9
* | Ibuiltin proofCyril SIX2019-10-042-0/+31
* | IcallCyril SIX2019-10-032-0/+27
* | Iload and IstoreCyril SIX2019-10-032-3/+43
* | Proof for IopCyril SIX2019-10-032-1/+20
* | Preparing the terrain for the rest of the instructions with one successorCyril SIX2019-10-031-5/+17
* | Duplicate - Proof of verificator for InopCyril SIX2019-10-032-4/+83
* | Starting implementing the verificatorCyril SIX2019-10-022-1/+34
* | Identity oracle realizing verify_mapping_entrypointCyril SIX2019-10-021-1/+4
* | Proof of first axiomCyril SIX2019-09-112-4/+25
* | Fixing Linking problemCyril SIX2019-09-112-31/+31
* | Utilisation d'un intermédiaire xfunction contenant le revmapCyril SIX2019-09-112-47/+81
* | Duplicate: proof complete, assuming revmap, revmap_correct and revmap_entrypointCyril SIX2019-09-061-5/+21
* | Duplicate: big progress on step_simulation, only Ijumptbl leftCyril SIX2019-09-053-85/+148
* | Duplicate: changement de match_nodesCyril SIX2019-09-041-36/+44
* | Duplicate: exec_function_external et exec_returnCyril SIX2019-09-041-3/+7
* | Duplicate: exec_function_internalCyril SIX2019-09-042-2/+43
* | transf_initial_statesCyril SIX2019-09-043-12/+84
* | Duplicate: match_statesCyril SIX2019-09-031-2/+10
* | Duplicate: match_nodesCyril SIX2019-09-031-8/+57
* | Start of match_statesCyril SIX2019-09-031-3/+23
* | Stubs for Duplicate passCyril SIX2019-09-033-0/+63
* | 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
* | finish merging master branch (fixes problems in glpk colamd)David Monniaux2019-06-063-43/+0
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-06-063-5/+59
|\|
| * Cminortyping: relax typechecking of function callsXavier Leroy2019-06-061-12/+15
| * If-conversion optimizationXavier Leroy2019-06-064-72/+584
| * Type inference and type checking for CminorXavier Leroy2019-06-061-0/+797
* | start to have whole path if-conversion?David Monniaux2019-06-041-1/+1
* | rm old select/selectl/selectf/selectfsDavid Monniaux2019-06-032-64/+3
generated by cgit (git 2.34.1) at 2024-06-13 10:57:09 +0000