aboutsummaryrefslogtreecommitdiffstats
path: root/backend/ForwardMoves.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/ForwardMoves.v')
-rw-r--r--backend/ForwardMoves.v3
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 1b375532..d42d1d17 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -335,7 +335,8 @@ Definition transf_function (f: function) : function :=
fn_params := f.(fn_params);
fn_stacksize := f.(fn_stacksize);
fn_code := PTree.map (transf_instr (forward_map f)) f.(fn_code);
- fn_entrypoint := f.(fn_entrypoint) |}.
+ fn_entrypoint := f.(fn_entrypoint);
+ fn_untrusted_analysis := mkuntrustedanalysis None None |}.
Definition transf_fundef (fd: fundef) : fundef :=