Goblint_lib.Constraints
Construction of a constraint system from an analysis specification and CFGs. Transformatons of analysis specifications as functors.
module M = Messages
module HashconsLifter
(S : Analyses.Spec) :
Analyses.Spec with module G = S.G and module C = S.C
Lifts a Spec
so that the domain is Hashcons
d
module HashconsContextLifter
(S : Analyses.Spec) :
Analyses.Spec
with module D = S.D
and module G = S.G
and module C = Printable.HConsed(S.C)
Lifts a Spec
so that the context is Hashcons
d.
module OptEqual (S : Analyses.Spec) : sig ... end
module LevelSliceLifter
(S : Analyses.Spec) :
Analyses.Spec
with module D = Lattice.Prod(S.D)(Lattice.Reverse(IntDomain.Lifted))
and module G = S.G
and module C = S.C
If dbg.slice.on, stops entering functions after dbg.slice.n levels.
module LimitLifter (S : Analyses.Spec) : sig ... end
Limits the number of widenings per node.
module WidenContextLifterSide (S : Analyses.Spec) : sig ... end
module DeadCodeLifter
(S : Analyses.Spec) :
Analyses.Spec
with module D = Analyses.Dom(S.D)
and module G = S.G
and module C = S.C
Lifts a Spec
with a special bottom element that represent unreachable code.
module NoContext : sig ... end
module IntConf : sig ... end
module ContextGasLifter
(S : Analyses.Spec) :
Analyses.Spec
with module D = Lattice.Prod(S.D)(Lattice.Chain(IntConf))
and module C = Printable.Option(S.C)(NoContext)
and module G = S.G
Lifts a Spec
with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack. For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information
module type Increment = sig ... end
module FromSpec
(S : Analyses.Spec)
(Cfg : MyCFG.CfgBackward)
(I : Increment) :
sig ... end
The main point of this file---generating a GlobConstrSys
from a Spec
.
module PathSensitive2
(Spec : Analyses.Spec) :
Analyses.Spec
with module G = Spec.G
and module C = Spec.C
and module V = Spec.V
Add path sensitivity to a analysis
module DeadBranchLifter (S : Analyses.Spec) : Analyses.Spec
module LongjmpLifter (S : Analyses.Spec) : Analyses.Spec
module RecursionTermLifter
(S : Analyses.Spec) :
Analyses.Spec with module D = S.D and module C = S.C
Add cycle detection in the context-sensitive dynamic function call graph to an analysis
module CompareGlobSys (SpecSys : Analyses.SpecSys) : sig ... end
module CompareHashtbl
(Var : ConstrSys.VarType)
(Dom : Lattice.S)
(VH : Batteries.Hashtbl.S with type key = Var.t) :
sig ... end
module CompareEqSys
(Sys : ConstrSys.EqConstrSys)
(VH : Batteries.Hashtbl.S with type key = Sys.Var.t) :
sig ... end
module CompareGlobal
(GVar : ConstrSys.VarType)
(G : Lattice.S)
(GH : Batteries.Hashtbl.S with type key = GVar.t) :
sig ... end
module CompareNode
(C : Printable.S)
(D : Lattice.S)
(LH : Batteries.Hashtbl.S with type key = Goblint_lib__.Analyses.VarF(C).t) :
sig ... end