| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | use a more recognizable option name | David Monniaux | 2021-07-16 | 3 | -3/+519 |
| * | fix for KVX | David Monniaux | 2021-07-16 | 1 | -2/+8 |
| * | setup registers | David Monniaux | 2021-07-16 | 2 | -0/+5 |
| * | Replacing default notrap load value by Vundef everywherecsix-PhD | Cyril SIX | 2021-06-18 | 4 | -17/+16 |
| * | fix modeling issue (Vundef for load outside of bounds) | David Monniaux | 2021-06-16 | 1 | -2/+7 |
| * | replacing omega with lia in some file | Léo Gourdin | 2021-03-29 | 13 | -141/+154 |
| * | Merge branch 'master' into merge_master_8.13.1 | Sylvain Boulmé | 2021-03-23 | 3 | -23/+38 |
| * | fix ci ? | Léo Gourdin | 2021-03-02 | 2 | -0/+2 |
| * | Conditions now propagated by CSE3 | David Monniaux | 2021-01-20 | 1 | -13/+36 |
| |\ | |||||
| | * | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-08 | 10 | -45/+44 |
| | |\ | |||||
| | * | | simpl -> cbn | David Monniaux | 2020-12-02 | 1 | -9/+9 |
| | * | | cond_depends_on_memory for KVX | David Monniaux | 2020-12-02 | 1 | -4/+17 |
| | * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-02 | 23 | -3313/+117 |
| | |\ \ | |||||
| | * | | | cond_valid_pointer_eq | David Monniaux | 2020-11-25 | 1 | -0/+10 |
| * | | | | update kvx | Sylvain Boulmé | 2021-01-07 | 4 | -98/+45 |
| * | | | | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2020-12-17 | 11 | -53/+57 |
| |\ \ \ \ | |||||
| | * | | | | upgrade kvx backend to coq.8.12.2 | Sylvain Boulmé | 2020-12-16 | 5 | -33/+41 |
| | | |_|/ | |/| | | |||||
| | * | | | Fixing test/regression for KVXv3.8_kvx | Cyril SIX | 2020-12-07 | 4 | -2/+16 |
| | * | | | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 26 | -3325/+159 |
| | |\ \ \ | | | |/ | | |/| | |||||
| | | * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | Cyril SIX | 2020-12-01 | 1 | -1/+0 |
| | | |\| | |||||
| | * | | | Fixing compilation for KVX | Cyril SIX | 2020-12-04 | 1 | -0/+3 |
| | * | | | still issues with FR in kvx | David Monniaux | 2020-12-03 | 3 | -27/+26 |
| | * | | | some fixes for KVX | David Monniaux | 2020-12-03 | 2 | -6/+0 |
| | * | | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 2 | -11/+0 |
| * | | | | Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy... | David Monniaux | 2020-11-27 | 36 | -9674/+117 |
| |\ \ \ \ | | |/ / | |/| | | |||||
| | * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-24 | 2 | -12/+22 |
| | |\ \ \ | |||||
| | * | | | | new OpWeights | David Monniaux | 2020-10-22 | 2 | -0/+25 |
| | * | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 2 | -7/+16 |
| | |\ \ \ \ | | | |/ / | | |/| | | |||||
| | * | | | | update op_valid_pointer_eq proof on the KVX | Sylvain Boulmé | 2020-10-17 | 1 | -22/+4 |
| | * | | | | fixing the move of the verified prepass scheduler into scheduling/ directory | Sylvain Boulmé | 2020-10-17 | 1 | -872/+0 |
| | * | | | | Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verif | Cyril SIX | 2020-10-16 | 55 | -11464/+859 |
| | |\ \ \ \ | |||||
| | | * | | | | so that all architectures compile | David Monniaux | 2020-10-02 | 1 | -0/+1 |
| | | * | | | | non pipelined units = none on KVX | David Monniaux | 2020-09-30 | 1 | -1/+3 |
| | | * | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-09-29 | 23 | -769/+765 |
| | | |\ \ \ \ | |||||
| | | * \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepass | David Monniaux | 2020-09-22 | 1 | -14/+0 |
| | | |\ \ \ \ \ | |||||
| | | | * | | | | | reflect changes | David Monniaux | 2020-09-22 | 1 | -14/+0 |
| | | * | | | | | | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepass | David Monniaux | 2020-09-21 | 2 | -272/+1 |
| | | |\| | | | | | |||||
| | | | * | | | | | moved some "total" value domain functions to a central location | David Monniaux | 2020-09-21 | 1 | -271/+0 |
| | | * | | | | | | just missing OpWeights for AARCH64 | David Monniaux | 2020-09-16 | 14 | -9446/+0 |
| | | * | | | | | | starting to move common files | David Monniaux | 2020-09-16 | 16 | -1651/+0 |
| | | * | | | | | | Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-... | David Monniaux | 2020-09-10 | 12 | -222/+230 |
| | | |\ \ \ \ \ \ | |||||
| | | | * \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash... | David Monniaux | 2020-09-05 | 6 | -75/+117 |
| | | | |\ \ \ \ \ \ | |||||
| | | * | | | | | | | | use with_destructor | David Monniaux | 2020-09-10 | 2 | -20/+29 |
| | * | | | | | | | | | removing useless opt_simu | Sylvain Boulmé | 2020-10-13 | 3 | -36/+25 |
| | * | | | | | | | | | refactoring of RTLpathSE_impl.v (split with _simu_specs) | Sylvain Boulmé | 2020-10-13 | 5 | -3911/+2086 |
| | * | | | | | | | | | remove the last tiny issue! | Sylvain Boulmé | 2020-10-12 | 1 | -10/+3 |
| | * | | | | | | | | | simpl hsstate_simu_core_correct | Sylvain Boulmé | 2020-10-12 | 1 | -3/+1 |
| | * | | | | | | | | | fix one issue by generalizing RTLpathSE_theory.sstate_simu | Sylvain Boulmé | 2020-10-12 | 2 | -9/+18 |
| | * | | | | | | | | | move issue from hsexec_correct to hsstate_simu_core_correct | Sylvain Boulmé | 2020-10-12 | 1 | -14/+19 |
| | * | | | | | | | | | most of the proof is done ! two (small ?) issues remain... | Sylvain Boulmé | 2020-10-12 | 1 | -30/+83 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |