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