Frama-C:
Plug-ins:
Libraries:

Frama-C API - Typing

Type system which computes the smallest C type that may contain all the possible values of a given integer term or predicate. Also compute the required casts. It is based on interval inference of module Interval.

It implement Figure 4 of J. Signoles' JFLA'15 paper "Rester statique pour devenir plus rapide, plus précis et plus mince".

Example: consider a variable x of type int and a variable y of type char on a (strange) architecture in which values of type int belongs to the interval [-128;127] and values of type char belongs to the interval [-32;31], while there are no other integral types. Then here are some information computed from the term 1+(x+1)/(y-64) by the type system: 1. x+1 must be a GMP (because of the potential overflow) 2. consequently x, which is an int, must be coerced into a GMP and the same for the number 1 in this addition. 3. y-64 can be computed in an int (because the result belongs to the interval [-96;-33]). 4. (x+1)/(y-64) must be a GMP operation because the numerator is a GMP (see 1.). Consequently y-64 must be coerced into a GMP too. However, the result belongs to the interval [-3;3] and thus can be safely coerced to an int. 5. Consequently the addition of the toplevel term 1+(x+1)/(y-64) can safely be computed in int: its result belongs to [-2;4].

Datatypes

Smart constructors

Useful operations over number_ty

exception Not_a_number
  • returns

    the C type corresponding to an number_ty. That is Gmp.z_t () for Gmpz, Real.t () for Real and TInt(ik, [[]]) for Ctype ik.

val number_ty_of_typ : post:bool -> Frama_c_kernel.Cil_types.typ -> Analyses_types.number_ty

Reverse of typ_of_number_ty number_ty_of_typ ~post ty return the number_ty corresponding to a C type. post indicates if the type is before or after the typing phase. The GMP types will be recognized only in a post-typing phase.

number_ty is a join-semi-lattice if you do not consider Other. If there is no Other in argument, this function computes the join of this semi-lattice. If one of the argument is Other, the function assumes that the other argument is also Other. In this case, the result is Other.

return the type of a quantified logic variable

val clear : unit -> unit

Typing

Remove all the previously computed types.

Getters

Below, the functions assume that either type_term or type_named_predicate has been previously computed for the given term or predicate.

  • returns

    the inferred type for the given term.

  • returns

    the necessary cast inferred by the type system if any, or the type inferred for the given term otherwise

Get the type which the given term must be generated to.

Get the type which the given term must be converted to if any, and the translation type otherwise

Get the type which the given term must be converted to (if any).

Register that the given term has the given type in the given context (if any). No verification is done.

  • returns

    the C type that corresponds to the given logic type.

Typing processing

val type_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 types of all the terms in a given predicate

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

val preprocess_term : use_gmp_opt:bool -> ?ctx:Analyses_types.number_ty -> logic_env:Analyses_datatype.Logic_env.t -> Frama_c_kernel.Cil_types.term -> unit

Compute the type of each subterm of the given term in the given context. If use_gmp_opt is false, then the conversion to the given context is done even if -e-acsl-gmp-only is set.