package goblint

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

The main point of this file---generating a GlobConstrSys from a Spec.

Parameters

module S : Analyses.Spec
module I : Increment

Signature

include Analyses.GlobConstrSys with module LVar = Analyses.VarF(S.C) and module GVar = Basetype.Variables and module D = S.D and module G = S.G
module LVar = Analyses.VarF(S.C)
module GVar = Basetype.Variables
module D = S.D
module G = S.G
val increment : Analyses.increment_data
val system : LVar.t -> ((LVar.t -> D.t) -> (LVar.t -> D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t) option
val tf : (MyCFG.node * S.C.t) -> ((Cil.location * MyCFG.edge) list * MyCFG.node) -> ((MyCFG.node * S.C.t) -> S.D.t) -> ((MyCFG.node * S.C.t) -> S.D.t -> unit) -> (Cil.varinfo -> G.t) -> (Cil.varinfo -> G.t -> unit) -> D.t