aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* swap load and store at disjoint offsetsDavid Monniaux2019-12-161-1/+53
* swap stores at disjoint offsetsDavid Monniaux2019-12-161-16/+30
* comment out theorem that cannot be provedDavid Monniaux2019-12-141-29/+33
* progress in chunksDavid Monniaux2019-12-131-45/+9
* some subgoal was provedDavid Monniaux2019-12-121-6/+61
* begin overlap proofsDavid Monniaux2019-12-111-0/+43
* Converting Asm.v and Asmblockgenproof.v back to Unix formatCyril SIX2019-12-032-2426/+2426
* finish mergeDavid Monniaux2019-12-022-11/+20
* Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-027-185/+148
|\
| * fixing a potential inconsistency from unsafe_coerceSylvain Boulmé2019-11-142-7/+13
| * removing Focus (deprecated)Sylvain Boulmé2019-11-141-2/+2
| * Un espace en tropCyril SIX2019-10-211-1/+1
| * eq_condition already existedDavid Monniaux2019-10-161-6/+0
| * [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-16/+2
| * Few minor other changes in proofCyril SIX2019-10-151-3/+3
| * More elaborate comments + rewriting for easier to understand Asmblockgenproof.vCyril SIX2019-10-151-145/+89
| * Converting mppa_k1c/*.v files to Unix formatCyril SIX2019-10-112-754/+754
| * Fixing fp_is_parent too weak (#165)Cyril SIX2019-10-112-1798/+1811
| * Merge branch 'mppa-duplicate-rtl' into mppa-workCyril SIX2019-10-081-0/+6
| |\
| | * IcondCyril SIX2019-10-071-0/+6
| * | Asmblockgenproof : cur rewritingCyril SIX2019-10-011-11/+11
| * | Tiny cleanCyril SIX2019-10-011-1/+0
| * | Asmblockgenproof renaming fpok --> epCyril SIX2019-10-011-11/+11
| |/
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-241-2/+2
|\|
| * (#161) - Fixing vararg bugCyril SIX2019-09-241-2/+2
* | is_trapping_op_soundDavid Monniaux2019-09-231-0/+28
* | Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc...David Monniaux2019-09-204-18/+5
|\ \
| * | fix compilingDavid Monniaux2019-09-202-3/+3
| * | extraction problemsDavid Monniaux2019-09-201-1/+2
| * | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...David Monniaux2019-09-203-18/+4
| |/
* | fix Focus -> { ... }David Monniaux2019-09-201-2/+2
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-206-46/+48
|\|
| * __builtin_bswap16, 32 and 64Cyril SIX2019-09-202-36/+35
| * Detailing oracle/vérificateur in the timingsCyril SIX2019-09-182-2/+3
| * Timings for Machblockgen, Asmblockgen and postpass schedulingCyril SIX2019-09-182-6/+8
| * Compatibility fix for Coq 8.7.1Cyril SIX2019-09-131-3/+3
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-102-17/+0
|\|
| * Removing unused .all, .any, .nall and .none conditionsCyril SIX2019-09-052-17/+0
* | asmblockgen worksDavid Monniaux2019-09-082-5/+48
* | more proofs on notrap2David Monniaux2019-09-081-9/+53
* | more proofs on notrapDavid Monniaux2019-09-081-6/+124
* | notrap in mppa_k1c ML codeDavid Monniaux2019-09-083-31/+35
* | a couple "Admitted" and the Coq compilesDavid Monniaux2019-09-081-12/+18
* | moving forward with notrapDavid Monniaux2019-09-081-22/+10
* | furtherDavid Monniaux2019-09-081-3/+20
* | moving forward on K1CDavid Monniaux2019-09-078-171/+200
* | more stuff on non trapping loadsDavid Monniaux2019-09-051-0/+8
* | more proofsDavid Monniaux2019-09-051-0/+13
* | more on notrapDavid Monniaux2019-09-055-19/+57
* | forgot this functionDavid Monniaux2019-09-031-2/+0
generated by cgit (git 2.34.1) at 2024-06-03 00:21:17 +0000