package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

dune-project

Dependency

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

Authors

Maintainers

Sources

goblint-2.6.0.tbz

sha256=20d5b7332a9f6072ab9ba86c4a53b898eaf681286c56a8805c41850bbf3ddf41

sha512=7c7685cfcd9aa866bc40e813df2bfcb3c79b3d40e615d8d6d0939c5798b9d70dd7f2ba87a741f5ba0ce891e9d254627207fb28057f1f2f6611e4e0d128fd6a71

doc/goblint.constraint/Goblint_constraint/Translators/index.html

Module `Goblint_constraint.Translators`Source

Source

module EqConstrSysFromDemandConstrSys
  (S : ConstrSys.DemandEqConstrSys) : 
  ConstrSys.EqConstrSys
    with type v = S.v
     and type d = S.d
     and module Var = S.Var
     and module Dom = S.Dom

Translate a DemandConstrSys into a EqConstrSys

Source

module EqConstrSysFromGlobConstrSys
  (S : ConstrSys.DemandGlobConstrSys) : 
  ConstrSys.DemandEqConstrSys
    with type v = ConstrSys.Var2(S.LVar)(S.GVar).t
     and type d = Lattice.Lift2(S.G)(S.D).t
     and module Var = ConstrSys.Var2(S.LVar)(S.GVar)
     and module Dom = Lattice.Lift2(S.G)(S.D)

Translate a DemandGlobConstrSys into a DemandEqConstrSys

Source

module GlobConstrSolFromEqConstrSolBase
  (S : ConstrSys.DemandGlobConstrSys)
  (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 = ConstrSys.Var2(S.LVar)(S.GVar).t) : 
  sig ... end

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

Source

module GlobConstrSolFromEqConstrSol
  (S : ConstrSys.DemandGlobConstrSys)
  (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.

Source

module DemandEqIncrSolverFromGenericEqIncrSolver
  (Sol : SolverTypes.GenericEqIncrSolver) : 
  SolverTypes.DemandEqIncrSolver

Source

module GlobSolverFromEqSolver
  (Sol : SolverTypes.DemandEqIncrSolverBase)
  (S : ConstrSys.DemandGlobConstrSys)
  (LH : Batteries.Hashtbl.S with type key = S.LVar.t)
  (GH : Batteries.Hashtbl.S with type key = S.GVar.t) : 
  sig ... end

Transforms a DemandEqIncrSolver into a DemandGlobIncrSolver.

package goblint

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/goblint.constraint/Goblint_constraint/Translators/index.html

Module Goblint_constraint.TranslatorsSource

dune-project
Dependency

Module `Goblint_constraint.Translators`Source