aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* 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 gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-032-17/+26
* 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
| * 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
|\|
generated by cgit (git 2.34.1) at 2024-06-02 21:28:50 +0000