Bounds.Bound
It makes a bound of Bound.MultB
, which represents a multiplication of two bounds. For example, MultB (1, x, y)
represents 1 + x × y
.
type eval_sym = t Symb.Symbol.eval
val pp_mark : markup:bool -> F.formatter -> t -> unit
val of_int : int -> t
val of_big_int : Z.t -> t
val minf : t
val mone : t
val zero : t
val one : t
val z255 : t
val pinf : t
val of_normal_path :
Symb.Symbol.make_t ->
unsigned:bool ->
?non_int:bool ->
Symb.SymbolPath.partial ->
t
val of_offset_path :
is_void:bool ->
Symb.Symbol.make_t ->
Symb.SymbolPath.partial ->
t
val of_length_path :
is_void:bool ->
Symb.Symbol.make_t ->
Symb.SymbolPath.partial ->
t
val of_modeled_path : Symb.Symbol.make_t -> 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 is_zero : t -> bool
val is_infty : t -> bool
val is_not_infty : t -> bool
val is_minf : t -> bool
val is_pinf : t -> bool
val is_symbolic : t -> bool
val xcompare : t IStdlib.PartialOrder.xcompare
val get_const : t -> Z.t option
val mult_const_l : Ints.NonZeroInt.t -> t -> t
val mult_const_u : Ints.NonZeroInt.t -> t -> t
val div_const_l : t -> Ints.NonZeroInt.t -> t option
val div_const_u : t -> Ints.NonZeroInt.t -> t option
val get_symbols : t -> Symb.SymbolSet.t
val has_void_ptr_symb : t -> bool
val subst_lb : t -> eval_sym -> t Absint.AbstractDomain.Types.bottom_lifted
val subst_ub : t -> eval_sym -> t Absint.AbstractDomain.Types.bottom_lifted
Removes positive symbols that are coming from length paths
val get_same_one_symbol : t -> t -> Symb.SymbolPath.t option
It returns a symbol s
when the two bounds are all linear expressions of the symbol 1⋅s
.
It returns true
when the two bounds are linear expressions of the same one symbol 1⋅s
.
val is_incr_of : Symb.SymbolPath.partial -> t -> bool
Check if bound
is path+1
when called is_incr_of path bound
val exists_str : f:(string -> bool) -> t -> bool