sig
type binary =
ConstantInt of Integer.t
| ConstantVar of Cil_types.varinfo
| AffineRef of Cil_types.varinfo * Integer.t
| Boolean of Loop_analysis.Binary.conds
| Unknown
| Bottom
and cond =
UnknownCond
| Lt of bool * Loop_analysis.Binary.binary * Loop_analysis.Binary.binary
| Le of bool * Loop_analysis.Binary.binary * Loop_analysis.Binary.binary
| Eq of Loop_analysis.Binary.binary * Loop_analysis.Binary.binary
| Ne of Loop_analysis.Binary.binary * Loop_analysis.Binary.binary
and conds = Loop_analysis.Binary.cond list
val binary_compare :
Loop_analysis.Binary.binary -> Loop_analysis.Binary.binary -> int
val cond_compare :
Loop_analysis.Binary.cond -> Loop_analysis.Binary.cond -> int
module CondSet :
sig
type elt = cond
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
end
type t = Loop_analysis.Binary.binary
val bottom : Loop_analysis.Binary.binary
val add :
Loop_analysis.Binary.binary ->
Loop_analysis.Binary.binary -> Loop_analysis.Binary.binary
val neg : Loop_analysis.Binary.binary -> Loop_analysis.Binary.binary
val pretty : Format.formatter -> Loop_analysis.Binary.binary -> unit
val pretty_cond : Format.formatter -> Loop_analysis.Binary.cond -> unit
val pretty_conds :
Format.formatter -> Loop_analysis.Binary.cond list -> unit
val transfer_lval :
Cil_types.lval ->
(Cil_types.lval -> Loop_analysis.Binary.binary option) ->
Loop_analysis.Binary.binary
val transfer_exp :
Cil_datatype.Exp.t ->
(Cil_types.lval -> Loop_analysis.Binary.binary option) ->
Loop_analysis.Binary.binary
val not_cond : Loop_analysis.Binary.cond -> Loop_analysis.Binary.cond
val transfer_cond :
Cil_types.exp ->
(Cil_types.lval -> Loop_analysis.Binary.binary option) ->
Loop_analysis.Binary.cond
val join_conds :
Loop_analysis.Binary.CondSet.elt list ->
Loop_analysis.Binary.CondSet.elt list ->
Loop_analysis.Binary.CondSet.elt list
val join :
Loop_analysis.Binary.binary ->
Loop_analysis.Binary.binary -> Loop_analysis.Binary.binary
end