Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | DuplicateParam -> DuplicateOracle + simpler Duplicatepasses | Sylvain Boulmé | 2020-10-28 | 1 | -1/+1 |
| | |||||
* | Reworked Duplicate to be parametrized | Cyril SIX | 2020-10-27 | 1 | -0/+5 |
| | |||||
* | Adding copyrights | Cyril SIX | 2020-05-04 | 1 | -0/+14 |
| | |||||
* | Adding info field for branching in RTL, LTL, XTL and all associated passes | Cyril SIX | 2020-03-11 | 1 | -4/+4 |
| | |||||
* | removing some coqc 8.10 warnings | Sylvain Boulmé | 2020-03-09 | 1 | -1/+1 |
| | |||||
* | Revert "Modified the hook for the oracle" | Cyril SIX | 2020-01-23 | 1 | -3/+2 |
| | | | | | | This reverts commit 04a46f516487557df00f43453c8decbc8567c458. It was actually not needed | ||||
* | Verificator finished for handling reversed Icond | Cyril SIX | 2020-01-23 | 1 | -5/+9 |
| | |||||
* | Added clause in match_inst to allow Icond reversal | Cyril SIX | 2020-01-23 | 1 | -4/+13 |
| | |||||
* | Modified the hook for the oracle | Cyril SIX | 2020-01-23 | 1 | -2/+3 |
| | |||||
* | make it compile for ARM | David Monniaux | 2019-12-06 | 1 | -4/+4 |
| | |||||
* | finish merge | David Monniaux | 2019-12-02 | 1 | -2/+18 |
| | |||||
* | Duplicateproof: minor edit | Sylvain Boulmé | 2019-11-26 | 1 | -3/+4 |
| | |||||
* | simplification of Duplicate: remove xfunction | Sylvain Boulmé | 2019-11-14 | 1 | -117/+119 |
| | |||||
* | Merge remote-tracking branch 'origin/mppa-duplicate-rtl-alt' into mppa-work | Cyril SIX | 2019-10-24 | 1 | -53/+77 |
|\ | |||||
| * | An alternative proof where the match_state does not depend on the translation | Sylvain Boulmé | 2019-10-23 | 1 | -53/+77 |
| | | |||||
* | | eq_condition already existed | David Monniaux | 2019-10-16 | 1 | -1/+1 |
|/ | |||||
* | Finished Duplicate proof. | Cyril SIX | 2019-10-07 | 1 | -35/+40 |
| | |||||
* | Icond | Cyril SIX | 2019-10-07 | 1 | -0/+9 |
| | |||||
* | Itailcall | Cyril SIX | 2019-10-07 | 1 | -2/+8 |
| | |||||
* | Ireturn | Cyril SIX | 2019-10-07 | 1 | -0/+4 |
| | |||||
* | Ibuiltin proof | Cyril SIX | 2019-10-04 | 1 | -0/+7 |
| | |||||
* | Icall | Cyril SIX | 2019-10-03 | 1 | -0/+8 |
| | |||||
* | Iload and Istore | Cyril SIX | 2019-10-03 | 1 | -3/+19 |
| | |||||
* | Proof for Iop | Cyril SIX | 2019-10-03 | 1 | -0/+7 |
| | |||||
* | Preparing the terrain for the rest of the instructions with one successor | Cyril SIX | 2019-10-03 | 1 | -5/+17 |
| | |||||
* | Duplicate - Proof of verificator for Inop | Cyril SIX | 2019-10-03 | 1 | -3/+81 |
| | |||||
* | Starting implementing the verificator | Cyril SIX | 2019-10-02 | 1 | -1/+1 |
| | |||||
* | Proof of first axiom | Cyril SIX | 2019-09-11 | 1 | -1/+10 |
| | |||||
* | Fixing Linking problem | Cyril SIX | 2019-09-11 | 1 | -16/+16 |
| | |||||
* | Utilisation d'un intermédiaire xfunction contenant le revmap | Cyril SIX | 2019-09-11 | 1 | -34/+48 |
| | |||||
* | Duplicate: proof complete, assuming revmap, revmap_correct and revmap_entrypoint | Cyril SIX | 2019-09-06 | 1 | -5/+21 |
| | |||||
* | Duplicate: big progress on step_simulation, only Ijumptbl left | Cyril SIX | 2019-09-05 | 1 | -74/+138 |
| | |||||
* | Duplicate: changement de match_nodes | Cyril SIX | 2019-09-04 | 1 | -36/+44 |
| | |||||
* | Duplicate: exec_function_external et exec_return | Cyril SIX | 2019-09-04 | 1 | -3/+7 |
| | |||||
* | Duplicate: exec_function_internal | Cyril SIX | 2019-09-04 | 1 | -2/+34 |
| | |||||
* | transf_initial_states | Cyril SIX | 2019-09-04 | 1 | -4/+66 |
| | |||||
* | Duplicate: match_states | Cyril SIX | 2019-09-03 | 1 | -2/+10 |
| | |||||
* | Duplicate: match_nodes | Cyril SIX | 2019-09-03 | 1 | -8/+57 |
| | |||||
* | Start of match_states | Cyril SIX | 2019-09-03 | 1 | -3/+23 |
| | |||||
* | Stubs for Duplicate pass | Cyril SIX | 2019-09-03 | 1 | -0/+29 |