package goblint

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

Address set lattice.

  • parameter Mval

    mvalue used in addresses.

  • parameter ID

    integers used for conversions.

Parameters

module ID : IntDomain.Z

Signature

module Addr : sig ... end
include SetDomain.S with type elt = Addr.t
include Lattice.S
include Lattice.PO
include Printable.S
type t
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val show : t -> string
val pretty : unit -> t -> Printable.Pretty.doc
val printXml : 'a BatInnerIO.output -> t -> unit
val name : unit -> string
val to_yojson : t -> Yojson.Safe.t
val tag : t -> int

Unique ID, given by HConsed, for context identification in witness

val arbitrary : unit -> t QCheck.arbitrary
val relift : t -> t
val leq : t -> t -> bool
val join : t -> t -> t
val meet : t -> t -> t
val widen : t -> t -> t

widen x y assumes leq x y. Solvers guarantee this by calling widen old (join old new).

val narrow : t -> t -> t
val pretty_diff : unit -> (t * t) -> Lattice.Pretty.doc

If leq x y = false, then pretty_diff () (x, y) should explain why.

val bot : unit -> t
val is_bot : t -> bool
val top : unit -> t
val is_top : t -> bool
type elt = Addr.t
val empty : unit -> t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t

See Set.S.remove.

NB! On set abstractions this is a strong removal, i.e. all subsumed elements are also removed.

val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t

See Set.S.diff.

NB! On set abstractions this is a strong removal, i.e. all subsumed elements are also removed.

val subset : t -> t -> bool
val disjoint : t -> t -> bool
val iter : (elt -> unit) -> t -> unit

See Set.S.iter.

On set abstractions this iterates only over canonical elements, not all subsumed elements.

val map : (elt -> elt) -> t -> t

See Set.S.map.

On set abstractions this maps only canonical elements, not all subsumed elements.

val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a

See Set.S.fold.

On set abstractions this folds only over canonical elements, not all subsumed elements.

val for_all : (elt -> bool) -> t -> bool

See Set.S.for_all.

On set abstractions this checks only canonical elements, not all subsumed elements.

val exists : (elt -> bool) -> t -> bool

See Set.S.exists.

On set abstractions this checks only canonical elements, not all subsumed elements.

val filter : (elt -> bool) -> t -> t

See Set.S.filter.

On set abstractions this filters only canonical elements, not all subsumed elements.

val partition : (elt -> bool) -> t -> t * t

See Set.S.partition.

On set abstractions this partitions only canonical elements, not all subsumed elements.

val cardinal : t -> int

See Set.S.cardinal.

On set abstractions this counts only canonical elements, not all subsumed elements.

val elements : t -> elt list

See Set.S.elements.

On set abstractions this lists only canonical elements, not all subsumed elements.

val of_list : elt list -> t
val min_elt : t -> elt

See Set.S.min_elt.

On set abstractions this chooses only a canonical element, not any subsumed element.

val max_elt : t -> elt

See Set.S.max_elt.

On set abstractions this chooses only a canonical element, not any subsumed element.

val choose : t -> elt

See Set.S.choose.

On set abstractions this chooses only a canonical element, not any subsumed element.

val null_ptr : t

Address set containing only the NULL pointer.

val unknown_ptr : t

Address set containing the unknown pointer, which is non-NULL.

val not_null : t

Address set containing the unknown pointer, which is non-NULL.

val top_ptr : t

Address set containing any pointer, NULL or not.

val is_null : t -> bool

Whether address set contains only the NULL pointer.

val is_not_null : t -> bool

Whether address set does not contain the NULL pointer.

val may_be_null : t -> bool

Whether address set contains the NULL pointer.

val may_be_unknown : t -> bool

Whether address set contains the unknown pointer.

val is_definite : t -> bool

Whether address set is a single NULL pointer or mvalue that has only definite integer indexing (and fields).

val is_element : Addr.t -> t -> bool

Whether address set contains only the given address.

val of_var : GoblintCil.varinfo -> t

Convert from variable (without offset).

val of_mval : Mval.t -> t

Convert from mvalue.

val of_int : ID.t -> t

Convert from integer.

val to_var_may : t -> GoblintCil.varinfo list

Convert to variables with any offset.

val to_var_must : t -> GoblintCil.varinfo list

Convert to variables without offset.

val to_mval : t -> Mval.t list

Convert to mvalues.

val to_int : t -> ID.t

Convert to integer.

val to_bool : t -> bool option

Convert to boolean if possible.

val type_of : t -> GoblintCil.typ

Type of address set.

val of_string : string -> t

Convert from string literal.

val to_string : t -> string list

Convert to string literals.

val to_string_length : t -> ID.t

Find length of C string.

val substring_extraction : t -> t -> t
val string_comparison : t -> t -> int option -> ID.t
val string_writing_defined : t -> 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