package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install 

dune-project
 Dependency

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

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. P
    Pierre Nigron
  36. A
    Anne Pacalet
  37. V
    Valentin Perrelle
  38. G
    Guillaume Petiot
  39. D
    Dario Pinto
  40. V
    Virgile Prevosto
  41. A
    Armand Puccetti
  42. F
    Félix Ridoux
  43. V
    Virgile Robles
  44. J
    Jan Rochel
  45. M
    Muriel Roger
  46. J
    Julien Signoles
  47. N
    Nicolas Stouls
  48. K
    Kostyantyn Vorobyov
  49. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-28.1-Nickel.tar.gz
sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

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

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 infered type for the given term.

  • returns

    the necessary cast infered by the type system if any, or the type infered 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 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

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.