aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* Adding stub RTLpathLivegenaux.mlCyril SIX2020-05-252-0/+6
* RTL -> RTLpath -> RTLCyril SIX2020-05-201-1/+70
* Revert "Modifying RTLpath in order to allow for stopping at Icond"Cyril SIX2020-05-201-23/+11
* Modifying RTLpath in order to allow for stopping at IcondCyril SIX2020-05-201-11/+23
* No need to change default_succ : we keep ifnot as default, and adjust the pat...Cyril SIX2020-05-201-2/+0
* Admitting the restCyril SIX2020-05-202-7/+7
* StailcallCyril SIX2020-05-201-5/+21
* Proof of sisteps_correct_falseCyril SIX2020-05-191-8/+31
* sistep_correct proved completelyCyril SIX2020-05-191-21/+16
* Avancement on sistep_correct for loadCyril SIX2020-05-191-4/+22
* Progress on load_notrap_value in symbolic executionCyril SIX2020-04-301-12/+27
* Progression on LOAD sistep_correctCyril SIX2020-04-301-3/+30
* Back to a proven sistep_correct (except for the LOAD case)Cyril SIX2020-04-301-19/+26
* Proof of sistep_preserves_sabortCyril SIX2020-04-291-19/+63
* Complete proof of ssem_exclude_sabortCyril SIX2020-04-291-5/+8
* ssem_exit_fallthrough_upto_exit finally done - it was very simple actuallyCyril SIX2020-04-291-64/+7
* The lemmas i was basing my theorems on are actually wrong..Cyril SIX2020-04-291-48/+39
* Proving admitted ssem_exit_fallthrough_upto_exit -> need to prove is_tail_existsCyril SIX2020-04-281-30/+38
* Proof of ssem_exit_exclude_sabort - on avance !Cyril SIX2020-04-281-41/+11
* Cutting ssem_exits into two pieces + advancing some proofsCyril SIX2020-04-271-130/+248
* no: the simpler fix is too simple...Sylvain Boulmé2020-04-251-22/+14
* a simpler fix ?Sylvain Boulmé2020-04-251-2/+18
* fixing sabort_exits ?Sylvain Boulmé2020-04-241-1/+16
* Reverting change to sistateCyril SIX2020-04-241-39/+7
* [BROKEN] Added wf predicate sistate - simatch_exclude_abort proven, need to m...Cyril SIX2020-04-231-77/+121
* Finished renamingCyril SIX2020-04-232-337/+339
* Started general renaming for clearer and more understandable codeCyril SIX2020-04-223-250/+243
* list_val_inj --> list_sval_injCyril SIX2020-04-221-8/+8
* Trying to cut sem_istate_exclude_abort into lemmasCyril SIX2020-04-221-8/+68
* Added and cleaned some comments on RTLpath.vCyril SIX2020-04-211-1/+8
* notrap casesDavid Monniaux2020-04-151-3/+5
* Some progress on notrap loadCyril SIX2020-04-153-23/+61
* Fixing the merge. Needs to add notrap load semantics + prove other admitted s...Cyril SIX2020-04-103-61/+71
* [BROKEN] Merge branch 'mppa-work' into mppa-RTLpathSECyril SIX2020-04-1031-770/+1526
|\
| * 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
generated by cgit (git 2.34.1) at 2024-06-11 19:07:02 +0000