Skip to content

Commit

Permalink
Let meet in UnionDomain.Map throw Uncomparable in case different fiel…
Browse files Browse the repository at this point in the history
…ds are set.

Fixes an issue where meet in branch refinement yielded bot on unions where different fields were set.
  • Loading branch information
jerhard committed Nov 28, 2023
1 parent 18a87f6 commit ae1204d
Showing 1 changed file with 10 additions and 0 deletions.
10 changes: 10 additions & 0 deletions src/cdomains/unionDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -192,6 +192,16 @@ struct
let join =
Map.join

let meet a b =
if a == b then
a
else
let merge_pair _ x y = match x, y with
| Some x, Some y -> Some (Values.meet x y)
| _, _ -> raise Lattice.Uncomparable
in
Map.merge merge_pair a b

(** Performs join or widen operation using per element merge function *)
let merge ~merge_values x y =
if is_top x || is_top y then
Expand Down

0 comments on commit ae1204d

Please sign in to comment.