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.lib/Goblint_lib/C2poDomain/D/index.html

Module C2poDomain.D

include sig ... end
type t = [
  1. | `Bot
  2. | `Lifted of C2PODomain.t
]
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> Ppx_deriving_runtime.int
val hash : t -> int
val tag : 'a -> 'b
val arbitrary : unit -> 'a
val lift : 'a -> [> `Lifted of 'a ]
val show : [< `Bot | `Lifted of C2PODomain.t ] -> string
val pretty : unit -> t -> Printable.Pretty.doc
val name : unit -> string
val to_yojson : [< `Bot | `Lifted of C2PODomain.t ] -> Yojson.Safe.t
val relift : [< `Bot | `Lifted of C2PODomain.t ] -> [> `Bot | `Lifted of C2PODomain.t ]
val bot : unit -> [> `Bot ]
val is_bot : [> `Bot ] -> bool
val top : unit -> [> `Lifted of C2PODomain.t ]
val is_top : [< `Bot | `Lifted of C2PODomain.t ] -> bool
val leq : [< `Bot | `Lifted of C2PODomain.t ] -> [< `Bot | `Lifted of C2PODomain.t ] -> bool
val pretty_diff : unit -> (t * t) -> Lattice.Pretty.doc
val join : ([< `Bot | `Lifted of C2PODomain.t Lifted ] as 'a) -> 'a -> 'a
val widen : [> `Lifted of C2PODomain.t ] -> ([> `Lifted of C2PODomain.t ] as 'a) -> 'a
val show_all : [< `Bot | `Lifted of CongruenceClosure.t ] -> string
val meet : [< `Bot | `Lifted of C2PODomain.t ] -> [< `Bot | `Lifted of C2PODomain.t ] -> [> `Bot | `Lifted of C2PODomain.t ]
val narrow : ([> `Bot | `Lifted of C2PODomain.t ] as 'a) -> [> `Bot | `Lifted of C2PODomain.t ] -> 'a
val printXml : 'a BatInnerIO.output -> [< `Bot | `Lifted of C2PODomain.t ] -> unit
val remove_terms_containing_aux_variable : CongruenceClosure.data -> CongruenceClosure.data

Remove terms from the data structure. It removes all terms that contain an AssignAux variable, while maintaining all equalities about variables that are not being removed.

val remove_terms_containing_return_variable : CongruenceClosure.data -> CongruenceClosure.data

Remove terms from the data structure. It removes all terms that contain an ReturnAux variable, while maintaining all equalities about variables that are not being removed.

val remove_terms_containing_variables : DuplicateVars.Var.t list -> CongruenceClosure.data -> CongruenceClosure.data

Remove terms from the data structure. It removes all terms which contain one of the "vars", while maintaining all equalities about variables that are not being removed.

val remove_terms_not_containing_variables : DuplicateVars.Var.t list -> CongruenceClosure.data -> CongruenceClosure.data

Remove terms from the data structure. It removes all terms which do not contain one of the "vars", except the global vars are also kept (when vglob = true), while maintaining all equalities about variables that are not being removed.

val remove_may_equal_terms : Queries.ask -> Z.t -> UnionFind.T.t -> CongruenceClosure.data -> CongruenceClosure.data

Remove terms from the data structure. It removes all terms that may be changed after an assignment to "term".

Remove terms from the data structure. It removes all terms that may point to one of the tainted addresses.

Remove terms from the data structure. It removes all terms that are not in the scope, and also those that are tmp variables.