aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Duplicateproof.v
Commit message (Expand)AuthorAgeFilesLines
* being more archi-independantLéo Gourdin2021-11-021-1/+1
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-19/+13
* remove some useless "OK tt"Sylvain Boulmé2021-01-071-7/+7
* Making verify_mapping_mn_rec tail recursive (should fix arm CI) #231Cyril SIX2021-01-061-1/+1
* DuplicateParam -> DuplicateOracle + simpler DuplicatepassesSylvain Boulmé2020-10-281-1/+1
* Reworked Duplicate to be parametrizedCyril SIX2020-10-271-0/+5
* Adding copyrightsCyril SIX2020-05-041-0/+14
* Adding info field for branching in RTL, LTL, XTL and all associated passesCyril SIX2020-03-111-4/+4
* removing some coqc 8.10 warningsSylvain Boulmé2020-03-091-1/+1
* Revert "Modified the hook for the oracle"Cyril SIX2020-01-231-3/+2
* Verificator finished for handling reversed IcondCyril SIX2020-01-231-5/+9
* Added clause in match_inst to allow Icond reversalCyril SIX2020-01-231-4/+13
* Modified the hook for the oracleCyril SIX2020-01-231-2/+3
* make it compile for ARMDavid Monniaux2019-12-061-4/+4
* finish mergeDavid Monniaux2019-12-021-2/+18
* Duplicateproof: minor editSylvain Boulmé2019-11-261-3/+4
* simplification of Duplicate: remove xfunctionSylvain Boulmé2019-11-141-117/+119
* Merge remote-tracking branch 'origin/mppa-duplicate-rtl-alt' into mppa-workCyril SIX2019-10-241-53/+77
|\
| * An alternative proof where the match_state does not depend on the translationSylvain Boulmé2019-10-231-53/+77
* | eq_condition already existedDavid Monniaux2019-10-161-1/+1
|/
* Finished Duplicate proof.Cyril SIX2019-10-071-35/+40
* IcondCyril SIX2019-10-071-0/+9
* ItailcallCyril SIX2019-10-071-2/+8
* IreturnCyril SIX2019-10-071-0/+4
* Ibuiltin proofCyril SIX2019-10-041-0/+7
* IcallCyril SIX2019-10-031-0/+8
* Iload and IstoreCyril SIX2019-10-031-3/+19
* Proof for IopCyril SIX2019-10-031-0/+7
* Preparing the terrain for the rest of the instructions with one successorCyril SIX2019-10-031-5/+17
* Duplicate - Proof of verificator for InopCyril SIX2019-10-031-3/+81
* Starting implementing the verificatorCyril SIX2019-10-021-1/+1
* Proof of first axiomCyril SIX2019-09-111-1/+10
* Fixing Linking problemCyril SIX2019-09-111-16/+16
* Utilisation d'un intermédiaire xfunction contenant le revmapCyril SIX2019-09-111-34/+48
* Duplicate: proof complete, assuming revmap, revmap_correct and revmap_entrypointCyril SIX2019-09-061-5/+21
* Duplicate: big progress on step_simulation, only Ijumptbl leftCyril SIX2019-09-051-74/+138
* Duplicate: changement de match_nodesCyril SIX2019-09-041-36/+44
* Duplicate: exec_function_external et exec_returnCyril SIX2019-09-041-3/+7
* Duplicate: exec_function_internalCyril SIX2019-09-041-2/+34
* transf_initial_statesCyril SIX2019-09-041-4/+66
* Duplicate: match_statesCyril SIX2019-09-031-2/+10
* Duplicate: match_nodesCyril SIX2019-09-031-8/+57
* Start of match_statesCyril SIX2019-09-031-3/+23
* Stubs for Duplicate passCyril SIX2019-09-031-0/+29
generated by cgit (git 2.34.1) at 2024-05-09 09:58:22 +0000