Module BO.Itv

module F = Stdlib.Format
module Bound = Bounds.Bound
module SymbolPath = Symb.SymbolPath
module SymbolSet = Symb.SymbolSet
module ItvRange : sig ... end
module ItvPure : sig ... end
include sig ... end
type t
val pp : IStdlib__PrettyPrintable.F.formatter -> t -> unit
val leq : lhs:t -> rhs:t -> bool
val join : t -> t -> t
val widen : prev:t -> next:t -> num_iters:int -> t
val bottom : t
val is_bottom : t -> bool
val map : f:(ItvPure.t -> ItvPure.t) -> t -> t
val widen_thresholds : thresholds:Z.t list -> prev:t -> next:t -> num_iters:int -> t
val compare : t -> t -> int
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 get_range_of_iterator : t -> t
val of_bool : Boolean.t -> t
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 is_false : t -> bool
val decr : t -> t
val decr_length : t -> t
val incr : t -> t
val set_lb : Bound.t -> t -> t
val set_lb_zero : t -> t
val neg : t -> t
val normalize : t -> t
val is_symbolic : t -> bool
val is_top : t -> bool
val get_symbols : t -> SymbolSet.t
val eq : t -> t -> bool
val le : lhs:t -> rhs:t -> bool
val lnot : t -> Boolean.t
val range : IBase.Location.t -> t -> ItvRange.t
val div : t -> t -> t
val div_const : t -> Z.t -> t
val minus : t -> t -> t
val mult : t -> t -> t
val mult_const : t -> Z.t -> t
val plus : t -> t -> t
val shiftlt : t -> t -> t
val shiftrt : t -> t -> t
val band_sem : t -> t -> t
val eq_sem : t -> t -> Boolean.t
val ge_sem : t -> t -> Boolean.t
val gt_sem : t -> t -> Boolean.t
val land_sem : t -> t -> Boolean.t
val le_sem : t -> t -> Boolean.t
val lor_sem : t -> t -> Boolean.t
val lt_sem : t -> t -> Boolean.t
val min_sem : ?use_minmax_bound:bool -> t -> t -> t
val max_sem : ?use_minmax_bound:bool -> t -> t -> t
val mod_sem : t -> t -> t
val ne_sem : t -> t -> Boolean.t
val prune_eq_zero : t -> t
val prune_ne_zero : t -> t
val prune_ge_one : t -> t
val prune_binop : IR.Binop.t -> t -> t -> t
val prune_eq : t -> t -> t
val prune_ne : t -> t -> t
val prune_lt : t -> t -> t
val prune_le : 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