HashCachedContextLifter (goblint.Goblint_lib.SpecLifters.HashCachedContextLifter)

Parameters

module S : Analyses.Spec

Signature

module D : sig ... end

module G : sig ... end

module C : sig ... end

module V : sig ... end

module P : sig ... end

val name : unit -> string

type marshal

val init : marshal option -> unit

val finalize : unit -> marshal

val startstate : GoblintCil.varinfo -> D.t

val morphstate : GoblintCil.varinfo -> D.t -> D.t

val exitstate : GoblintCil.varinfo -> D.t

val context : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  GoblintCil.fundec ->
  D.t ->
  C.t

val startcontext : unit -> C.t

val sync : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  [ `Join | `JoinCall of CilType.Fundec.t | `Normal | `Return ] ->
  D.t

val query : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  'a Queries.t ->
  'a Queries.result

val assign : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  GoblintCil.lval ->
  GoblintCil.exp ->
  D.t

val vdecl : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  GoblintCil.varinfo ->
  D.t

val branch : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  GoblintCil.exp ->
  bool ->
  D.t

val body : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  GoblintCil.fundec ->
  D.t

val return : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  GoblintCil.exp option ->
  GoblintCil.fundec ->
  D.t

val asm : (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man -> D.t

val skip : (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man -> D.t

val special : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  D.t

val enter : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  GoblintCil.lval option ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  (D.t * D.t) list

val combine_env : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  GoblintCil.lval option ->
  GoblintCil.exp ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  C.t option ->
  D.t ->
  Queries.ask ->
  D.t

val combine_assign : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  GoblintCil.lval option ->
  GoblintCil.exp ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  C.t option ->
  D.t ->
  Queries.ask ->
  D.t

val paths_as_set : (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man -> D.t list

val threadenter : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  multiple:bool ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  D.t list

val threadspawn : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  multiple:bool ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  D.t

val event : 
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  Events.t ->
  (D.t, G.t, C.t, V.t) Goblint_lib__Analyses.man ->
  D.t