Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| * | | finish RTLtoBTL proof | Léo Gourdin | 2021-06-18 | 1 | -2/+18 | |
| * | | End of main scheduling proof | Léo Gourdin | 2021-06-18 | 3 | -59/+90 | |
| * | | some advance, new section to simplify context from symbolic exec | Léo Gourdin | 2021-06-17 | 3 | -66/+151 | |
| * | | some advance in sched proof | Léo Gourdin | 2021-06-15 | 1 | -24/+92 | |
| * | | Preparation for scheduling proof, main lemmas ok | Léo Gourdin | 2021-06-14 | 4 | -16/+41 | |
| * | | begin scheduler BTL proof | Léo Gourdin | 2021-06-14 | 2 | -5/+142 | |
| * | | stub match_states | Sylvain Boulmé | 2021-06-11 | 1 | -1/+3 | |
| * | | add hid in BTL_SEtheory: this avoids duplication of types (and should not be ... | Sylvain Boulmé | 2021-06-11 | 2 | -150/+157 | |
| * | | Roadmap: precision sur le cout de verification des superblocks | Sylvain Boulmé | 2021-06-11 | 1 | -2/+9 | |
| * | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int... | Sylvain Boulmé | 2021-06-11 | 4 | -39/+43 | |
| |\ \ | ||||||
| | * \ | Merge branch 'kvx-work' into BTL | Léo Gourdin | 2021-06-10 | 4 | -39/+43 | |
| | |\ \ | ||||||
| * | | | | proving the remaining lemma for sexec_rec_okpreserv | Sylvain Boulmé | 2021-06-11 | 1 | -123/+162 | |
| |/ / / | ||||||
| * | | | theorem rexec_simu_correct | Sylvain Boulmé | 2021-06-10 | 1 | -25/+111 | |
| * | | | fix rst_simu_correct | Sylvain Boulmé | 2021-06-10 | 1 | -27/+21 | |
| * | | | remove history | Sylvain Boulmé | 2021-06-10 | 2 | -196/+121 | |
| * | | | fix sstate_simu | Sylvain Boulmé | 2021-06-09 | 2 | -32/+35 | |
| * | | | valid_pointer_preserv dans BTL_SEtheory => opportunites de *grosses* simplifi... | Sylvain Boulmé | 2021-06-09 | 2 | -87/+42 | |
| * | | | generalize nested | Sylvain Boulmé | 2021-06-09 | 1 | -71/+74 | |
| * | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int... | Sylvain Boulmé | 2021-06-08 | 1 | -28/+172 | |
| |\ \ \ | ||||||
| | * | | | End of liveness proof | Léo Gourdin | 2021-06-07 | 1 | -54/+45 | |
| | * | | | ugly complete version of liveness proof (I will clean in next commits) | Léo Gourdin | 2021-06-07 | 1 | -34/+40 | |
| | * | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int... | Léo Gourdin | 2021-06-07 | 3 | -27/+351 | |
| | |\ \ \ | ||||||
| | * | | | | advance for tr_input proof | Léo Gourdin | 2021-06-07 | 1 | -24/+171 | |
| * | | | | | preuve de rexec_rec_correct via les notions history/histOK | Sylvain Boulmé | 2021-06-08 | 1 | -41/+251 | |
| | |/ / / | |/| | | | ||||||
| * | | | | avancement ref de l'exe symbolique | Sylvain Boulmé | 2021-06-07 | 2 | -26/+306 | |
| * | | | | m | Sylvain Boulmé | 2021-06-06 | 1 | -1/+3 | |
| * | | | | IDEE pour la STRENGTH-REDUCTION | Sylvain Boulmé | 2021-06-06 | 1 | -1/+43 | |
| |/ / / | ||||||
| * | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int... | Léo Gourdin | 2021-06-04 | 2 | -12/+115 | |
| |\ \ \ | ||||||
| | * | | | starting refinement of symbolic execution | Sylvain Boulmé | 2021-06-04 | 2 | -12/+115 | |
| * | | | | preparation and starting final lemma | Léo Gourdin | 2021-06-04 | 1 | -21/+100 | |
| |/ / / | ||||||
| * | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int... | Léo Gourdin | 2021-06-04 | 3 | -35/+77 | |
| |\ \ \ | ||||||
| | * | | | progress in BTL_SEsimuref | Sylvain Boulmé | 2021-06-04 | 3 | -35/+77 | |
| * | | | | Some advance in Liveness lemmas | Léo Gourdin | 2021-06-04 | 1 | -71/+138 | |
| |/ / / | ||||||
| * | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int... | Léo Gourdin | 2021-06-03 | 2 | -109/+112 | |
| |\ \ \ | ||||||
| | * \ \ | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int... | Sylvain Boulmé | 2021-06-03 | 1 | -21/+112 | |
| | |\ \ \ | ||||||
| | * | | | | progress in BTL_SEsimuref | Sylvain Boulmé | 2021-06-03 | 2 | -109/+112 | |
| * | | | | | update a more general version of the liveness checker | Léo Gourdin | 2021-06-03 | 1 | -93/+118 | |
| | |/ / / | |/| | | | ||||||
| * | | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int... | Léo Gourdin | 2021-06-02 | 2 | -176/+255 | |
| |\| | | | ||||||
| | * | | | minor renaming | Sylvain Boulmé | 2021-06-02 | 1 | -9/+9 | |
| | * | | | fix the definition of [symbolic_simu] in BTL_SEtheory | Sylvain Boulmé | 2021-06-02 | 2 | -172/+251 | |
| * | | | | lemmas on entrypoint, tr_inputs, eqlive_regs, ... | Léo Gourdin | 2021-06-02 | 1 | -21/+112 | |
| |/ / / | ||||||
| * | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int... | Léo Gourdin | 2021-06-02 | 3 | -110/+416 | |
| |\ \ \ | ||||||
| | * | | | the current "high-level" specification of the simulation test will not work ! | Sylvain Boulmé | 2021-06-02 | 3 | -37/+124 | |
| | * | | | starting BTL_SEsimuref | Sylvain Boulmé | 2021-06-01 | 2 | -99/+318 | |
| * | | | | some advance in main liveness lemmas | Léo Gourdin | 2021-06-02 | 1 | -28/+68 | |
| |/ / / | ||||||
| * | | | Some others main lemmas | Léo Gourdin | 2021-06-01 | 1 | -7/+33 | |
| * | | | preparing liveness proof main theorem | Léo Gourdin | 2021-06-01 | 1 | -2/+43 | |
| * | | | Lemma liveness_checker_correct | Léo Gourdin | 2021-06-01 | 1 | -0/+12 | |
| * | | | Lemma list_iblock_checker_correct | Léo Gourdin | 2021-06-01 | 1 | -0/+20 | |
| * | | | Dupmap bugfix and some advance in Livegen | Léo Gourdin | 2021-05-31 | 4 | -29/+89 |