From 60923ea18f414a2d609497f2f1f03b136d9bb3d0 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Tue, 21 Nov 2023 20:15:31 +0200 Subject: [PATCH] Special function lval not invalidated recursively --- src/analyses/base.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 84be8c7a19..8b6350aa2d 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2123,7 +2123,7 @@ struct let invalidate_ret_lv st = match lv with | Some lv -> if M.tracing then M.tracel "invalidate" "Invalidating lhs %a for function call %s\n" d_plainlval lv f.vname; - invalidate ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv] + invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv] | None -> st in let addr_type_of_exp exp = @@ -2328,7 +2328,7 @@ struct | _ -> failwith ("non-floating-point argument in call to function "^f.vname) end in - let apply_abs ik x = +let apply_abs ik x = let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in begin match eval_x with | Int int_x ->