package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install 

dune-project
 Dependency

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

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. K
    Karoliine Holter
  6. M
    Michael Petter
  7. A
    Ali Rasim Kocal
  8. R
    Ralf Vogler
  9. K
    Kalmer Apinis
  10. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>
  3. K
    Karoliine Holter <karoliine.holter@ut.ee>

Sources

goblint-2.7.1.tbz
sha256=af01aac256229f33a90a9fcbfed04b01e3097f154d4d124f006476d6387c6a66
sha512=2a93bfe16881adbc2d8dcbfe38c1e19cd24ca105d8e1eda13d02440f3002874ffe2957dfd937510765233a054a40568b0052db92e31d382a5bd215d1ec12565c

doc/goblint_cdomain_value/ValueDomain/Blob/argument-1-Value/index.html

Parameter Blob.Value

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.

include Lattice.Bot with type t := t
val bot : unit -> t
val is_bot : t -> bool
include Lattice.Top with type t := t
val top : unit -> t
val is_top : t -> bool
type offs
val eval_offset : VDQ.t -> (AD.t -> t) -> t -> offs -> GoblintCil.exp option -> GoblintCil.lval option -> GoblintCil.typ -> t
val update_offset : ?blob_destructive:bool -> VDQ.t -> t -> offs -> t -> GoblintCil.exp option -> GoblintCil.lval -> GoblintCil.typ -> t
val update_array_lengths : (GoblintCil.exp -> t) -> t -> GoblintCil.Cil.typ -> t
val affect_move : ?replace_with_const:bool -> VDQ.t -> t -> GoblintCil.varinfo -> (GoblintCil.exp -> int option) -> t
val affecting_vars : t -> GoblintCil.varinfo list
val invalidate_value : VDQ.t -> GoblintCil.typ -> t -> t
val invalidate_abstract_value : t -> t
val is_statically_safe_cast : GoblintCil.typ -> GoblintCil.typ -> bool
val is_dynamically_safe_cast : GoblintCil.typ -> GoblintCil.typ -> t -> bool
val cast : ?torg:GoblintCil.typ -> GoblintCil.typ -> t -> t
val smart_join : (GoblintCil.exp -> Z.t option) -> (GoblintCil.exp -> Z.t option) -> t -> t -> t
val smart_widen : (GoblintCil.exp -> Z.t option) -> (GoblintCil.exp -> Z.t option) -> t -> t -> t
val smart_leq : (GoblintCil.exp -> Z.t option) -> (GoblintCil.exp -> Z.t option) -> t -> t -> bool
val is_immediate_type : GoblintCil.typ -> bool
val is_mutex_type : GoblintCil.typ -> bool
val bot_value : ?varAttr:GoblintCil.attributes -> GoblintCil.typ -> t
val is_bot_value : t -> bool
val init_value : ?bitfield:int option -> ?varAttr:GoblintCil.attributes -> GoblintCil.typ -> t
val top_value : ?varAttr:GoblintCil.attributes -> GoblintCil.typ -> t
val is_top_value : t -> GoblintCil.typ -> bool
val zero_init_value : ?varAttr:GoblintCil.attributes -> GoblintCil.typ -> t
include ArrayDomain.Null with type t := t
type retnull =
  1. | Null
  2. | NotNull
  3. | Maybe
val null : unit -> t
val is_null : t -> retnull
val get_ikind : t -> GoblintCil.Cil.ikind option
val zero_of_ikind : GoblintCil.Cil.ikind -> t
val not_zero_of_ikind : GoblintCil.Cil.ikind -> t
val project : VDQ.t -> PrecisionUtil.int_precision option -> (GoblintCil.attributes * GoblintCil.attributes) option -> t -> t
val mark_jmpbufs_as_copied : t -> t