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 Edit opam file Versions (11)

Authors

Maintainers

Sources

goblint-2.8.0.tbz

sha256=9175eec0143102243964e34a0786584fd590c60422009259c705a89a27f88de4

sha512=9d760007dd8d003cf596516444ed7acc7370fc3d446e75ac71b0176522c3baae090410762f9035e7aae4f6b0e394bf28bb5b1c08ca0476920b94aa919ef04f42

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