aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
* Fix cutrewrite deprecatedCyril SIX2020-04-011-3/+4
|
* proof clarificationDavid Monniaux2020-03-201-3/+5
|
* more understandabe proofsDavid Monniaux2020-03-201-38/+38
|
* progress in RA invariantsDavid Monniaux2020-03-201-23/+24
|
* Duplicate: getting rid of the annoying exception-based codeCyril SIX2020-03-091-7/+2
|
* removing more coq8.10 warningsSylvain Boulmé2020-03-094-2/+10
|
* removing some coqc 8.10 warningsSylvain Boulmé2020-03-091-4/+4
|
* removing warnings on hints in coreSylvain Boulmé2020-03-0711-42/+39
|
* forgot k1CDavid Monniaux2020-03-032-0/+147
|
* Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-032-17/+26
| | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
* Moving some arch specific theorems from PSproof to AsmblockpropsCyril SIX2020-02-112-219/+218
|
* Moving Asmblockgenproof0 to mppa_k1c/lib/Cyril SIX2020-02-101-0/+0
|
* Removing from Asmblockgenproof0 architecture specific definitionsCyril SIX2020-02-108-129/+152
|
* Moved some theoremsCyril SIX2020-02-104-113/+101
|
* Fixing maddw and maddd resource tablesCyril SIX2020-02-061-2/+19
|
* Using Ocaml type instead of string to identify resourcesCyril SIX2020-02-061-35/+36
|
* Fixed reservation tablesCyril SIX2020-02-061-44/+46
|
* Breaking the prologue to satisfy resource constraintsCyril SIX2020-02-061-1/+1
|
* 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
| | |
generated by cgit (git 2.34.1) at 2024-07-12 04:40:33 +0000