aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | | * | | | | fix roadmap on "Simulation modulo liveness"Sylvain Boulmé2021-05-121-24/+61
| | * | | | | | some advanceLéo Gourdin2021-05-161-24/+191
| | * | | | | | iblock_istep rec and correct lemmasLéo Gourdin2021-05-131-0/+83
| | |/ / / / /
| | * | | | | ascii simuLéo Gourdin2021-05-121-17/+48
| | * | | | | finish proofLéo Gourdin2021-05-111-39/+45
| | * | | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-114-14/+325
| | |\ \ \ \ \
| | | * | | | | better autodestruct ?Sylvain Boulmé2021-05-112-17/+16
| | | * | | | | pointeur Justus -> roadmapSylvain Boulmé2021-05-111-1/+1
| | | * | | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-05-112-38/+77
| | | |\ \ \ \ \
| | | * | | | | | prove sexec_exactSylvain Boulmé2021-05-112-12/+324
| | * | | | | | | new lemma definition, some preparations in existing proofsLéo Gourdin2021-05-111-52/+65
| | | |/ / / / / | | |/| | | | |
| | * | | | | | new strong_state predicate and lemmaLéo Gourdin2021-05-102-38/+77
| | |/ / / / /
| | * | | | | Some more proof cases, comments and cleanupLéo Gourdin2021-05-102-97/+97
| | * | | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-101-4/+230
| | |\ \ \ \ \
| | | * | | | | précision du roadmapSylvain Boulmé2021-05-101-4/+230
| | * | | | | | is_exp and bcond proofLéo Gourdin2021-05-102-22/+36
| | |/ / / / /
| | * | | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-094-13/+372
| | |\ \ \ \ \
| | | * | | | | sexec: renommage Sdead -> Sabort + simplification de sexec_correctSylvain Boulmé2021-05-081-57/+21
| | | * | | | | idee pour simplifier la preuve: restreindre le "right_assoc" en "expand" !Sylvain Boulmé2021-05-083-5/+66
| | | * | | | | idea of a new scheme to define the semantics of LOAD NOTRAPSylvain Boulmé2021-05-071-0/+22
| | | * | | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-05-071-11/+82
| | | |\ \ \ \ \
| | | * | | | | | start a model of symbolic execution in Continuation-Passing-StyleSylvain Boulmé2021-05-071-18/+233
| | | * | | | | | fix SymbValPreserved sectionSylvain Boulmé2021-05-071-1/+98
| | * | | | | | | mib_exit draftLéo Gourdin2021-05-091-3/+4
| | * | | | | | | Some advance in proof and NOTRAP loads fixLéo Gourdin2021-05-072-10/+60
| | * | | | | | | intermediate lemma for opt_simu intro caseLéo Gourdin2021-05-071-10/+21
| | | |/ / / / / | | |/| | | | |
| | * | | | | | a draft for the Bnop caseLéo Gourdin2021-05-071-11/+25
| | * | | | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-072-1/+541
| | |\| | | | |
| | | * | | | | refactorisation + 1ere version de sstateSylvain Boulmé2021-05-061-1461/+169
| | | * | | | | init BTL_SEtheory (by copy/paste from RTLpathSE_theory)Sylvain Boulmé2021-05-062-1/+1833
| | * | | | | | proof OK for Call and Return statesLéo Gourdin2021-05-071-6/+21
| | * | | | | | starting RTL->BTL proofLéo Gourdin2021-05-061-4/+46
| | |/ / / / /
| | * | | | | fix match_statesSylvain Boulmé2021-05-061-6/+8
| | * | | | | cleaner match_statesSylvain Boulmé2021-05-061-16/+21
| | * | | | | start RTL -> BTLSylvain Boulmé2021-05-065-50/+383
| | * | | | | finish verify_block and proofLéo Gourdin2021-05-051-21/+123
| | * | | | | advance in cfg checkerLéo Gourdin2021-05-051-1/+138
| | * | | | | clean deprecated commentsSylvain Boulmé2021-05-051-6/+1
| | * | | | | Factorize as suggested for call/tailcallLéo Gourdin2021-05-041-43/+43
| | * | | | | finishing proofs and cleanupLéo Gourdin2021-05-041-134/+48
| | * | | | | some advance and simplificationsLéo Gourdin2021-05-041-67/+71
| | * | | | | suggestions...Sylvain Boulmé2021-05-041-20/+70
| | * | | | | builtin case OK, call and tailcall started but not finishedLéo Gourdin2021-05-041-1/+29
| | * | | | | one example case on main proofLéo Gourdin2021-05-041-18/+20
| | * | | | | Some try in step_simulationLéo Gourdin2021-05-041-3/+20
| | * | | | | proof for Icond in iblock_istepLéo Gourdin2021-05-041-1/+31
| | * | | | | essai avec le cond_star_stepSylvain Boulmé2021-05-041-12/+45
| | * | | | | essaisSylvain Boulmé2021-05-031-16/+31
| | * | | | | some advanceLéo Gourdin2021-05-031-8/+39
| | * | | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-05-031-35/+22
| | |\ \ \ \ \
generated by cgit (git 2.34.1) at 2024-07-07 02:38:53 +0000