BO.Itv
module Bound = Bounds.Bound
module SymbolPath = Symb.SymbolPath
module SymbolSet = Symb.SymbolSet
module ItvRange : sig ... end
module ItvPure : sig ... end
val bot : t
_|_
val zero_255 : t
0, 255
val m1_255 : t
-1, 255
val nat : t
0, +oo
val pos : t
1, +oo
val top : t
-oo, +oo
val zero : t
0
val one : t
1
val zero_one : t
0, 1
val unknown_bool : t
0, 1
val of_int : int -> t
val of_big_int : Z.t -> t
val of_int_lit : IR.IntLit.t -> t
val get_const : t -> Z.t option
val is_zero : t -> bool
val is_one : t -> bool
val is_mone : t -> bool
val get_bound :
t ->
Symb.BoundEnd.t ->
Bound.t Absint.AbstractDomain.Types.bottom_lifted
val is_false : t -> bool
val is_symbolic : t -> bool
val is_top : t -> bool
val get_symbols : t -> SymbolSet.t
val range : IBase.Location.t -> t -> ItvRange.t
val prune_binop : IR.Binop.t -> t -> t -> t
val subst : t -> Bound.eval_sym -> t
val max_of_ikind : IR.IntegerWidths.t -> IR.Typ.ikind -> t
val of_normal_path :
unsigned:bool ->
?non_int:bool ->
Symb.SymbolPath.partial ->
t
val of_offset_path : is_void:bool -> Symb.SymbolPath.partial -> t
val of_length_path : is_void:bool -> Symb.SymbolPath.partial -> t
val of_modeled_path : Symb.SymbolPath.partial -> t
val is_offset_path_of : Symb.SymbolPath.partial -> t -> bool
val is_length_path_of : Symb.SymbolPath.partial -> t -> bool
val has_only_non_int_symbols : t -> bool
val is_incr_of : Symb.SymbolPath.partial -> t -> bool
Check if itv
is path+1
when called is_incr_of path itv