aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
...
* | Calcul de dominateurs a l'air de marcherCyril SIX2019-12-101-88/+144
* | Merge remote-tracking branch 'refs/remotes/origin/mppa-duplicate-oracle' into...Cyril SIX2019-12-094-130/+11
|\ \
| * | Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-dupl...David Monniaux2019-12-094-130/+11
| |\|
| | * Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-12-0949-157/+1158
| | |\
| | * | 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
| | |\ \ \ \ | | | | |/ / | | | |/| |
| | * | | | 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
| | |\ \ \ \ \ | | | |_|_|/ / | | |/| | | |
* | / | | | | Rajout du calcul de dominateurs - pas testéCyril SIX2019-12-091-16/+43
|/ / / / / /
* | | | | | merge w/ non trapping loadsDavid Monniaux2019-12-061-3/+3
* | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-duplicate-oracleDavid Monniaux2019-12-0658-423/+1502
|\ \ \ \ \ \ | | |_|_|_|/ | |/| | | |
| * | | | | make it compile for ARMDavid Monniaux2019-12-061-4/+4
| * | | | | finish mergeDavid Monniaux2019-12-023-14/+32
| * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-024-1/+709
| |\ \ \ \ \
| | * | | | | Duplicateproof: minor editSylvain Boulmé2019-11-261-3/+4
| | | |_|_|/ | | |/| | |
| | * | | | simplification of Duplicate: remove xfunctionSylvain Boulmé2019-11-142-187/+154
| | | |/ / | | |/| |
| | * | | 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
| | |\ \ \ \ | | | |/ / / | | |/| | / | | | | |/ | | | |/|
| * | | | 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
generated by cgit (git 2.34.1) at 2024-07-12 08:42:34 +0000