Skip to content

Commit 4d3d8e3

Browse files
committed
Fix lval type in base entire var refinement
The entire var is refined, but update_offset goes deeper into fields.
1 parent 3014833 commit 4d3d8e3

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/analyses/baseInvariant.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ struct
103103
let old_val = get_var ~man st var in
104104
let old_val = map_oldval old_val var.vtype in
105105
let offs = convert_offset ~man st o in
106-
let new_val = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) old_val offs c' (Some exp) x (var.vtype) in
106+
let new_val = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) old_val offs c' (Some exp) x (Cilfacade.typeOfLval x) in
107107
let v = apply_invariant ~old_val ~new_val in
108108
if is_some_bot v then contra st
109109
else (

0 commit comments

Comments
 (0)