package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-2.4.0.tbz
sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6
sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af
doc/goblint.lib/Goblint_lib/Analyses/index.html
Module Goblint_lib.Analyses
Analysis specification and constraint system signatures.
module M = Messages
type fundecs =
GoblintCil.fundec list * GoblintCil.fundec list * GoblintCil.fundec list
Analysis starts from lists of functions: start functions, exit functions, and * other functions.
module Var : sig ... end
module VarF (LD : Printable.S) : sig ... end
module type SpecSysVar = sig ... end
module GVarF (V : SpecSysVar) : sig ... end
module GVarFC (V : SpecSysVar) (C : Printable.S) : sig ... end
module GVarG (G : Lattice.S) (C : Printable.S) : sig ... end
type ('d, 'g, 'c, 'v) ctx = {
ask : 'a. 'a Queries.t -> 'a Queries.result;
emit : Events.t -> unit;
node : MyCFG.node;
prev_node : MyCFG.node;
control_context : unit -> ControlSpecC.t;
(*top-level Control Spec context, raises
*)Ctx_failure
if missingcontext : unit -> 'c;
(*current Spec context, raises
*)Ctx_failure
if missingedge : MyCFG.edge;
local : 'd;
global : 'v -> 'g;
spawn : ?multiple:bool -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> unit;
split : 'd -> Events.t list -> unit;
sideg : 'v -> 'g -> unit;
}
val ask_of_ctx : ('a, 'b, 'c, 'd) ctx -> Queries.ask
Convert ctx
to Queries.ask
.
module type Spec = sig ... end
module type MCPA = sig ... end
module type MCPSpec = sig ... end
type increment_data = {
server : bool;
solver_data : Stdlib.Obj.t;
changes : CompareCIL.change_info;
restarting : VarQuery.t list;
}
module StdV : sig ... end
module UnitV : sig ... end
module VarinfoV : sig ... end
module EmptyV : sig ... end
module UnitA : sig ... end
module UnitP : sig ... end
module DefaultSpec : sig ... end
Relatively safe default implementations of some boring Spec functions.
module IdentitySpec : sig ... end
module IdentityUnitContextsSpec : sig ... end
module ValueContexts (D : Lattice.S) : sig ... end
module type SpecSys = sig ... end
module type SpecSysSol = sig ... end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>