Skip to content

Commit

Permalink
propagate bottom through narrowing operator of lifters
Browse files Browse the repository at this point in the history
  • Loading branch information
Red-Panda64 committed Jul 11, 2024
1 parent b8a5bb9 commit a23b728
Showing 1 changed file with 8 additions and 0 deletions.
8 changes: 8 additions & 0 deletions src/domain/lattice.ml
Original file line number Diff line number Diff line change
Expand Up @@ -277,6 +277,8 @@ struct
let narrow x y =
match (x,y) with
| (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
| (_, `Bot) -> `Bot
| (`Top, y) -> y
| _ -> x
end

Expand Down Expand Up @@ -337,6 +339,8 @@ struct
| (`Lifted x, `Lifted y) ->
(try `Lifted (Base.narrow x y)
with Uncomparable -> `Bot)
| (_, `Bot) -> `Bot
| (`Top, y) -> y
| _ -> x
end

Expand Down Expand Up @@ -408,6 +412,8 @@ struct
match (x,y) with
| (`Lifted1 x, `Lifted1 y) -> `Lifted1 (Base1.narrow x y)
| (`Lifted2 x, `Lifted2 y) -> `Lifted2 (Base2.narrow x y)
| (_, `Bot) -> `Bot
| (`Top, y) -> y
| _ -> x

end
Expand Down Expand Up @@ -539,6 +545,7 @@ struct
let narrow x y =
match (x,y) with
| (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
| (_, `Bot) -> `Bot
| _ -> x
end

Expand Down Expand Up @@ -580,6 +587,7 @@ struct
let narrow x y =
match (x,y) with
| (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
| (`Top, y) -> y
| _ -> x

let pretty_diff () (x,y) =
Expand Down

0 comments on commit a23b728

Please sign in to comment.