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, 2 insertions, 1 deletions
diff --git a/backend/FirstNop.v b/backend/FirstNop.v
index b3c765e4..f921114b 100644
--- a/backend/FirstNop.v
+++ b/backend/FirstNop.v
@@ -20,7 +20,8 @@ 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_entrypoint := start_pc;
+ fn_untrusted_analysis := mkuntrustedanalysis None None |}.
Definition transf_fundef (fd: fundef) : fundef :=
AST.transf_fundef transf_function fd.