aboutsummaryrefslogtreecommitdiffstats
path: root/backend/FirstNop.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/FirstNop.v')
-rw-r--r--backend/FirstNop.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/backend/FirstNop.v b/backend/FirstNop.v
index f921114b..b3c765e4 100644
--- a/backend/FirstNop.v
+++ b/backend/FirstNop.v
@@ -20,8 +20,7 @@ Definition transf_function (f: function) : function :=
fn_params := f.(fn_params);
fn_stacksize := f.(fn_stacksize);
fn_code := PTree.set start_pc (Inop f.(fn_entrypoint)) f.(fn_code);
- fn_entrypoint := start_pc;
- fn_untrusted_analysis := mkuntrustedanalysis None None |}.
+ fn_entrypoint := start_pc |}.
Definition transf_fundef (fd: fundef) : fundef :=
AST.transf_fundef transf_function fd.