aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTL.v
Commit message (Expand)AuthorAgeFilesLines
* fix Builtin semanticsSylvain Boulmé2021-05-251-10/+24
* starting to experiment SE of fsemSylvain Boulmé2021-05-251-17/+74
* improve fsemSylvain Boulmé2021-05-211-15/+30
* defines fsem (aka functional semantics) of BTLSylvain Boulmé2021-05-201-7/+74
* finishing RTLtoBTLLéo Gourdin2021-05-171-18/+0
* Lemmas on ISTEPLéo Gourdin2021-05-171-0/+1
* Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-05-111-0/+5
|\
| * new strong_state predicate and lemmaLéo Gourdin2021-05-101-0/+5
* | prove sexec_exactSylvain Boulmé2021-05-111-1/+1
|/
* Some more proof cases, comments and cleanupLéo Gourdin2021-05-101-68/+1
* Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-091-5/+83
|\
| * idee pour simplifier la preuve: restreindre le "right_assoc" en "expand" !Sylvain Boulmé2021-05-081-5/+61
| * idea of a new scheme to define the semantics of LOAD NOTRAPSylvain Boulmé2021-05-071-0/+22
* | Some advance in proof and NOTRAP loads fixLéo Gourdin2021-05-071-6/+7
|/
* start RTL -> BTLSylvain Boulmé2021-05-061-49/+70
* finish verify_block and proofLéo Gourdin2021-05-051-21/+123
* advance in cfg checkerLéo Gourdin2021-05-051-1/+138
* debroussaillage et precisions...Sylvain Boulmé2021-05-011-15/+15
* BTLtoRTL: proof for internal/external/return statesLéo Gourdin2021-04-301-2/+2
* start the new "BTL" IR.Sylvain Boulmé2021-04-281-0/+575
generated by cgit (git 2.34.1) at 2024-07-04 13:13:21 +0000