diff options
Diffstat (limited to 'backend/CSE.v')
| -rw-r--r-- | backend/CSE.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index 838d96a6..432751d2 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -572,7 +572,8 @@ Definition transf_function (rm: romem) (f: function) : res function := f.(fn_params) f.(fn_stacksize) (transf_code approxs f.(fn_code)) - f.(fn_entrypoint)) + f.(fn_entrypoint) + (mkuntrustedanalysis None None)) end. Definition transf_fundef (rm: romem) (f: fundef) : res fundef := |