diff options
Diffstat (limited to 'backend/CSE3.v')
| -rw-r--r-- | backend/CSE3.v | 12 |
1 files changed, 11 insertions, 1 deletions
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. |