WidenContextLifterSide (p.goblint.2.5.0.doc.goblint.lib.Goblint

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

module P : sig ... end

val name : unit -> string

type marshal = S.marshal

val init : S.marshal option -> unit

val finalize : unit -> S.marshal

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

val startcontext : unit -> S.C.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 conv : ('a * 'b, 'c, 'd, 'e) Analyses.ctx -> ('a, 'c, 'd, 'e) Analyses.ctx

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

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 | `JoinCall of CilType.Fundec.t | `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 event : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  Events.t ->
  (S.D.t * 'b, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  S.D.t * 'a

val threadenter : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  multiple:bool ->
  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 ->
  multiple:bool ->
  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 paths_as_set : 
  (S.D.t * 'a, S.G.t, S.C.t, S.V.t) Analyses.ctx ->
  (S.D.t * 'a) list

val combine_env : 
  (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) ->
  Queries.ask ->
  S.D.t * 'a

val combine_assign : 
  (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) ->
  Queries.ask ->
  S.D.t * 'a