package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-2.5.0.tbz
sha256=452d8491527aea21f2cbb11defcc14ba0daf9fdb6bdb9fc0af73e56eac57b916
sha512=1993cd45c4c7fe124ca6e157f07d17ec50fab5611b270a434ed1b7fb2910aa85a8e6eaaa77dad770430710aafb2f6d676c774dd33942d921f23e2f9854486551
doc/src/goblint.domain/boolDomain.ml.html
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)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>