package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

Dune Dependency

Authors

Maintainers

Sources

goblint-2.4.0.tbz
sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6
sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af

doc/goblint.constraint/ConstrSys/index.html

Module ConstrSysSource

constraint system signatures.

Sourcemodule type SysVar = sig ... end
Sourcemodule type VarType = sig ... end
Sourcetype '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

Sourcemodule type MonSystem = sig ... end

A side-effecting system.

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

Any system of side-effecting equations over lattices.

Sourcemodule type GlobConstrSys = sig ... end

A side-effecting system with globals.

Sourcemodule 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.

Sourcemodule type IncrSolverArg = sig ... end

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

An incremental solver takes the argument about postsolving.

Sourcemodule 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)

Sourcemodule 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)

Sourcemodule 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

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

Splits a EqConstrSys solution into a GlobConstrSys solution.

Transforms a GenericEqIncrSolver into a GenericGlobSolver.

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

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

OCaml

Innovation. Community. Security.