Module `Constraints.WidenContextLifterSide`

Parameters

module S : Analyses.Spec

Signature

module DD : sig ... end

module M : sig ... end

module D : sig ... end

module G = S.G

module C = S.C

module V = S.V

val name : unit -> string

type marshal = S.marshal

val init : S.marshal option -> unit

val finalize : unit -> S.marshal

val should_join : (S.D.t * 'a) -> (S.D.t * 'b) -> bool

val inj : ('a -> 'b) -> 'a -> 'b * M.t

val startstate : GoblintCil.varinfo -> S.D.t * M.t

val exitstate : GoblintCil.varinfo -> S.D.t * M.t

val morphstate : GoblintCil.varinfo -> (S.D.t * 'a) -> S.D.t * 'a

val context : GoblintCil.fundec -> (S.D.t * 'a) -> S.C.t

val conv : ('a * 'b, 'c, 'd, 'e) Analyses.ctx -> ('a, 'c, 'd, 'e) Analyses.ctx

val lift_fun : 
  ('a * 'b, 'c, 'd, 'e) Analyses.ctx ->
  (('a, 'c, 'd, 'e) Analyses.ctx -> 'f) ->
  ('f -> 'g) ->
  'g * 'b

val sync : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  [ `Join | `Normal | `Return ] ->
  S.D.t * 'a

val query : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  'b Queries.t ->
  'b Queries.result

val assign : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  GoblintCil.lval ->
  GoblintCil.exp ->
  S.D.t * 'a

val vdecl : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  GoblintCil.varinfo ->
  S.D.t * 'a

val branch : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  GoblintCil.exp ->
  bool ->
  S.D.t * 'a

val body : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  GoblintCil.fundec ->
  S.D.t * 'a

val return : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  GoblintCil.exp option ->
  GoblintCil.fundec ->
  S.D.t * 'a

val asm : (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx -> S.D.t * 'a

val skip : (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx -> S.D.t * 'a

val special : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  S.D.t * 'a

val threadenter : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  (S.D.t * 'a) list

val threadspawn : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  (S.D.t * 'b, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  S.D.t * 'a

val enter : 
  (S.D.t * M.t, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  ((S.D.t * M.t) * (S.D.t * M.t)) list

val combine : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.exp ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  S.C.t option ->
  (S.D.t * 'b) ->
  S.D.t * 'a

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/Constraints/WidenContextLifterSide/index.html

Module `Constraints.WidenContextLifterSide`

Parameters

Signature

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/Constraints/WidenContextLifterSide/index.html

Module Constraints.WidenContextLifterSide

Parameters

Signature

Module `Constraints.WidenContextLifterSide`