package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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

Module `E_ACSL.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

val c_int : Analyses_types.number_ty

val ikind : Frama_c_kernel.Cil_types.ikind -> Analyses_types.number_ty

val fkind : Frama_c_kernel.Cil_types.fkind -> Analyses_types.number_ty

val gmpz : Analyses_types.number_ty

val rational : Analyses_types.number_ty

val nan : Analyses_types.number_ty

Useful operations over `number_ty`

exception Not_a_number

val typ_of_number_ty : Analyses_types.number_ty -> Frama_c_kernel.Cil_types.typ

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.

raises Not_a_number
in case of Nan.

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.

val join : 
  Analyses_types.number_ty ->
  Analyses_types.number_ty ->
  Analyses_types.number_ty

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.

val number_ty_bound_variable : 
  profile:Analyses_datatype.Profile.t ->
  (Frama_c_kernel.Cil_types.term
   * Frama_c_kernel.Cil_types.logic_var
   * Frama_c_kernel.Cil_types.term) ->
  Analyses_types.number_ty

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.

val get_number_ty : 
  logic_env:Analyses_datatype.Logic_env.t ->
  Frama_c_kernel.Cil_types.term ->
  Analyses_types.number_ty

returns
the infered type for the given term.

val get_effective_ty : 
  logic_env:Analyses_datatype.Logic_env.t ->
  Frama_c_kernel.Cil_types.term ->
  Analyses_types.number_ty

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

val get_typ : 
  logic_env:Analyses_datatype.Logic_env.t ->
  Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Cil_types.typ

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

val get_effective_typ : 
  logic_env:Analyses_datatype.Logic_env.t ->
  Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Cil_types.typ

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

val get_cast : 
  logic_env:Analyses_datatype.Logic_env.t ->
  Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Cil_types.typ option

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

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

val typ_of_lty : 
  Frama_c_kernel.Cil_types.logic_type ->
  Frama_c_kernel.Cil_types.typ

returns
the C type that correponds 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

val preprocess_rte : 
  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 : 
  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.

On This Page

Datatypes
Typing/types-related utils
Typing processing