package goblint

  1. Overview
  2. Docs
package goblint
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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct