aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'mppa-work' into mppa-duplicate-oracleCyril SIX2020-01-221-0/+132
|\
| * Fixing issue with "destruct ... in ..." tactics with Coq 8.8Cyril SIX2020-01-091-5/+5
| |
| * 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
| |
* | Opcode heuristic done for K1cCyril SIX2019-12-161-2/+30
| |
* | Stub for opcode heuristicCyril SIX2019-12-161-0/+4
|/
* 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
| | | | | | | | | | Now, unsafe_coerce axioms are clearly consistent (for any interpretation of may-return monads). But, the extraction is still unsafe...
| * 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| * 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 ↵David Monniaux2019-09-204-18/+5
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
| * | 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 ↵David Monniaux2019-09-203-18/+4
| |/ | | | | | | mppa-work-upstream-merge
* | 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
| |
generated by cgit (git 2.34.1) at 2024-07-11 22:44:13 +0000