package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
(** Boolean domains. *)

module type Names =
sig
  val name: string
  val true_name: string
  val false_name: string
end

module MakeBool (Names: Names) =
struct
  include Printable.StdLeaf
  type t = bool [@@deriving eq, ord, hash]
  let name () = Names.name

  let show x = if x then Names.true_name else Names.false_name
  include Printable.SimpleShow (struct
      type nonrec t = t
      let show = show
    end)

  let arbitrary () = QCheck.bool

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

module StdNames: Names =
struct
  let name = "bool"
  let true_name = "true"
  let false_name = "false"
end

module Bool =
struct
  include MakeBool (StdNames)
  let to_yojson = [%to_yojson: bool] (* override to_yojson from SimpleShow *)
end

module MakeMayBool (Names: Names): Lattice.S with type t = bool =
struct
  include MakeBool (Names)
  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 MayBool: Lattice.S with type t = bool =
struct
  include MakeMayBool (StdNames)
  let to_yojson = [%to_yojson: bool] (* override to_yojson from SimpleShow *)
end

(* TODO: MakeMustBool? *)

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)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct