diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-07-16 20:47:25 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-07-16 20:47:25 +0200 |
| commit | e11b548d94b247b5359960b8d31027b53ee0dffc (patch) | |
| tree | 094678822bb8dfd4fcc748f225736a43a4b03ff4 /backend | |
| parent | 51668ba258e7b79a1b2b129a404b1eb9981e8e3b (diff) | |
| download | compcert-kvx-e11b548d94b247b5359960b8d31027b53ee0dffc.tar.gz compcert-kvx-e11b548d94b247b5359960b8d31027b53ee0dffc.zip | |
rm condition parametrization in CSE3analysis
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CSE3analysis.v | 7 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 12 |
2 files changed, 6 insertions, 13 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 75e00f67..9a6c9c0d 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -477,13 +477,10 @@ Section OPERATIONS. end. Definition apply_cond cond args (rel : RELATION.t) : RB.t := - if Compopts.optim_CSE3_conditions tt - then - match apply_cond1 cond args rel with + match apply_cond1 cond args rel with | Some rel => Some (apply_cond0 cond args rel) | None => RB.bot - end - else Some rel. + end. Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) := match instr with diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 382c9f4c..523b52df 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1350,14 +1350,10 @@ Section SOUNDNESS. Proof. unfold apply_cond. intros. - destruct (Compopts.optim_CSE3_conditions tt). - { - pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1. - destruct apply_cond1 eqn:COND1. - { apply apply_cond0_sound; auto. } - exact SOUND1. - } - exact REL. + pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1. + destruct apply_cond1 eqn:COND1. + { apply apply_cond0_sound; auto. } + exact SOUND1. Qed. (* |