aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTL_SEtheory.v
Commit message (Expand)AuthorAgeFilesLines
* [Cherry picking] 01ade46b340267d8782c413f6bd5a3cff13ef0a6Léo Gourdin2021-12-061-26/+26
* cleaner symbolic semantic of load trapsSylvain Boulmé2021-10-251-12/+10
* [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-011-2/+2
* non trapping loadsLéo Gourdin2021-07-231-17/+27
* add hid in BTL_SEtheory: this avoids duplication of types (and should not be ...Sylvain Boulmé2021-06-111-127/+142
* remove historySylvain Boulmé2021-06-101-8/+10
* fix sstate_simuSylvain Boulmé2021-06-091-1/+17
* valid_pointer_preserv dans BTL_SEtheory => opportunites de *grosses* simplifi...Sylvain Boulmé2021-06-091-21/+29
* avancement ref de l'exe symboliqueSylvain Boulmé2021-06-071-7/+4
* starting refinement of symbolic executionSylvain Boulmé2021-06-041-9/+9
* progress in BTL_SEsimurefSylvain Boulmé2021-06-041-23/+11
* progress in BTL_SEsimurefSylvain Boulmé2021-06-031-31/+54
* minor renamingSylvain Boulmé2021-06-021-9/+9
* fix the definition of [symbolic_simu] in BTL_SEtheorySylvain Boulmé2021-06-021-64/+243
* the current "high-level" specification of the simulation test will not work !Sylvain Boulmé2021-06-021-10/+48
* starting BTL_SEsimurefSylvain Boulmé2021-06-011-99/+1
* remove dupmap from BTL_Scheduler !Sylvain Boulmé2021-05-281-14/+10
* archi pour la verif du schedulerSylvain Boulmé2021-05-281-11/+13
* fix some merge errorsLéo Gourdin2021-05-281-1/+1
* Merge branch 'BTL_fsem' into BTLLéo Gourdin2021-05-281-246/+295
|\
| * most of the proof BTL.fsem -> BTL.cfgsem.Sylvain Boulmé2021-05-281-1/+1
| * cleaning BTL_SEtheorySylvain Boulmé2021-05-271-190/+114
| * end of BTL_SEtheory w.r.t fsemSylvain Boulmé2021-05-271-162/+169
| * fix tr_sis definitionSylvain Boulmé2021-05-261-57/+90
| * fix Builtin semanticsSylvain Boulmé2021-05-251-27/+3
| * starting to experiment SE of fsemSylvain Boulmé2021-05-251-55/+158
| * defines fsem (aka functional semantics) of BTLSylvain Boulmé2021-05-201-6/+12
* | Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-201-7/+7
* | Adding a BTL record to help oraclesLéo Gourdin2021-05-191-11/+11
|/
* better autodestruct ?Sylvain Boulmé2021-05-111-16/+0
* prove sexec_exactSylvain Boulmé2021-05-111-11/+323
* sexec: renommage Sdead -> Sabort + simplification de sexec_correctSylvain Boulmé2021-05-081-57/+21
* 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
* refactorisation + 1ere version de sstateSylvain Boulmé2021-05-061-1461/+169
* init BTL_SEtheory (by copy/paste from RTLpathSE_theory)Sylvain Boulmé2021-05-061-0/+1831
generated by cgit (git 2.34.1) at 2024-05-08 21:15:00 +0000