diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-08 20:16:47 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-08 20:28:00 +0100 |
| commit | d7213cfdef90fc3ebc5f57ae18277d7b4c9dd126 (patch) | |
| tree | 32f5adae832bb34a9dd25c7a7c34fe11208c1c7e /backend/CSE3analysisproof.v | |
| parent | 0f9018baabe8feeed19d8f7e14f8480e898b5a84 (diff) | |
| download | compcert-kvx-d7213cfdef90fc3ebc5f57ae18277d7b4c9dd126.tar.gz compcert-kvx-d7213cfdef90fc3ebc5f57ae18277d7b4c9dd126.zip | |
analysis with Abst_same
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 14 |
1 files changed, 10 insertions, 4 deletions
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: |