diff options
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 556b44b3..cbc31670 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -914,7 +914,8 @@ Definition transf_function' (f: function) (approxs: PMap.t numbering) : function f.(fn_params) f.(fn_stacksize) (transf_code approxs f.(fn_code)) - f.(fn_entrypoint). + f.(fn_entrypoint) + (mkuntrustedanalysis None None). Definition regs_lessdef (rs1 rs2: regset) : Prop := forall r, Val.lessdef (rs1#r) (rs2#r). |