aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
Commit message (Expand)AuthorAgeFilesLines
* Moving common tools, adding liveness input/output information to BTL generati...Léo Gourdin2021-05-247-50/+32
* splitting is_expand property with a weak version for conditionsLéo Gourdin2021-05-232-78/+117
* Now supporting Bnop insertion in conditionsLéo Gourdin2021-05-215-139/+135
* Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-05-2013-165/+550
|\
| * working oracles (no renumber for now)Léo Gourdin2021-05-205-79/+144
| * Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-207-125/+141
| * Merge branch 'BTL' into BTL-translationLéo Gourdin2021-05-194-10/+9
| |\
| * | Adding a BTL record to help oraclesLéo Gourdin2021-05-197-165/+265
| * | Grouping common RTL functions, printer improvementLéo Gourdin2021-05-194-108/+26
| * | first oracle seems okLéo Gourdin2021-05-182-11/+15
| * | oracle simplification, BTL printer, and error msg specLéo Gourdin2021-05-183-97/+253
| * | First draft of the RTL2BTL oracleLéo Gourdin2021-05-181-4/+105
| * | todosLéo Gourdin2021-05-181-1/+1
| * | preparing compiler passes and ml oraclesLéo Gourdin2021-05-176-12/+37
* | | correction de l'idee de la Functional semanticsSylvain Boulmé2021-05-201-26/+17
| |/ |/|
* | Merge branch 'kvx-work' into BTLLéo Gourdin2021-05-193-8/+3
|\ \
| * | Compatibilité Coq 8.13David Monniaux2021-04-283-8/+3
* | | status updateLéo Gourdin2021-05-181-2/+6
| |/ |/|
* | finishing RTLtoBTLLéo Gourdin2021-05-173-42/+35
* | mib lemmaLéo Gourdin2021-05-171-26/+29
* | Lemmas on ISTEPLéo Gourdin2021-05-172-194/+127
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-171-24/+61
|\ \
| * | fix roadmap on "Simulation modulo liveness"Sylvain Boulmé2021-05-121-24/+61
* | | some advanceLéo Gourdin2021-05-161-24/+191
* | | iblock_istep rec and correct lemmasLéo Gourdin2021-05-131-0/+83
|/ /
* | ascii simuLéo Gourdin2021-05-121-17/+48
* | finish proofLéo Gourdin2021-05-111-39/+45
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-113-13/+309
|\ \
| * | better autodestruct ?Sylvain Boulmé2021-05-111-16/+0
| * | pointeur Justus -> roadmapSylvain Boulmé2021-05-111-1/+1
| * | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-05-112-38/+77
| |\ \
| * | | prove sexec_exactSylvain Boulmé2021-05-112-12/+324
* | | | new lemma definition, some preparations in existing proofsLéo Gourdin2021-05-111-52/+65
| |/ / |/| |
* | | new strong_state predicate and lemmaLéo Gourdin2021-05-102-38/+77
|/ /
* | Some more proof cases, comments and cleanupLéo Gourdin2021-05-102-97/+97
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-101-4/+230
|\ \
| * | précision du roadmapSylvain Boulmé2021-05-101-4/+230
* | | is_exp and bcond proofLéo Gourdin2021-05-102-22/+36
|/ /
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-094-13/+372
|\ \
| * | sexec: renommage Sdead -> Sabort + simplification de sexec_correctSylvain Boulmé2021-05-081-57/+21
| * | idee pour simplifier la preuve: restreindre le "right_assoc" en "expand" !Sylvain Boulmé2021-05-083-5/+66
| * | 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
| |\ \
| * | | 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
* | | | mib_exit draftLéo Gourdin2021-05-091-3/+4
* | | | Some advance in proof and NOTRAP loads fixLéo Gourdin2021-05-072-10/+60
* | | | intermediate lemma for opt_simu intro caseLéo Gourdin2021-05-071-10/+21
| |/ / |/| |
* | | 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-071-0/+539
|\| |
generated by cgit (git 2.34.1) at 2024-06-02 18:25:44 +0000