aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
|\
| * 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
| |\
| * | proof OK for Call and Return statesLéo Gourdin2021-05-071-6/+21
| * | starting RTL->BTL proofLéo Gourdin2021-05-061-4/+46
* | | 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
| |/ |/|
* | 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
|/
* 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
|\
| * A better structure for inductive propLéo Gourdin2021-05-031-35/+25
* | une autre suggestionSylvain Boulmé2021-05-031-0/+14
|/
* Trying a inductive predicate for BTL-RTL proofLéo Gourdin2021-05-031-10/+41
* more implem notes in BTLroadmapSylvain Boulmé2021-05-021-1/+8
* BTL roadmapSylvain Boulmé2021-05-021-0/+79
* debroussaillage et precisions...Sylvain Boulmé2021-05-012-23/+73
* BTLtoRTL: proof for internal/external/return statesLéo Gourdin2021-04-302-2/+27
* start the new "BTL" IR.Sylvain Boulmé2021-04-286-2/+735
* add auxfileDavid Monniaux2021-04-271-0/+17
* Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...Léo Gourdin2021-04-2218-566/+370
|\
| * fix broken link in index-kvx.htmlSylvain Boulmé2021-04-161-1/+1
| * Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVXCyril SIX2021-04-135-525/+173
| |\
| | * CleaningCyril SIX2021-04-021-2/+1
| | * More efficientCyril SIX2021-04-021-8/+12
| | * Outermost loop detection worksCyril SIX2021-04-021-9/+10
| | * Getting all loop bodiesCyril SIX2021-04-022-2/+50
| | * get_loop_headers simplification (using the new get_loop_backedges)Cyril SIX2021-04-021-39/+7
| | * Simple backedge detection (modified code from get_loop_headers)Cyril SIX2021-04-023-0/+57
| | * Big simplification of get_loop_infoCyril SIX2021-03-311-111/+16
| | * Simplification of the Linearize heuristic (same result functionally)Cyril SIX2021-03-301-216/+6
| | * Simplifications on Linearize - details belowCyril SIX2021-03-291-205/+79
| | * Code simplification of get_path_map (no functionality change)Cyril SIX2021-01-261-14/+16
generated by cgit (git 2.34.1) at 2024-07-14 14:51:04 +0000