sig
module B = Binary
module Varinfo = Cil_datatype.Varinfo
type t = B.t Varinfo.Map.t * B.conds * Cil_types.stmt
val pretty :
Format.formatter -> B.binary Varinfo.Map.t * B.cond list -> unit
val bottom : 'a Varinfo.Map.t * 'b list * Cil_types.stmt
val init : 'a -> 'b Varinfo.Map.t * 'c list * 'a
val load :
B.binary Varinfo.Map.t ->
Cil_types.lhost * Cil_types.offset -> B.binary option
val join2_stmts :
Cil_datatype.Stmt.t -> Cil_datatype.Stmt.t -> Cil_datatype.Stmt.t
val do_instr :
Cil_types.instr ->
B.binary Varinfo.Map.t * B.cond list ->
B.binary Varinfo.Map.t * B.cond list
val do_guard :
'a ->
Cil_types.exp ->
B.binary Varinfo.Map.t * B.cond list ->
(B.binary Varinfo.Map.t * B.cond list) *
(B.binary Varinfo.Map.t * B.cond list)
val compile_node :
Cil_datatype.Stmt.t ->
B.binary Varinfo.Map.t * B.cond list * Cil_datatype.Stmt.t ->
(Cil_datatype.Stmt.t Region_analysis.edge *
(B.binary Varinfo.Map.t * B.cond list * Cil_datatype.Stmt.t))
list
val mu :
(Loop_analysis.Store.t -> Loop_analysis.Store.t) ->
B.binary Varinfo.Map.t * B.cond list * Cil_datatype.Stmt.t ->
B.binary Varinfo.Map.t * B.cond list * Cil_datatype.Stmt.t
val join2_mem :
B.binary Varinfo.Map.t ->
B.binary Varinfo.Map.t -> B.binary Varinfo.Map.t
val join2 :
B.binary Varinfo.Map.t * B.CondSet.elt list * Cil_datatype.Stmt.t ->
B.binary Varinfo.Map.t * B.CondSet.elt list * Cil_datatype.Stmt.t ->
B.binary Varinfo.Map.t * B.CondSet.elt list * Cil_datatype.Stmt.t
val join :
(B.binary Varinfo.Map.t * B.CondSet.elt list * Cil_datatype.Stmt.t) list ->
B.binary Varinfo.Map.t * B.CondSet.elt list * Cil_datatype.Stmt.t
type abstract_value = Loop_analysis.Store.t
end