aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Duplicate.v
Commit message (Expand)AuthorAgeFilesLines
* remove some useless "OK tt"Sylvain Boulmé2021-01-071-4/+4
* Making verify_mapping_mn_rec tail recursive (should fix arm CI) #231Cyril SIX2021-01-061-2/+1
* DuplicateParam -> DuplicateOracle + simpler DuplicatepassesSylvain Boulmé2020-10-281-3/+3
* Reworked Duplicate to be parametrizedCyril SIX2020-10-271-5/+21
* Adding copyrightsCyril SIX2020-05-041-0/+14
* Adding info field for branching in RTL, LTL, XTL and all associated passesCyril SIX2020-03-111-2/+2
* Revert "Modified the hook for the oracle"Cyril SIX2020-01-231-8/+5
* Verificator finished for handling reversed IcondCyril SIX2020-01-231-6/+9
* Modified the hook for the oracleCyril SIX2020-01-231-5/+8
* finish mergeDavid Monniaux2019-12-021-11/+13
* simplification of Duplicate: remove xfunctionSylvain Boulmé2019-11-141-70/+35
* Merge remote-tracking branch 'origin/mppa-duplicate-rtl-alt' into mppa-workCyril SIX2019-10-241-7/+0
|\
| * An alternative proof where the match_state does not depend on the translationSylvain Boulmé2019-10-231-7/+0
* | eq_condition already existedDavid Monniaux2019-10-161-1/+1
|/
* Finished Duplicate proof.Cyril SIX2019-10-071-1/+18
* IcondCyril SIX2019-10-071-0/+17
* ItailcallCyril SIX2019-10-071-0/+9
* IreturnCyril SIX2019-10-071-1/+5
* Ibuiltin proofCyril SIX2019-10-041-0/+24
* IcallCyril SIX2019-10-031-0/+19
* Iload and IstoreCyril SIX2019-10-031-0/+24
* Proof for IopCyril SIX2019-10-031-1/+13
* Duplicate - Proof of verificator for InopCyril SIX2019-10-031-1/+2
* Starting implementing the verificatorCyril SIX2019-10-021-0/+33
* Proof of first axiomCyril SIX2019-09-111-3/+15
* Fixing Linking problemCyril SIX2019-09-111-15/+15
* Utilisation d'un intermédiaire xfunction contenant le revmapCyril SIX2019-09-111-13/+33
* Duplicate: big progress on step_simulation, only Ijumptbl leftCyril SIX2019-09-051-10/+9
* Duplicate: exec_function_internalCyril SIX2019-09-041-0/+9
* transf_initial_statesCyril SIX2019-09-041-7/+16
* Stubs for Duplicate passCyril SIX2019-09-031-0/+31
generated by cgit (git 2.34.1) at 2024-05-09 09:54:13 +0000