From d7213cfdef90fc3ebc5f57ae18277d7b4c9dd126 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 8 Dec 2020 20:16:47 +0100 Subject: analysis with Abst_same --- backend/CSE3analysisproof.v | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'backend/CSE3analysisproof.v') diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 7e456748..10ffe760 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1298,7 +1298,10 @@ Section SOUNDNESS. PTree.get pc (fn_code fn) = Some instr -> In pc' (successors_instr instr) -> RB.ge (PMap.get pc' inv) - (apply_instr' (ctx:=ctx) tenv (fn_code fn) pc (PMap.get pc inv)). + (match apply_instr' (ctx:=ctx) tenv (fn_code fn) pc + (PMap.get pc inv) with + | Abst_same rel' => rel' + end). Definition is_inductive_allstep := forall pc pc', is_inductive_step pc pc'. @@ -1317,11 +1320,14 @@ Section SOUNDNESS. pose proof (ALL INSTR) as AT_PC. destruct (inv # pc). 2: apply RB.ge_bot. - rewrite List.forallb_forall in AT_PC. unfold apply_instr'. rewrite INSTR. - apply relb_leb_correct. - auto. + destruct apply_instr. + { (* same *) + rewrite List.forallb_forall in AT_PC. + apply relb_leb_correct. + auto. + } Qed. Lemma checked_is_inductive_entry: -- cgit