We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 9f1e5f9 commit 91388efCopy full SHA for 91388ef
src/analyses/base.ml
@@ -1411,9 +1411,13 @@ struct
1411
let new_value = VD.update_offset (Queries.to_value_domain_ask a) old_value offs projected_value lval_raw ((Var x), cil_offset) t in
1412
if WeakUpdates.mem x st.weak then
1413
VD.join old_value new_value
1414
- else if invariant then
+ else if invariant then (
1415
(* without this, invariant for ambiguous pointer might worsen precision for each individual address to their join *)
1416
- VD.meet old_value new_value
+ try
1417
+ VD.meet old_value new_value
1418
+ with Lattice.Uncomparable ->
1419
+ new_value
1420
+ )
1421
else
1422
new_value
1423
in
0 commit comments