package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=dba2b664c7c125687e708e871d83fbfb6ba6d9ee98d235b4850d9a238caa84de
sha512=529987cde39691ad9e955000a3603e89c1c8cf14ed5e8b4cd3a7fc26e47d016aff571b472e2329725133c46f8d0cb45a05b88994eeffaa221a4d31b4c543adcd
doc/goblint.lib/Goblint_lib/Constraints/index.html
Module Goblint_lib.Constraints
How to generate constraints for a solver using specifications described in Analyses
.
module M = Messages
module HashconsLifter
(S : Analyses.Spec) :
Analyses.Spec
with module D = Lattice.HConsed(S.D)
and 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 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 EqIncrSolverFromEqSolver
(Sol : Analyses.GenericEqBoxSolver) :
Analyses.GenericEqBoxIncrSolver
Convert a non-incremental solver into an "incremental" solver. It will solve from scratch, perform standard postsolving and have no marshal data.
module Var2
(LV : Analyses.VarType)
(GV : Analyses.VarType) :
Analyses.VarType with type t = [ `L of LV.t | `G of GV.t ]
Combined variables so that we can also use the more common EqConstrSys
that uses only one kind of a variable.
module EqConstrSysFromGlobConstrSys
(S : Analyses.GlobConstrSys) :
Analyses.EqConstrSys
with type v = Var2(S.LVar)(S.GVar).t
and type d = Lattice.Lift2(S.G)(S.D)(Printable.DefaultNames).t
and module Var = Var2(S.LVar)(S.GVar)
and module Dom = Lattice.Lift2(S.G)(S.D)(Printable.DefaultNames)
Translate a GlobConstrSys
into a EqConstrSys
module GlobConstrSolFromEqConstrSolBase
(S : Analyses.GlobConstrSys)
(LH : Goblint_lib.Prelude.Hashtbl.S with type key = S.LVar.t)
(GH : Goblint_lib.Prelude.Hashtbl.S with type key = S.GVar.t)
(VH : Goblint_lib.Prelude.Hashtbl.S with type key = Var2(S.LVar)(S.GVar).t) :
sig ... end
Splits a EqConstrSys
solution into a GlobConstrSys
solution with given Hashtbl.S
for the EqConstrSys
.
module GlobConstrSolFromEqConstrSol
(S : Analyses.GlobConstrSys)
(LH : Goblint_lib.Prelude.Hashtbl.S with type key = S.LVar.t)
(GH : Goblint_lib.Prelude.Hashtbl.S with type key = S.GVar.t) :
sig ... end
Splits a EqConstrSys
solution into a GlobConstrSys
solution.
module GlobSolverFromEqSolver
(Sol : Analyses.GenericEqBoxIncrSolverBase) :
Analyses.GenericGlobSolver
Transforms a GenericEqBoxIncrSolver
into a GenericGlobSolver
.
module PathSensitive2
(Spec : Analyses.Spec) :
Analyses.Spec
with type D.t = HoareDomain.Set(Spec.D).t
and 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 CompareGlobSys
(S : Analyses.Spec)
(Sys :
Analyses.GlobConstrSys
with module LVar = Analyses.VarF(S.C)
and module GVar = Analyses.GVarF(S.V)
and module D = S.D
and module G = Analyses.GVarG(S.G)(S.C))
(LH : Goblint_lib.Prelude.Hashtbl.S with type key = Sys.LVar.t)
(GH : Goblint_lib.Prelude.Hashtbl.S with type key = Sys.GVar.t) :
sig ... end
module CompareHashtbl
(Var : Analyses.VarType)
(Dom : Lattice.S)
(VH : Goblint_lib.Prelude.Hashtbl.S with type key = Var.t) :
sig ... end
module CompareEqSys
(Sys : Analyses.EqConstrSys)
(VH : Goblint_lib.Prelude.Hashtbl.S with type key = Sys.Var.t) :
sig ... end
module CompareGlobal
(GVar : Analyses.VarType)
(G : Lattice.S)
(GH : Goblint_lib.Prelude.Hashtbl.S with type key = GVar.t) :
sig ... end
module CompareNode
(C : Printable.S)
(D : Lattice.S)
(LH : Goblint_lib.Prelude.Hashtbl.S with type key = Analyses.VarF(C).t) :
sig ... end
module CurrentVarEqConstrSys (S : Analyses.EqConstrSys) : sig ... end
EqConstrSys
where current_var
indicates the variable whose right-hand side is currently being evaluated.