Module `E_ACSL.Interval_utils`

val is_included : Analyses_types.ival -> Analyses_types.ival -> bool

val join : Analyses_types.ival -> Analyses_types.ival -> Analyses_types.ival

val meet : Analyses_types.ival -> Analyses_types.ival -> Analyses_types.ival

val is_singleton_int : Analyses_types.ival -> bool

val bottom : Analyses_types.ival

val top_ival : Analyses_types.ival

val singleton : Frama_c_kernel.Integer.t -> Analyses_types.ival

val singleton_of_int : int -> Analyses_types.ival

val ival : 
  Frama_c_kernel.Integer.t ->
  Frama_c_kernel.Integer.t ->
  Analyses_types.ival

val interv_of_unknown_block : Analyses_types.ival lazy_t

val unify : Analyses_types.ival -> Analyses_types.ival

returns
the smallest interval containing a disjoint union of intervals

val lift_unop : 
  (Frama_c_kernel.Ival.t -> Frama_c_kernel.Ival.t) ->
  Analyses_types.ival ->
  Analyses_types.ival

lift a unary operation on IVal.t to the type ival

val lift_arith_binop : 
  (Frama_c_kernel.Ival.t -> Frama_c_kernel.Ival.t -> Frama_c_kernel.Ival.t) ->
  Analyses_types.ival ->
  Analyses_types.ival ->
  Analyses_types.ival

Lift a binary operation on IVal.t to the type ival

val extract_ival : Analyses_types.ival -> Frama_c_kernel.Ival.t

assume Ival _ as argument

val ival_of_ikind : Frama_c_kernel.Cil_types.ikind -> Frama_c_kernel.Ival.t

val interv_of_typ : Frama_c_kernel.Cil_types.typ -> Analyses_types.ival

returns
the smallest interval which contains the given C type.

val extended_interv_of_typ : 
  Frama_c_kernel.Cil_types.typ ->
  Analyses_types.ival

returns
the interval n..m+1 when interv_of_typ returns n..m. It is in particular useful for computing bounds of quantified variables.

val interv_of_logic_typ : 
  Frama_c_kernel.Cil_types.logic_type ->
  Analyses_types.ival

returns
the smallest interval which contains the given logic type.

exception Not_representable_ival

raised by ikind_of_ival.

since 28.0-Nickel

val ikind_of_ival : Frama_c_kernel.Ival.t -> Frama_c_kernel.Cil_types.ikind

returns
the smallest ikind that contains the given interval.

raises Not_representable_ival
if the given interval does not fit into any C integral type.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-e-acsl.core/E_ACSL/Interval_utils/index.html

Module `E_ACSL.Interval_utils`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-e-acsl.core/E_ACSL/Interval_utils/index.html

Module E_ACSL.Interval_utils

Module `E_ACSL.Interval_utils`