package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-2.5.0.tbz
sha256=452d8491527aea21f2cbb11defcc14ba0daf9fdb6bdb9fc0af73e56eac57b916
sha512=1993cd45c4c7fe124ca6e157f07d17ec50fab5611b270a434ed1b7fb2910aa85a8e6eaaa77dad770430710aafb2f6d676c774dd33942d921f23e2f9854486551
doc/goblint.lib/Goblint_lib/SpecLifters/index.html
Module Goblint_lib.SpecLifters
Various simple and old analysis lifters.
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 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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>