From 7b34d3c03fea76b85ec72d5ee82c53353960e2b2 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 16 Jul 2021 21:11:34 +0200
Subject: make CSE3 condition parametric

---
 backend/CSE3.v | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'backend/CSE3.v')

diff --git a/backend/CSE3.v b/backend/CSE3.v
index 746ba399..5d05821a 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -20,6 +20,14 @@ Local Open Scope error_monad_scope.
 
 Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints.
 
+Record cse3params : Type :=
+  mkcse3params
+    { cse3_conditions : bool;
+    }.
+
+Section PARAMS.
+  Variable params : cse3params.
+
 Section REWRITE.
   Context {ctx : eq_context}.
 
@@ -54,7 +62,7 @@ Definition subst_args fmap pc xl :=
   forward_move_l_b (PMap.get pc fmap) xl.
 
 Definition find_cond_in_fmap fmap pc cond args :=
-  if Compopts.optim_CSE3_conditions tt
+  if cse3_conditions params
   then
     match PMap.get pc fmap with
     | Some rel =>
@@ -129,3 +137,5 @@ Definition transf_fundef (fd: fundef) : res fundef :=
 
 Definition transf_program (p: program) : res program :=
   transform_partial_program transf_fundef p.
+
+End PARAMS.
-- 
cgit