Parameters
Signature
include sig ... end
val name : unit -> string
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 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 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