Skip to content

Commit 60923ea

Browse files
committed
Special function lval not invalidated recursively
1 parent 3485100 commit 60923ea

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/analyses/base.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2123,7 +2123,7 @@ struct
21232123
let invalidate_ret_lv st = match lv with
21242124
| Some lv ->
21252125
if M.tracing then M.tracel "invalidate" "Invalidating lhs %a for function call %s\n" d_plainlval lv f.vname;
2126-
invalidate ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv]
2126+
invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv]
21272127
| None -> st
21282128
in
21292129
let addr_type_of_exp exp =
@@ -2328,7 +2328,7 @@ struct
23282328
| _ -> failwith ("non-floating-point argument in call to function "^f.vname)
23292329
end
23302330
in
2331-
let apply_abs ik x =
2331+
let apply_abs ik x =
23322332
let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in
23332333
begin match eval_x with
23342334
| Int int_x ->

0 commit comments

Comments
 (0)