aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTL.v
Commit message (Expand)AuthorAgeFilesLines
* 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