diff options
Diffstat (limited to 'backend/RTLTunneling.v')
| -rw-r--r-- | backend/RTLTunneling.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v index 878e079f..255aff3c 100644 --- a/backend/RTLTunneling.v +++ b/backend/RTLTunneling.v @@ -109,8 +109,9 @@ Definition tunnel_function (f: RTL.function): res RTL.function := (fn_sig f) (fn_params f) (fn_stacksize f) - (PTree.map1 (tunnel_instr td) c) - (td (fn_entrypoint f))) + (PTree.map1 (tunnel_instr td) c) (* rq: `map1` est un map sans le pointeur *) + (td (fn_entrypoint f)) + (mkuntrustedanalysis None None)) else Error (msg "Some node of the union-find is not in the CFG"). Definition tunnel_fundef (f: fundef): res fundef := |