diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-02 16:00:38 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-02 16:00:38 +0200 |
| commit | 57fce9febbd616becc8f120447de9c40318bcbfa (patch) | |
| tree | 34d5b2eae4b581daaa6a7851911c591a939b5a8c /backend/Duplicateproof.v | |
| parent | c22d994917d6a67efc065c1205ede4d448445c10 (diff) | |
| download | compcert-kvx-57fce9febbd616becc8f120447de9c40318bcbfa.tar.gz compcert-kvx-57fce9febbd616becc8f120447de9c40318bcbfa.zip | |
Starting implementing the verificator
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index fe26db55..4ffd2c5d 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -41,7 +41,7 @@ Inductive match_inst (is_copy: node -> option node): instruction -> instruction Axiom revmap_correct: forall f xf n n', transf_function_aux f = OK xf -> (fn_revmap xf)!n' = Some n -> - (forall i, (fn_code f)!n = Some i -> exists i', (fn_code (fn_RTL xf))!n' = Some i' /\ match_inst (fun n => (fn_revmap xf)!n) i i'). + (forall i, (fn_code f)!n = Some i -> exists i', (fn_code (fn_RTL xf))!n' = Some i' /\ match_inst (fun n' => (fn_revmap xf)!n') i i'). Theorem revmap_entrypoint: forall f xf, transf_function_aux f = OK xf -> (fn_revmap xf)!(fn_entrypoint (fn_RTL xf)) = Some (fn_entrypoint f). |