package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

Dune Dependency

Authors

Maintainers

Sources

goblint-2.3.0.tbz
sha256=b729c94adb383a39aea32eb005c988dfd44b92af22ee6a4eedf4239542ac6c26
sha512=643b98770e5fe5644324c95c9ae3a9f698f25c8b11b298f0751d524e0b20af368b2a465fc8200b75a73d48fc9a053fd90f5e8920d4db070927f93188bb8687e0

doc/goblint.lib/Goblint_lib/PostSolver/index.html

Module Goblint_lib.PostSolver

Extra constraint system evaluation pass for warning generation, verification, pruning, etc.

module Pretty = GoblintCil.Pretty
module type S = sig ... end

Postsolver with hooks.

module type F = functor (S : Analyses.EqConstrSys) -> functor (VH : Batteries.Hashtbl.S with type key = S.v) -> S with module S = S and module VH = VH

Functorial postsolver for any system.

module Unit : F

Base implementation for postsolver.

module Compose (PS1 : S) (PS2 : S with module S = PS1.S and module VH = PS1.VH) : S with module S = PS1.S and module VH = PS1.VH

Sequential composition of two postsolvers.

module Prune : F

Postsolver for pruning solution using reachability.

module Verify : F

Postsolver for verifying solution in demand-driven fashion.

module Warn : F

Postsolver for enabling messages (warnings) output.

module SaveRun : F

Postsolver for save_run option.

module type StartEqConstrSys = sig ... end

EqConstrSys together with start values to be used.

module EqConstrSysFromStartEqConstrSys (S : StartEqConstrSys) : Analyses.EqConstrSys with type v = S.v and type d = S.d and module Var = S.Var and module Dom = S.Dom

Join start values into right-hand sides. This simplifies start handling in Make.

module type IncrS = sig ... end

Postsolver for incremental.

module MakeIncr (PS : IncrS) : sig ... end

Make incremental postsolving function from incremental postsolver.

module type MakeListArg = sig ... end

List of postsolvers.

module type MakeIncrListArg = sig ... end

List of postsolvers for incremental.

module MakeIncrList (Arg : MakeIncrListArg) : sig ... end

Make incremental postsolving function from incremental list of postsolvers. If list is empty, no postsolving is performed.

module MakeList (Arg : MakeListArg) : sig ... end

Make complete (non-incremental) postsolving function from list of postsolvers. If list is empty, no postsolving is performed.

module type MakeStdArg = sig ... end

Standard postsolver options.

module ListArgFromStdArg (S : Analyses.EqConstrSys) (VH : Batteries.Hashtbl.S with type key = S.v) (Arg : MakeStdArg) : MakeListArg with module S = S and module VH = VH

List of standard postsolvers.

OCaml

Innovation. Community. Security.