package goblint

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

constraint system signatures.

module type SysVar = sig ... end
module type VarType = sig ... end
type 'v sys_change_info = {
  1. obsolete : 'v list;
    (*

    Variables to destabilize.

    *)
  2. delete : 'v list;
    (*

    Variables to delete.

    *)
  3. reluctant : 'v list;
    (*

    Variables to solve reluctantly.

    *)
  4. restart : 'v list;
    (*

    Variables to restart.

    *)
}

Abstract incremental change to constraint system.

  • parameter 'v

    constrain system variable type

module type MonSystem = sig ... end

A side-effecting system.

module type EqConstrSys = MonSystem with type 'a m := 'a option

Any system of side-effecting equations over lattices.

module type GlobConstrSys = sig ... end

A side-effecting system with globals.

module type GenericEqIncrSolverBase = functor (S : EqConstrSys) -> functor (H : Batteries.Hashtbl.S with type key = S.v) -> sig ... end

A solver is something that can translate a system into a solution (hash-table). Incremental solver has data to be marshaled.

module type IncrSolverArg = sig ... end

(Incremental) solver argument, indicating which postsolving should be performed by the solver.

An incremental solver takes the argument about postsolving.

module type GenericEqSolver = functor (S : EqConstrSys) -> functor (H : Batteries.Hashtbl.S with type key = S.v) -> sig ... end

A solver is something that can translate a system into a solution (hash-table)

module type GenericGlobSolver = functor (S : GlobConstrSys) -> functor (LH : Batteries.Hashtbl.S with type key = S.LVar.t) -> functor (GH : Batteries.Hashtbl.S with type key = S.GVar.t) -> sig ... end

A solver is something that can translate a system into a solution (hash-table)

module Var2 (LV : VarType) (GV : VarType) : VarType with type t = [ `L of LV.t | `G of GV.t ]

Combined variables so that we can also use the more common EqConstrSys that uses only one kind of a variable.

Translate a GlobConstrSys into a EqConstrSys

module GlobConstrSolFromEqConstrSolBase (S : GlobConstrSys) (LH : Batteries.Hashtbl.S with type key = S.LVar.t) (GH : Batteries.Hashtbl.S with type key = S.GVar.t) (VH : Batteries.Hashtbl.S with type key = Var2(S.LVar)(S.GVar).t) : sig ... end

Splits a EqConstrSys solution into a GlobConstrSys solution with given Hashtbl.S for the EqConstrSys.

module GlobConstrSolFromEqConstrSol (S : GlobConstrSys) (LH : Batteries.Hashtbl.S with type key = S.LVar.t) (GH : Batteries.Hashtbl.S with type key = S.GVar.t) : sig ... end

Splits a EqConstrSys solution into a GlobConstrSys solution.

module GlobSolverFromEqSolver (Sol : GenericEqIncrSolverBase) (S : GlobConstrSys) (LH : Batteries.Hashtbl.S with type key = S.LVar.t) (GH : Batteries.Hashtbl.S with type key = S.GVar.t) : sig ... end

Transforms a GenericEqIncrSolver into a GenericGlobSolver.

module CurrentVarEqConstrSys (S : EqConstrSys) : sig ... end

EqConstrSys where current_var indicates the variable whose right-hand side is currently being evaluated.

OCaml

Innovation. Community. Security.