aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* An alternative proof where the match_state does not depend on the translationSylvain Boulmé2019-10-232-60/+77
* 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
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-0321-150/+1552
|\ \
| * | ARM: select is not supported at type TlongXavier Leroy2019-06-011-2/+3
| * | If-conversion optimizationXavier Leroy2019-05-314-72/+579
| * | Type inference and type checking for CminorXavier Leroy2019-05-311-0/+798
| |/
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-314-5/+5
generated by cgit (git 2.34.1) at 2024-07-12 05:05:08 +0000