aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2020-04-2056-6790/+8851
|\
| * 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 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
| |\ \
generated by cgit (git 2.34.1) at 2024-06-03 02:58:36 +0000