aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
* 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 int...Sylvain Boulmé2021-06-11347-6030/+10566
|\
| * 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 https://gricad-gitlab.univ-grenoble-alpes.fr/sixcy...Olivier Lebeltel2021-06-091-1/+1
| | |\
| | | * 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
| | * timingDavid Monniaux2021-06-072-0/+117
| | * Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2021-06-06340-6016/+11801
| | |\
generated by cgit (git 2.34.1) at 2024-07-06 15:39:05 +0000