Module E_ACSL.Interval

Interval inference for terms.

Compute the smallest interval that contains all the possible values of a given integer term. The interval of C variables is directly inferred from their C type. The interval of logic variables must be registered from outside before computing the interval of a term containing such variables (see module Interval.Env).

It implements Figure 3 of J. Signoles' JFLA'15 paper "Rester statique pour devenir plus rapide, plus précis et plus mince". Also implements a partial support for real numbers.

Example: consider a variable x of type int on a (strange) architecture in which values of type int belongs to the interval [-128;127] and a logic variable y which was registered in the environment with an interval [-32;31]. Then here are the intervals computed from the term 1+(x+1)/(y-64): 1. x in [128;127]; 2. x+1 in [129;128]; 3. y in [-32;31]; 4. y-64 in [-96;-33]; 5. (x+1)/(y-64) in [-3;3]; 6. 1+(x+1)/(y-64) in [-2;4]

Note: this is a partial wrapper on top of Ival.t, to which most functions are delegated.

Useful operations on intervals

val is_included : t -> t -> bool
val join : t -> t -> t
val meet : t -> t -> t
val widen : t -> t
  • returns

    the smallest interval containing a disjoint union of intervals

val is_singleton_int : t -> bool
val extract_ival : t -> Frama_c_kernel.Ival.t

assume Ival _ as argument

  • returns

    the smallest ikind that contains the given interval.

  • raises Cil.Not_representable

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

val interv_of_typ : Frama_c_kernel.Cil_types.typ -> t
  • returns

    the smallest interval which contains the given C type.

  • raises Is_a_real

    if the given type is a float type.

  • raises Not_a_number

    if the given type does not represent any number.

val extended_interv_of_typ : Frama_c_kernel.Cil_types.typ -> t
  • returns

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

  • raises Is_a_real

    if the given type is a float type.

  • raises Not_a_number

    if the given type does not represent any number.

  • returns

    the result of adding one to an interval. This is because when we have a condition x<t, we need to generate t+1

Inference system

val get_from_profile : profile:Analyses_datatype.Profile.t -> Frama_c_kernel.Cil_types.term -> t
  • returns

    the value computed by the interval inference phase

  • raises Is_a_real

    if the term is either a float or a real.

  • raises Not_a_number

    if the term does not represent any number.

  • returns

    the value computed by the interval inference phase, same as get_from_profile but with a full-fledged logic environment instead of a function profile

Interval processing

val infer_program : Frama_c_kernel.Cil_types.file -> unit

compute and store the type of all the terms that will be translated in a program

val preprocess_predicate : logic_env:Analyses_datatype.Logic_env.t -> Frama_c_kernel.Cil_types.predicate -> unit

compute and store the type of all the terms in a code annotation

val preprocess_code_annot : logic_env:Analyses_datatype.Logic_env.t -> Frama_c_kernel.Cil_types.code_annotation -> unit

compute and store the type of all the terms in a code annotation

val preprocess_term : logic_env:Analyses_datatype.Logic_env.t -> Frama_c_kernel.Cil_types.term -> unit
val clear : unit -> unit