Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 |
|\ | |||||
| * | centralize if_same | David Monniaux | 2020-10-09 | 1 | -6/+0 |
| | | |||||
| * | do not synthesize select if both operands are identical | David Monniaux | 2020-10-09 | 2 | -7/+22 |
| | | |||||
* | | 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 |
| |\| | |||||
| | * | simpl -> cbn | David Monniaux | 2020-09-29 | 23 | -793/+789 |
| | | | |||||
| * | | 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 |
| | |/ | |||||
| | * | use scheduler_by_name | David Monniaux | 2020-09-10 | 3 | -9/+11 |
| | | | |||||
| * | | 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 ↵ | David Monniaux | 2020-09-10 | 12 | -222/+230 |
| |\ \ | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif-hash-junk | ||||
| | * | | Merge remote-tracking branch 'origin/kvx-work' into ↵ | David Monniaux | 2020-09-05 | 6 | -75/+117 |
| | |\| | | | | | | | | | | | | | | | | | | | | | mppa-RTLpathSE-verif-hash-junk iMe | ||||
| | | * | fix issue 198 (incorrect reservation table for multiply-add) | David Monniaux | 2020-09-02 | 1 | -5/+5 |
| | | | | |||||
| | | * | "nop" is not even printed out and thus uses no resources | David Monniaux | 2020-09-01 | 1 | -13/+21 |
| | | | | |||||
| | | * | clean solution to close channels | David Monniaux | 2020-08-31 | 1 | -21/+24 |
| | | | | |||||
| | | * | fix problem with some file descriptors possibly never getting closed | David Monniaux | 2020-08-31 | 1 | -4/+10 |
| | | | | | | | | | | | | | | | | (need to propagate fix to other kinds of solvers) | ||||
| | | * | links to the impure library on github | Sylvain Boulmé | 2020-07-31 | 1 | -1/+2 |
| | | | | |||||
| | | * | Improving Coqdoc on abstractbb | Sylvain Boulmé | 2020-07-31 | 4 | -46/+71 |
| | | | | |||||
| * | | | 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 |
| | | | | |||||
* | | | | oops: forget to save before compile/commit/push | Sylvain Boulmé | 2020-10-12 | 1 | -2/+5 |
| | | | | |||||
* | | | | end of merge with Cyril's proof | Sylvain Boulmé | 2020-10-12 | 2 | -59/+227 |
| | | | | |||||
* | | | | starting to merge with Cyril's proof | Sylvain Boulmé | 2020-10-11 | 1 | -48/+773 |
| | | | | |||||
* | | | | hconsing: full proof of hsiexec_path_correct | Sylvain Boulmé | 2020-10-10 | 2 | -42/+71 |
| | | | | |||||
* | | | | progress on hslocal_set_sreg_correct | Sylvain Boulmé | 2020-10-10 | 1 | -37/+53 |
| | | | | |||||
* | | | | progress on hsexec_inst_correct_dyn | Sylvain Boulmé | 2020-10-10 | 1 | -39/+140 |
| | | | | |||||
* | | | | hconsing: red_PTree_set_correct | Sylvain Boulmé | 2020-10-09 | 1 | -0/+11 |
| | | | | |||||
* | | | | hconsing: root_happly_correct + simplify_correct DONE | Sylvain Boulmé | 2020-10-09 | 4 | -15/+145 |
| | | | | |||||
* | | | | prove the kvx-test-prepass fix (commit 0e4186b8f) | Sylvain Boulmé | 2020-10-08 | 1 | -14/+58 |
| | | | | | | | | | | | | | | | | (only in the version without hconsing) | ||||
* | | | | Merge branch 'mppa-RTLpathSE-verif_Op_mem-irrel' into mppa-RTLpathSE-xverif | Sylvain Boulmé | 2020-10-08 | 1 | -30/+29 |
|\ \ \ \ | |||||
| * | | | | prove the trick of simplify (as implemented in RTLpathSE_impl_junk) | Sylvain Boulmé | 2020-08-27 | 1 | -18/+6 |
| | | | | | |||||
| * | | | | prove that Mem.valid is preserved by symbolic execution of RTLpath | Sylvain Boulmé | 2020-08-27 | 1 | -12/+22 |
| | | | | | |||||
* | | | | | Restart the proof with cherry-pick from Cyril and commit 0e4186b8f | Sylvain Boulmé | 2020-10-08 | 2 | -1795/+433 |
| | | | | | |||||
* | | | | | update from kvx-test-prepass (commit 0e4186b8f) | Sylvain Boulmé | 2020-10-08 | 1 | -4/+10 |
| | | | | | |||||
* | | | | | Some theorem was wrong | Cyril SIX | 2020-09-30 | 1 | -4/+18 |
| | | | | | |||||
* | | | | | Proof of hsok_local_set_sreg | Cyril SIX | 2020-09-30 | 1 | -4/+25 |
| | | | | |