module Store: sig
.. end
module B: Loop_analysis.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_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 : (t -> 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 = t