aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* merge merge mergeDavid Monniaux2019-11-141-1/+1
* Merge branch 'mppa-work-upstream-merge' of gricad-gitlab.univ-grenoble-alpes....David Monniaux2019-11-141-3/+1
|\
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-11-144-0/+710
| |\
* | \ Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-11-142-187/+154
|\ \ \ | | |/ | |/|
| * | simplification of Duplicate: remove xfunctionSylvain Boulmé2019-11-142-187/+154
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-11-135-126/+11
|\ \ \
| * | | Remove no longer needed file PrintLTLinBernhard Schommer2019-11-121-115/+0
| * | | Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-022-8/+8
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-11-134-1/+740
|\ \ \ \ | | |/ / | |/| / | |_|/ |/| |
| * | Merge remote-tracking branch 'origin/mppa-duplicate-rtl-alt' into mppa-workCyril SIX2019-10-242-60/+77
| |\ \
| | * | An alternative proof where the match_state does not depend on the translationSylvain Boulmé2019-10-232-60/+77
| * | | eq_condition already existedDavid Monniaux2019-10-162-2/+2
| * | | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-1610-51/+146
| |\ \ \ | | |/ / | |/| / | | |/
| * | 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 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
* | 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
|\|
generated by cgit (git 2.34.1) at 2024-07-12 04:04:19 +0000