aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
* correction de l'idee de la Functional semanticsSylvain Boulmé2021-05-201-26/+17
* Merge branch 'kvx-work' into BTLLéo Gourdin2021-05-198-48/+1410
|\
| * Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-198-48/+1410
| * Merge branch 'riscv-work-fpinit-stillexp' into kvx-workLéo Gourdin2021-05-190-0/+0
| |\
| | * xorimmsubmission_OOPSLA2021_RISCVLéo Gourdin2021-04-092-0/+77
| | * removing useless flag checkLéo Gourdin2021-04-091-3/+1
* | | Merge branch 'kvx-work' into BTLLéo Gourdin2021-05-1912-80/+105
|\| |
| * | debug prints uniformizedLéo Gourdin2021-05-181-69/+66
| * | for making the dockerDavid Monniaux2021-05-114-0/+3
| * | for pruning the dockerDavid Monniaux2021-05-111-1/+2
| * | pruning the imageDavid Monniaux2021-05-111-0/+4
| * | adjust to compile for various archDavid Monniaux2021-05-111-3/+3
| * | progress being madeDavid Monniaux2021-05-101-2/+15
| * | build for aarch64David Monniaux2021-05-101-1/+4
| * | dockerfilesDavid Monniaux2021-05-102-8/+9
| * | dockerfile for buildingDavid Monniaux2021-05-101-0/+8
| * | Increasing required OCaml version (Pervasives <-> Stdlib module renaming)Cyril SIX2021-05-041-2/+2
| * | for OCaml 4.13David Monniaux2021-04-301-1/+1
| * | Compatibilité Coq 8.13David Monniaux2021-04-285-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-114-14/+325
|\ \ \
| * | | better autodestruct ?Sylvain Boulmé2021-05-112-17/+16
| * | | 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
generated by cgit (git 2.34.1) at 2024-07-14 04:13:36 +0000