package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

Dune Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (8)

Authors

Maintainers

Sources

goblint-1.1.1.tbz

sha256=999272bfbd3b9b96fcd58987b237ac6e9fa6d92ef935cc89f1ea2b4205185141

sha512=f3bf6ab71cf8c258d3290da4bf9f6fe42d7c671822e0efeb0fc50afdff078ab15e352237e5c1db31c5aa3a9d430691268ed2e5e00da10f2615835f672f91683d

doc/goblint.lib/PostSolver/index.html

Module `PostSolver`

module type S = sig ... end

Postsolver with hooks.

module type F =
  functor (S : Analyses.EqConstrSys) ->
  functor (VH : Prelude.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 Make (PS : S) : sig ... end

Make complete postsolving function from postsolver. This is generic and non-incremental.

module type MakeListArg = sig ... end

List of postsolvers.

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

Make complete postsolving function from list of postsolvers. If list is empty, no postsolving is performed. This is generic and non-incremental.

module type MakeStdArg = sig ... end

Standard postsolver options.

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

List of standard postsolvers.