package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

Dune Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (8)

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. R
    Ralf Vogler
  6. K
    Kalmer Apinis
  7. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>

Sources

goblint-2.0.0.tbz
sha256=2f4f2e25b765452f0e336941f35f6cb396d7c213a2d347abe5d35febc5159b1f
sha512=e96af4cad91f6985c8db93c194925853e96cad0ec1a0d9f4d32bbe16d3e5fa1e305f54be02839f21ba89ad2af0c2d5d7aa819ade221ce097dc4dbd0fcd8c8500

doc/goblint.lib/Goblint_lib/AddressDomain/AddressSet/index.html

Module AddressDomain.AddressSet

Parameters

module Idx : IntDomain.Z

Signature

include module type of struct include Printable.Std end
type group = Printable.Std.group = |
val show_group : group -> 'a
val to_group : 'a -> 'b option
val trace_enabled : bool
val tag : 'a -> 'b
val arbitrary : unit -> 'a
val relift : 'a -> 'a
module Addr : sig ... end
include sig ... end
type bucket = Addr.t list
module Map = Batteries.Map.Int
module B : sig ... end
val elements : 'a list Map.t -> 'a list
val merge_meet : ('a -> 'b -> 'c) -> 'b list Map.t -> 'a list Map.t -> 'c list Map.t
val merge_widen : (Addr.t -> Addr.t -> Addr.t) -> Addr.t list Map.t -> Addr.t list Map.t -> Addr.t list Map.t
val merge_join : (Addr.t -> Addr.t -> Addr.t) -> Addr.t list Map.t -> Addr.t list Map.t -> Addr.t list Map.t
val join : Addr.t list Map.t -> Addr.t list Map.t -> Addr.t list Map.t
val of_list_by : (Addr.t -> Addr.t -> Addr.t) -> Addr.t list -> Addr.t list Map.t
val of_list : Addr.t list -> Addr.t list Map.t
val singleton : Addr.t -> Addr.t list Map.t
val exists : ('a -> bool) -> 'a list Map.t -> bool
val for_all : ('a -> bool) -> 'a list Map.t -> bool
val mem : Addr.t -> Addr.t list Map.t -> bool
val choose : 'a list Map.t -> 'a
val apply_list : ('a list -> Addr.t list) -> 'a list Map.t -> Addr.t list Map.t
val map : ('a -> Addr.t) -> 'a list Map.t -> Addr.t list Map.t
val filter : (Addr.t -> bool) -> Addr.t list Map.t -> Addr.t list Map.t
val remove : Addr.t -> Addr.t list Map.t -> Addr.t list Map.t
val add : Addr.t -> Addr.t list Map.t -> Addr.t list Map.t
val fold : ('a -> 'b -> 'b) -> 'a list Map.t -> 'b -> 'b
val cardinal : 'a list Map.t -> int
val diff : Addr.t list Map.t -> Addr.t list Map.t -> Addr.t list Map.t
val empty : unit -> 'a Map.t
val is_empty : 'a Map.t -> bool
val union : Addr.t list Map.t -> Addr.t list Map.t -> Addr.t list Map.t
val iter : ('a -> unit) -> 'a list Map.t -> unit
val is_element : 'a -> 'a list Map.t -> bool
val bot : unit -> 'a Map.t
val is_bot : 'a Map.t -> bool
val top : unit -> 'a
val leq : Addr.t list Map.t -> Addr.t list Map.t -> bool
val name : unit -> string
val equal : Addr.t list Map.t -> Addr.t list Map.t -> bool
val hash : Addr.t list Map.t -> int
val compare : Addr.t list Map.t -> Addr.t list Map.t -> int
val to_yojson : Addr.t list Map.t -> [> `List of Yojson.Safe.t list ]
val pretty_diff : unit -> (t * t) -> Goblint_lib__HoareDomain.Pretty.doc
val printXml : 'a BatInnerIO.output -> Addr.t list Map.t -> unit
val widen : Addr.t list Map.t -> Addr.t list Map.t -> Addr.t list Map.t
type field = Addr.field
type idx = Idx.t
type offs = [
  1. | `NoOffset
  2. | `Field of field * offs
  3. | `Index of idx * offs
]
val null_ptr : Addr.t list Map.t
val unknown_ptr : Addr.t list Map.t
val not_null : Addr.t list Map.t
val top_ptr : Addr.t list Map.t
val may_be_unknown : Addr.t list Map.t -> bool
val is_null : Addr.t list Map.t -> bool
val is_not_null : Addr.t list Map.t -> bool
val may_be_null : Addr.t list Map.t -> bool
val to_bool : Addr.t list Map.t -> bool option
val has_unknown : Addr.t list Map.t -> bool
val of_int : (module IntDomain.Z with type t = 'a) -> 'a -> Addr.t list Map.t
val to_int : (module IntDomain.Z with type t = 'a) -> Addr.t list Map.t -> 'a
val get_type : Addr.t list Map.t -> GoblintCil.typ
val from_var : CilType.Varinfo.t -> Addr.t list Map.t
val from_var_offset : (CilType.Varinfo.t * (GoblintCil.fieldinfo, Idx.t) Goblint_lib__Lval.offs) -> Addr.t list Map.t
val to_var_may : Addr.t list Map.t -> CilType.Varinfo.t list
val to_var_must : Addr.t list Map.t -> CilType.Varinfo.t list
val to_var_offset : Addr.t list Map.t -> (CilType.Varinfo.t * (GoblintCil.fieldinfo, Idx.t) Goblint_lib__Lval.offs) list
val is_definite : Addr.t list Map.t -> bool
val from_string : string -> Addr.t list Map.t
val to_string : Addr.t list Map.t -> string list
val short_addr : Addr.t -> string
val pretty : unit -> Addr.t list Map.t -> GoblintCil.Pretty.doc
val show : Addr.t list Map.t -> string
val is_top : Addr.t list Map.t -> bool
val merge : (Addr.t list Map.t -> Addr.t list Map.t -> Addr.t list Map.t) -> (Addr.t list Map.t -> Addr.t list Map.t -> Addr.t list Map.t) -> Addr.t list Map.t -> Addr.t list Map.t -> Addr.t list Map.t
val meet : Addr.t list Map.t -> Addr.t list Map.t -> Addr.t list Map.t
val narrow : Addr.t list Map.t -> Addr.t list Map.t -> Addr.t list Map.t
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