aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-06-024-111/+417
|\
| * the current "high-level" specification of the simulation test will not work !Sylvain Boulmé2021-06-023-37/+124
| * starting BTL_SEsimurefSylvain Boulmé2021-06-013-100/+319
* | some advance in main liveness lemmasLéo Gourdin2021-06-021-28/+68
|/
* Some others main lemmasLéo Gourdin2021-06-011-7/+33
* preparing liveness proof main theoremLéo Gourdin2021-06-011-2/+43
* Lemma liveness_checker_correctLéo Gourdin2021-06-011-0/+12
* Lemma list_iblock_checker_correctLéo Gourdin2021-06-011-0/+20
* Dupmap bugfix and some advance in LivegenLéo Gourdin2021-05-316-30/+92
* Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-311-19/+13
|\
| * prove fsem2cfgsem_ibistep_simuSylvain Boulmé2021-05-311-19/+13
* | remove accidentally pushed test scriptsLéo Gourdin2021-05-313-44/+0
|/
* BTL Scheduler oracle and some draftsLéo Gourdin2021-05-319-13/+136
* BTLroadmap: jumptableSylvain Boulmé2021-05-291-1/+1
* maj roadmapSylvain Boulmé2021-05-281-36/+32
* declare a checker for the symbolic simulationSylvain Boulmé2021-05-281-2/+13
* remove dupmap from BTL_Scheduler !Sylvain Boulmé2021-05-283-36/+22
* archi pour la verif du schedulerSylvain Boulmé2021-05-283-11/+82
* starting to extend RTLtoBTL with Liveness checking (on BTL side)Sylvain Boulmé2021-05-288-37/+99
* splitting BTL by introducing BTLmatchRTLSylvain Boulmé2021-05-287-635/+615
* fix some merge errorsLéo Gourdin2021-05-284-4/+5
* Merge branch 'BTL_fsem' into BTLLéo Gourdin2021-05-285-284/+840
|\
| * most of the proof BTL.fsem -> BTL.cfgsem.Sylvain Boulmé2021-05-284-46/+280
| * cleaning BTL_SEtheorySylvain Boulmé2021-05-272-190/+187
| * end of BTL_SEtheory w.r.t fsemSylvain Boulmé2021-05-273-182/+194
| * fix tr_sis definitionSylvain Boulmé2021-05-262-81/+132
| * avancement roadmapSylvain Boulmé2021-05-261-11/+28
| * fix Builtin semanticsSylvain Boulmé2021-05-252-37/+27
| * starting to experiment SE of fsemSylvain Boulmé2021-05-252-72/+232
| * improve fsemSylvain Boulmé2021-05-211-15/+30
| * update roadmapSylvain Boulmé2021-05-201-3/+10
| * defines fsem (aka functional semantics) of BTLSylvain Boulmé2021-05-204-19/+92
* | Improvements in scheduling and renumbering BTL codeLéo Gourdin2021-05-285-94/+65
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-272-349/+302
|\ \
| * | simplification of normRTLSylvain Boulmé2021-05-251-67/+27
| * | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-05-244-21/+231
| |\ \
| * | | tiny simplifications in RTLtoBTLproofSylvain Boulmé2021-05-242-349/+342
* | | | [disabled checker] BTL Scheduling and Renumbering OK!Léo Gourdin2021-05-2715-181/+349
| |/ / |/| |
* | | a draft frontend for prepassLéo Gourdin2021-05-244-21/+231
|/ /
* | Moving common tools, adding liveness input/output information to BTL generati...Léo Gourdin2021-05-2412-54/+73
* | 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-2020-185/+612
|\ \ | |/ |/|
| * 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-209-127/+145
| * Merge branch 'BTL' into BTL-translationLéo Gourdin2021-05-1920-128/+1519
| |\
| * | Adding a BTL record to help oraclesLéo Gourdin2021-05-197-165/+265
| * | Grouping common RTL functions, printer improvementLéo Gourdin2021-05-198-117/+79
| * | first oracle seems okLéo Gourdin2021-05-182-11/+15
| * | oracle simplification, BTL printer, and error msg specLéo Gourdin2021-05-183-97/+253
generated by cgit (git 2.34.1) at 2024-07-12 05:07:32 +0000