Skip to content

Commit e2ee995

Browse files
committed
Fix var_eq assume removing lval
1 parent d22f333 commit e2ee995

File tree

1 file changed

+9
-5
lines changed

1 file changed

+9
-5
lines changed

src/analyses/varEq.ml

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -356,7 +356,6 @@ struct
356356
| StartOf (Var v,_) -> Some (ask.f (Queries.IsMultiple v)) (* Taking an address of a global is fine*)
357357
| StartOf lv -> Some false (* TODO: sound?! *)
358358

359-
(* Set given lval equal to the result of given expression. On doubt do nothing. *)
360359
let add_eq ask (lv:lval) (rv:Exp.t) st =
361360
let lvt = unrollType @@ Cilfacade.typeOfLval lv in
362361
if M.tracing then (
@@ -369,8 +368,8 @@ struct
369368
&& interesting rv
370369
&& is_global_var ask rv = Some false
371370
&& (isIntegralType lvt || isPointerType lvt)
372-
then D.add_eq (rv,Lval lv) (remove ask lv st)
373-
else remove ask lv st
371+
then D.add_eq (rv,Lval lv) st
372+
else st
374373
(* in
375374
match rv with
376375
| Lval rlval -> begin
@@ -384,6 +383,11 @@ struct
384383
end
385384
| _ -> st
386385
*)
386+
387+
(* Set given lval equal to the result of given expression. On doubt do nothing. *)
388+
let assign_eq ask lv rv st =
389+
add_eq ask lv rv (remove ask lv st)
390+
387391
(* Give the set of reachables from argument. *)
388392
let reachables ~deep (ask: Queries.ask) es =
389393
let reachable acc e =
@@ -428,7 +432,7 @@ struct
428432
(* removes all equalities with lval and then tries to make a new one: lval=rval *)
429433
let assign man (lval:lval) (rval:exp) : D.t =
430434
let rval = constFold true (stripCasts rval) in
431-
add_eq (Analyses.ask_of_man man) lval rval man.local
435+
assign_eq (Analyses.ask_of_man man) lval rval man.local
432436

433437
(* First assign arguments to parameters. Then join it with reachables, to get
434438
rid of equalities that are not reachable. *)
@@ -440,7 +444,7 @@ struct
440444
in
441445
let assign_one_param st lv exp =
442446
let rm = remove (Analyses.ask_of_man man) (Var lv, NoOffset) st in
443-
add_eq (Analyses.ask_of_man man) (Var lv, NoOffset) exp rm
447+
assign_eq (Analyses.ask_of_man man) (Var lv, NoOffset) exp rm
444448
in
445449
let nst =
446450
try fold_left2 assign_one_param man.local f.sformals args

0 commit comments

Comments
 (0)