aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTL.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-011-2/+1
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-16/+2
* [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-011-5/+3
* non trapping loadsLéo Gourdin2021-07-231-13/+38
* splitting BTL by introducing BTLmatchRTLSylvain Boulmé2021-05-281-559/+6
* fix some merge errorsLéo Gourdin2021-05-281-2/+2
* Merge branch 'BTL_fsem' into BTLLéo Gourdin2021-05-281-8/+483
|\
| * most of the proof BTL.fsem -> BTL.cfgsem.Sylvain Boulmé2021-05-281-41/+267
| * cleaning BTL_SEtheorySylvain Boulmé2021-05-271-0/+73
| * end of BTL_SEtheory w.r.t fsemSylvain Boulmé2021-05-271-2/+7
| * fix tr_sis definitionSylvain Boulmé2021-05-261-24/+42
| * 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
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-271-91/+1
|\ \
| * | tiny simplifications in RTLtoBTLproofSylvain Boulmé2021-05-241-91/+1
* | | [disabled checker] BTL Scheduling and Renumbering OK!Léo Gourdin2021-05-271-2/+2
|/ /
* | splitting is_expand property with a weak version for conditionsLéo Gourdin2021-05-231-22/+59
* | Now supporting Bnop insertion in conditionsLéo Gourdin2021-05-211-22/+44
* | Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-201-77/+81
* | Adding a BTL record to help oraclesLéo Gourdin2021-05-191-69/+74
* | oracle simplification, BTL printer, and error msg specLéo Gourdin2021-05-181-41/+41
* | preparing compiler passes and ml oraclesLéo Gourdin2021-05-171-4/+4
|/
* 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-05-08 14:43:28 +0000