Module `Goblint_solver.PostSolver`Source

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

module Pretty = GoblintCil.Pretty

module M = Messages

Sourcemodule type S = sig ... end

Postsolver with hooks.

module type F =
  functor (S : Goblint_constraint.ConstrSys.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.

Sourcemodule Unit : F

Base implementation for postsolver.

Source

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.

Sourcemodule Prune : F

Postsolver for pruning solution using reachability.

Sourcemodule Verify : F

Postsolver for verifying solution in demand-driven fashion.

Sourcemodule Warn : F

Postsolver for enabling messages (warnings) output.

Sourcemodule SaveRun : F

Postsolver for save_run option.

Sourcemodule type StartEqConstrSys = sig ... end

EqConstrSys together with start values to be used.

Source

module EqConstrSysFromStartEqConstrSys
  (S : StartEqConstrSys) : 
  Goblint_constraint.ConstrSys.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.

Sourcemodule type IncrS = sig ... end

Postsolver for incremental.

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

Make incremental postsolving function from incremental postsolver.

Sourcemodule type MakeListArg = sig ... end

List of postsolvers.

Sourcemodule type MakeIncrListArg = sig ... end

List of postsolvers for incremental.

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

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

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

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

Sourcemodule type MakeStdArg = sig ... end

Standard postsolver options.

Source

module ListArgFromStdArg
  (S : Goblint_constraint.ConstrSys.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.

Source

module EqIncrSolverFromEqSolver
  (Sol : Goblint_constraint.SolverTypes.GenericEqSolver) : 
  Goblint_constraint.SolverTypes.GenericEqIncrSolver

Convert a non-incremental solver into an "incremental" solver. It will solve from scratch, perform standard postsolving and have no marshal data.

Source

module DemandEqIncrSolverFromEqSolver
  (Sol : Goblint_constraint.SolverTypes.GenericEqSolver) : 
  Goblint_constraint.SolverTypes.DemandEqIncrSolver

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/goblint.solver/Goblint_solver/PostSolver/index.html

Module `Goblint_solver.PostSolver`Source

package goblint

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/goblint.solver/Goblint_solver/PostSolver/index.html

Module Goblint_solver.PostSolverSource

dune-project
Dependency

Module `Goblint_solver.PostSolver`Source