diff options
Diffstat (limited to 'backend/Duplicate.v')
| -rw-r--r-- | backend/Duplicate.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 3fd86728..a3c65acc 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -219,7 +219,7 @@ Definition verify_mapping dupmap (f f': function) : res unit := Definition transf_function (f: function) : res function := let (tcte, dupmap) := duplicate_aux f in let (tc, te) := tcte in - let f' := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in + let f' := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te (mkuntrustedanalysis None None) in do u <- verify_mapping dupmap f f'; OK f'. |