aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.vexpand4
1 files changed, 3 insertions, 1 deletions
diff --git a/extraction/extraction.vexpand b/extraction/extraction.vexpand
index 568b1b46..55ca3b5c 100644
--- a/extraction/extraction.vexpand
+++ b/extraction/extraction.vexpand
@@ -130,6 +130,8 @@ Extract Constant Compopts.optim_CSE3_glb =>
"fun _ -> !Clflags.option_fcse3_glb".
Extract Constant Compopts.optim_CSE3_trivial_ops =>
"fun _ -> !Clflags.option_fcse3_trivial_ops".
+Extract Constant Compopts.optim_CSE3_conditions =>
+ "fun _ -> !Clflags.option_fcse3_conditions".
Extract Constant Compopts.optim_move_loop_invariants =>
"fun _ -> !Clflags.option_fmove_loop_invariants".
@@ -223,7 +225,7 @@ Cd "extraction".
Separate Extraction
Z.ldiff Z.lnot Nat.leb
- CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem
+ CSE3analysis.eq_cond_depends_on_mem CSE3analysis.apply_instr'
Compiler.transf_c_program Compiler.transf_cminor_program
Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env