aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'BTL-SEimpl' of ↵Léo Gourdin2021-07-222-16/+14
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL-SEimpl
| * fix ciLéo Gourdin2021-07-212-16/+14
| |
* | renamingLéo Gourdin2021-07-221-51/+51
|/
* new expansionsLéo Gourdin2021-07-212-15/+935
|
* expansions btl proofsLéo Gourdin2021-07-215-9/+1008
|
* bug fix in oracleLéo Gourdin2021-07-201-33/+360
|
* new expansion oracle for BTLLéo Gourdin2021-07-204-6/+336
|
* fix depsLéo Gourdin2021-07-201-1/+2
|
* Fix compile on ARM/x86 backendsLéo Gourdin2021-07-208-1714/+181
|
* op simplify BTL introLéo Gourdin2021-07-208-10/+56
|
* proof for symbolic simu, need to finish equiv_inputsLéo Gourdin2021-07-203-23/+31
|
* Finish implem proof, need to adapt scheduler proofLéo Gourdin2021-07-194-114/+373
|
* hrexec_correct1Léo Gourdin2021-07-081-25/+48
|
* some progress in canonbuildingLéo Gourdin2021-07-071-14/+106
|
* symbolic_simu impl definitionsLéo Gourdin2021-07-071-47/+9
|
* hrexec1Léo Gourdin2021-07-071-27/+81
|
* progress in simulation testLéo Gourdin2021-07-071-57/+250
|
* Some advance, need to finish canonbuilding proofsLéo Gourdin2021-07-061-13/+270
|
* lemma on HC_set_regLéo Gourdin2021-07-052-52/+165
|
* red_PTree lemmasLéo Gourdin2021-07-012-10/+77
|
* cbranch expanseLéo Gourdin2021-06-301-0/+25
|
* coercions and simplifyLéo Gourdin2021-06-302-3/+91
|
* some advanceLéo Gourdin2021-06-301-14/+154
|
* Starting symbolic execution implementationLéo Gourdin2021-06-301-0/+314
|
* BTLroadmap: combinaison liveness et invariants ?Sylvain Boulmé2021-06-251-9/+47
|
* update BTLroadmapSylvain Boulmé2021-06-241-5/+6
|
* transf fct correct in BTL scheduler proofLéo Gourdin2021-06-201-5/+5
|
* finish main proofLéo Gourdin2021-06-191-18/+128
|
* lemma on eqregs?Léo Gourdin2021-06-182-14/+7
|
* finish RTLtoBTL proofLéo Gourdin2021-06-181-2/+18
|
* End of main scheduling proofLéo Gourdin2021-06-183-59/+90
|
* some advance, new section to simplify context from symbolic execLéo Gourdin2021-06-173-66/+151
|
* some advance in sched proofLéo Gourdin2021-06-151-24/+92
|
* Preparation for scheduling proof, main lemmas okLéo Gourdin2021-06-144-16/+41
|
* begin scheduler BTL proofLéo Gourdin2021-06-142-5/+142
|
* stub match_statesSylvain Boulmé2021-06-111-1/+3
|
* add hid in BTL_SEtheory: this avoids duplication of types (and should not be ↵Sylvain Boulmé2021-06-112-150/+157
| | | | harmful)
* Roadmap: precision sur le cout de verification des superblocksSylvain Boulmé2021-06-111-2/+9
|
* Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵Sylvain Boulmé2021-06-11347-6030/+10566
|\ | | | | | | into BTL
| * remove filter fileLéo Gourdin2021-06-101-39/+0
| |
| * Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-10346-5991/+10566
| |\
| | * push afadl test exampleLéo Gourdin2021-06-092-0/+21
| | |
| | * Merge branch 'kvx-work' of ↵Olivier Lebeltel2021-06-091-1/+1
| | |\ | | | | | | | | | | | | https://gricad-gitlab.univ-grenoble-alpes.fr/sixcy/CompCert into kvx-work
| | | * comment is now ## due to some weird MacOS bugDavid Monniaux2021-06-091-1/+1
| | | |
| | * | added config_macos_x86_64.shOlivier Lebeltel2021-06-091-0/+1
| | |/
| | * MacOS compatibilityDavid Monniaux2021-06-091-1/+1
| | |
| | * run CI on kvx-work-ssa kvx-work-velusDavid Monniaux2021-06-081-49/+57
| | |
| | * omega -> liaDavid Monniaux2021-06-081-8/+8
| | |
| | * coq 8.13.2David Monniaux2021-06-071-2/+1
| | |
| | * divisionDavid Monniaux2021-06-072-3/+4
| | |
generated by cgit (git 2.34.1) at 2024-07-12 03:42:46 +0000