From d456248687f059d822dc4bb18639137632a6745e Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Sat, 28 Sep 2024 18:39:40 +0100 Subject: [PATCH] put VIP typing check under the vip switch --- backend/cn/lib/check.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index 6d7aa81a0..9f0761020 100644 --- a/backend/cn/lib/check.ml +++ b/backend/cn/lib/check.ml @@ -422,13 +422,16 @@ let check_against_core_bt loc msg2 cbt bt = let check_has_alloc_id loc ptr ub_unspec = - let@ provable = provable loc in - match provable (LC.T (hasAllocId_ ptr loc)) with - | `True -> return () - | `False -> - let@ model = model () in - let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in - fail (fun ctxt -> { loc; msg = Needs_alloc_id { ptr; ub; ctxt; model } }) + if !use_vip then + let@ provable = provable loc in + match provable (LC.T (hasAllocId_ ptr loc)) with + | `True -> return () + | `False -> + let@ model = model () in + let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in + fail (fun ctxt -> { loc; msg = Needs_alloc_id { ptr; ub; ctxt; model } }) + else + return () let check_alloc_bounds loc ~ptr ub_unspec =