diff options
Diffstat (limited to 'backend/Constprop.v')
| -rw-r--r-- | backend/Constprop.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/backend/Constprop.v b/backend/Constprop.v index a3e432c0..0be9438c 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -247,8 +247,7 @@ Definition transf_function (rm: romem) (f: function) : function := f.(fn_params) f.(fn_stacksize) (PTree.map (transf_instr f an rm) f.(fn_code)) - f.(fn_entrypoint) - (mkuntrustedanalysis None None). + f.(fn_entrypoint). Definition transf_fundef (rm: romem) (fd: fundef) : fundef := AST.transf_fundef (transf_function rm) fd. |