| Commit message (Expand) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| | | * | | Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash... | David Monniaux | 2020-09-05 | 11 | -9848/+164 | |
| | | |\| | ||||||
| | | | * | remettre yarpgen | David Monniaux | 2020-09-02 | 1 | -1/+1 | |
| | | | * | 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 | |
| | | | * | example prog where list scheduler can be reoptimized using ILP | David Monniaux | 2020-08-31 | 1 | -0/+14 | |
| | | | * | 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 | |
| | | | * | links to the impure library on github | Sylvain Boulmé | 2020-07-31 | 2 | -2/+3 | |
| | | | * | Improving Coqdoc on abstractbb | Sylvain Boulmé | 2020-07-31 | 5 | -47/+72 | |
| | * | | | 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 | 6 | -3912/+2087 | |
| * | | | | 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 | |
| * | | | | 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 | |
| * | | | | | Some more progress | Cyril SIX | 2020-09-29 | 1 | -2/+33 | |
| * | | | | | Bit of progress | Cyril SIX | 2020-09-29 | 1 | -6/+40 | |
| * | | | | | Proof of simplify_correct | Cyril SIX | 2020-09-28 | 1 | -45/+101 | |
| * | | | | | A bit of new Ltac and renaming | Cyril SIX | 2020-09-21 | 1 | -23/+70 | |
| * | | | | | More avancement | Cyril SIX | 2020-09-18 | 1 | -3/+29 | |
| * | | | | | hsiexec_inst_correct_dyn proof of Iop | Cyril SIX | 2020-09-18 | 1 | -1/+42 | |
| * | | | | | Avancement | Cyril SIX | 2020-09-18 | 1 | -29/+83 | |
| * | | | | | Some renaming | Cyril SIX | 2020-09-18 | 1 | -129/+230 | |
| * | | | | | Proof of sfval_simu_check_correct | Cyril SIX | 2020-09-15 | 1 | -14/+132 | |
| * | | | | | Cleanup | Cyril SIX | 2020-09-09 | 1 | -4/+1 | |
| * | | | | | exec_final_correct proved | Cyril SIX | 2020-09-09 | 1 | -22/+122 | |
| * | | | | | Proving the last admit of ssem_final_simu | Cyril SIX | 2020-09-08 | 1 | -2/+24 | |
| * | | | | | hsexec_final_correct progress | Cyril SIX | 2020-09-07 | 1 | -2/+30 | |
| * | | | | | Proof of hfinal_simu_core_correct | Cyril SIX | 2020-09-07 | 4 | -35/+21 | |
| * | | | | | Proof of barg_proj_refines_eq | Cyril SIX | 2020-09-07 | 1 | -5/+43 | |
| * | | | | | Updates from _impl.v to _impl_junk.v | Cyril SIX | 2020-09-03 | 1 | -55/+102 | |
| * | | | | | Proof of hsilocal_simu_core_correct junk | Cyril SIX | 2020-09-03 | 1 | -14/+16 | |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |