Up  Next

Module Loop_analysis.Store.B

module B: Loop_analysis.Binary
type binary =
| ConstantInt of Integer.t
| ConstantVar of Cil_types.varinfo
| AffineRef of Cil_types.varinfo * Integer.t
| Boolean of conds
| Unknown
| Bottom 
type cond =
| UnknownCond
| Lt of bool * binary * binary
| Le of bool * binary * binary
| Eq of binary * binary
| Ne of binary * binary 
type conds = cond list 
val binary_compare : binary -> binary -> int
val cond_compare : cond -> cond -> int
module CondSet: Set.Make(sig


type t = Loop_analysis.Binary.cond 




val compare : Loop_analysis.Binary.cond -> Loop_analysis.Binary.cond -> int
end)
type t = binary 
val bottom : binary
val add : binary ->
       binary -> binary
val neg : binary -> binary
val pretty : Format.formatter -> binary -> unit
val pretty_cond : Format.formatter -> cond -> unit
val pretty_conds : Format.formatter -> cond list -> unit
val transfer_lval : Cil_types.lval ->
       (Cil_types.lval -> binary option) ->
       binary
val transfer_exp : Cil_datatype.Exp.t ->
       (Cil_types.lval -> binary option) ->
       binary
val transfer_exp : Cil_datatype.Exp.t ->
       (Cil_types.lval -> binary option) ->
       binary
val not_cond : cond -> cond
val transfer_cond : Cil_types.exp ->
       (Cil_types.lval -> binary option) ->
       cond
val transfer_cond : Cil_types.exp ->
       (Cil_types.lval -> binary option) ->
       cond
val join_conds : CondSet.elt list ->
       CondSet.elt list ->
       CondSet.elt list
val join : binary ->
       binary -> binary