package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-2.0.0.tbz
sha256=2f4f2e25b765452f0e336941f35f6cb396d7c213a2d347abe5d35febc5159b1f
sha512=e96af4cad91f6985c8db93c194925853e96cad0ec1a0d9f4d32bbe16d3e5fa1e305f54be02839f21ba89ad2af0c2d5d7aa819ade221ce097dc4dbd0fcd8c8500
doc/goblint.lib/Goblint_lib/MHPAnalysis/Spec/index.html
Module MHPAnalysis.Spec
include module type of struct include UnitAnalysis.Spec end
include Analyses.Spec with module D = Lattice.Unit with module C = Lattice.Unit
module D = Goblint_lib.UnitAnalysis.Spec.D
module G = UnitAnalysis.Spec.G
module C = Goblint_lib.UnitAnalysis.Spec.C
module V = UnitAnalysis.Spec.V
Global constraint variables.
type marshal = UnitAnalysis.Spec.marshal
Auxiliary data (outside of solution domains) that needs to be marshaled and unmarshaled. This includes: * hashtables, * varinfos (create_var), * RichVarinfos.
val init : marshal option -> unit
Initialize using unmarshaled auxiliary data (if present).
val finalize : unit -> marshal
Finalize and return auxiliary data to be marshaled.
val startstate : GoblintCil.varinfo -> D.t
val exitstate : GoblintCil.varinfo -> D.t
val query :
(D.t, G.t, C.t, V.t) Analyses.ctx ->
'a Queries.t ->
'a Queries.result
module A : sig ... end
val access : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> MHP.t
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>