aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTLtoRTLproof.v
Commit message (Expand)AuthorAgeFilesLines
* being more archi-independantLéo Gourdin2021-11-021-3/+3
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-6/+14
* CI fix on armLéo Gourdin2021-08-021-2/+2
* ci fix?Léo Gourdin2021-07-281-0/+2
* non trapping loadsLéo Gourdin2021-07-231-1/+2
* Fix compile on ARM/x86 backendsLéo Gourdin2021-07-201-4/+4
* starting to extend RTLtoBTL with Liveness checking (on BTL side)Sylvain Boulmé2021-05-281-0/+12
* splitting BTL by introducing BTLmatchRTLSylvain Boulmé2021-05-281-37/+5
* Merge branch 'BTL_fsem' into BTLLéo Gourdin2021-05-281-5/+13
|\
| * most of the proof BTL.fsem -> BTL.cfgsem.Sylvain Boulmé2021-05-281-2/+10
| * defines fsem (aka functional semantics) of BTLSylvain Boulmé2021-05-201-3/+3
* | [disabled checker] BTL Scheduling and Renumbering OK!Léo Gourdin2021-05-271-2/+2
* | Now supporting Bnop insertion in conditionsLéo Gourdin2021-05-211-9/+20
* | Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-201-8/+8
* | Adding a BTL record to help oraclesLéo Gourdin2021-05-191-3/+3
|/
* start RTL -> BTLSylvain Boulmé2021-05-061-0/+50
* 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
* debroussaillage et precisions...Sylvain Boulmé2021-05-011-8/+58
* BTLtoRTL: proof for internal/external/return statesLéo Gourdin2021-04-301-0/+25
* start the new "BTL" IR.Sylvain Boulmé2021-04-281-0/+127
generated by cgit (git 2.34.1) at 2024-05-08 05:34:33 +0000