Source file `boolDomain.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
(** Boolean domains. *)

module Bool =
struct
  include Basetype.RawBools
  (* type t = bool
     let equal = Bool.equal
     let compare = Bool.compare
     let relift x = x
     let arbitrary () = QCheck.bool *)

  let pretty_diff () (x,y) = GoblintCil.Pretty.dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
end

module MayBool: Lattice.S with type t = bool =
struct
  include Bool
  let bot () = false
  let is_bot x = x = false
  let top () = true
  let is_top x = x = true
  let leq x y = x == y || y
  let join = (||)
  let widen = (||)
  let meet = (&&)
  let narrow = (&&)
end

module MustBool: Lattice.S with type t = bool =
struct
  include Bool
  let bot () = true
  let is_bot x = x = true
  let top () = false
  let is_top x = x = false
  let leq x y = x == y || x
  let join = (&&)
  let widen = (&&)
  let meet = (||)
  let narrow = (||)
end

module FlatBool: Lattice.S with type t = [`Bot | `Lifted of bool | `Top] =
  Lattice.FlatConf (struct
    include Printable.DefaultConf
    let top_name = "?"
    let bot_name = "-"
  end) (Bool)