diff --git a/src/cdomain/value/cdomains/stringDomain.ml b/src/cdomain/value/cdomains/stringDomain.ml index 2b968b0321..8ab5cd384a 100644 --- a/src/cdomain/value/cdomains/stringDomain.ml +++ b/src/cdomain/value/cdomains/stringDomain.ml @@ -72,7 +72,7 @@ let to_string_length x = let to_exp = function | Some x -> GoblintCil.mkString x - | None -> raise (Lattice.Unsupported "Cannot express unknown string pointer as expression.") + | None -> failwith "Cannot express unknown string pointer as expression." let semantic_equal x y = match x, y with diff --git a/src/cdomains/stackDomain.ml b/src/cdomains/stackDomain.ml index 50864d6294..5a5168e22c 100644 --- a/src/cdomains/stackDomain.ml +++ b/src/cdomains/stackDomain.ml @@ -13,14 +13,14 @@ struct let n = 3 let rec times x = function 0 -> [] | n -> x::times x (n-1) let rec map2 f xs ys = - match xs, ys with x::xs, y::ys -> (try f x y :: map2 f xs ys with Lattice.Unsupported _ -> []) | _ -> [] + match xs, ys with x::xs, y::ys -> (try f x y :: map2 f xs ys with Lattice.BotValue | Lattice.TopValue -> []) | _ -> [] let rec fold_left2 f a b xs ys = match xs, ys with | [], _ | _, [] -> a | x::xs, y::ys -> try fold_left2 f (f a x y) b xs ys with - | Lattice.Unsupported _ -> b + | Lattice.BotValue | Lattice.TopValue -> b let rec take n xs = match n, xs with diff --git a/src/domain/lattice.ml b/src/domain/lattice.ml index cc72dd5be0..71a130573f 100644 --- a/src/domain/lattice.ml +++ b/src/domain/lattice.ml @@ -45,9 +45,6 @@ exception BotValue (** Exception raised by a bottomless lattice in place of a bottom value. Surrounding lattice functors may handle this on their own. *) -exception Unsupported of string -let unsupported x = raise (Unsupported x) - exception Invalid_widen of Pretty.doc let () = Printexc.register_printer (function @@ -93,10 +90,10 @@ struct include Base let leq = equal let join x y = - if equal x y then x else raise (Unsupported "fake join") (* TODO: TopValue? *) + if equal x y then x else raise TopValue let widen = join let meet x y = - if equal x y then x else raise (Unsupported "fake meet") (* TODO: BotValue? *) + if equal x y then x else raise BotValue let narrow = meet include NoBotTop @@ -394,11 +391,11 @@ struct | (x, `Bot) -> x | (`Lifted1 x, `Lifted1 y) -> begin try `Lifted1 (Base1.join x y) - with Unsupported _ | TopValue -> `Top + with TopValue -> `Top end | (`Lifted2 x, `Lifted2 y) -> begin try `Lifted2 (Base2.join x y) - with Unsupported _ | TopValue -> `Top + with TopValue -> `Top end | _ -> `Top @@ -410,11 +407,11 @@ struct | (x, `Top) -> x | (`Lifted1 x, `Lifted1 y) -> begin try `Lifted1 (Base1.meet x y) - with Unsupported _ | BotValue -> `Bot + with BotValue -> `Bot end | (`Lifted2 x, `Lifted2 y) -> begin try `Lifted2 (Base2.meet x y) - with Unsupported _ | BotValue -> `Bot + with BotValue -> `Bot end | _ -> `Bot @@ -581,10 +578,7 @@ end module Liszt (Base: S) = struct include Printable.Liszt (Base) - let bot () = raise (Unsupported "bot?") - let is_top _ = false - let top () = raise (Unsupported "top?") - let is_bot _ = false + include NoBotTop let leq = let f acc x y = Base.leq x y && acc in diff --git a/src/domain/mapDomain.ml b/src/domain/mapDomain.ml index a62fcb98e4..033302d8df 100644 --- a/src/domain/mapDomain.ml +++ b/src/domain/mapDomain.ml @@ -398,7 +398,7 @@ struct let leq = leq_with_fct Range.leq let find x m = try find x m with | Not_found -> Range.bot () - let top () = Lattice.unsupported "partial map top" + let top () = raise Lattice.TopValue let bot () = empty () let is_top _ = false let is_bot = is_empty @@ -448,7 +448,7 @@ struct let find x m = try find x m with | Not_found -> Range.top () let top () = empty () - let bot () = Lattice.unsupported "partial map bot" + let bot () = raise Lattice.BotValue let is_top = is_empty let is_bot _ = false diff --git a/src/domains/domainProperties.ml b/src/domains/domainProperties.ml index b2f0f7671a..fdf8e7512c 100644 --- a/src/domains/domainProperties.ml +++ b/src/domains/domainProperties.ml @@ -126,7 +126,7 @@ struct with | Failure _ (* raised by IntDomain *) | SetDomain.Unsupported _ (* raised by SetDomain *) - | Lattice.Unsupported _ (* raised by MapDomain *) -> + | Lattice.TopValue (* raised by MapDomain *) -> false let top_leq = make ~name:"top leq" (arb) (fun a -> diff --git a/tests/unit/domains/mapDomainTest.ml b/tests/unit/domains/mapDomainTest.ml index 26b8b6725c..64be44f77e 100644 --- a/tests/unit/domains/mapDomainTest.ml +++ b/tests/unit/domains/mapDomainTest.ml @@ -18,7 +18,7 @@ struct let get_empty () = try (is_empty_top := true; M.top ()) - with Lattice.Unsupported _ | Lattice.BotValue | Lattice.TopValue -> + with Lattice.TopValue -> (is_empty_top := false; M.bot ()) let is_empty x = @@ -44,7 +44,7 @@ struct map := M.remove "key1" !map; begin try ignore (M.find "key1" !map); assert_failure "problem removeing key1" - with Lattice.Unsupported _ | Lattice.BotValue | Lattice.TopValue -> () + with Lattice.BotValue | Lattice.TopValue -> () end ; end