aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Deadcode.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Deadcode.v')
-rw-r--r--backend/Deadcode.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index 719120ab..3412a6fa 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -206,8 +206,7 @@ Definition transf_function (rm: romem) (f: function) : res function :=
fn_params := f.(fn_params);
fn_stacksize := f.(fn_stacksize);
fn_code := PTree.map (transf_instr approx an) f.(fn_code);
- fn_entrypoint := f.(fn_entrypoint);
- fn_untrusted_analysis := mkuntrustedanalysis None None |}
+ fn_entrypoint := f.(fn_entrypoint) |}
| None =>
Error (msg "Neededness analysis failed")
end.