From 3bac7c653af570889c9214047b1bb7186e9b8eb8 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Wed, 25 Sep 2024 13:00:43 +0100 Subject: [PATCH] CN VIP: Clarify pointer to int --- backend/cn/lib/check.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index d4936b4ff..751ff39bf 100644 --- a/backend/cn/lib/check.ml +++ b/backend/cn/lib/check.ml @@ -1423,7 +1423,12 @@ let rec check_expr labels (e : BT.t Mu.mu_expr) (k : IT.t -> unit m) : unit m = let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in check_pexpr pe (fun arg -> let actual_value = cast_ (Memory.bt_of_sct act_to.ct) arg loc in - (* after discussing with Kavyan *) + (* NOTE: After discussing with Kavyan + (1) The pointer does NOT need to be live. The PNVI/VIP + formalisations are missing a rule for the dead pointer case. + The PNVI rules state that the pointer must be live so that + allocations are exposed. + (2) So, the only UB possible is unrepresentable results. *) let@ provable = provable loc in let here = Locations.other __FUNCTION__ in let lc = LC.T (representable_ (act_to.ct, arg) here) in