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. A
    Anne Pacalet
  36. V
    Valentin Perrelle
  37. G
    Guillaume Petiot
  38. D
    Dario Pinto
  39. V
    Virgile Prevosto
  40. A
    Armand Puccetti
  41. F
    Félix Ridoux
  42. V
    Virgile Robles
  43. M
    Muriel Roger
  44. J
    Julien Signoles
  45. N
    Nicolas Stouls
  46. K
    Kostyantyn Vorobyov
  47. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-27.0-beta-Cobalt.tar.gz
sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

doc/frama-c.kernel/Frama_c_kernel/Precise_locs/index.html

Module Frama_c_kernel.Precise_locs

This module provides transient datastructures that may be more precise than an Ival.t, Locations.Location_Bits.t and Locations.location respectively, typically for l-values such as t[i][j], p->t[i], etc. Those structures do not have a lattice structure, and cannot be stored as an abstract domain. However, they can be use to model more precisely read or write accesses to semi-imprecise l-values.

Precise offsets

type precise_offset
val pretty_offset : Format.formatter -> precise_offset -> unit
val equal_offset : precise_offset -> precise_offset -> bool
val offset_zero : precise_offset
val offset_bottom : precise_offset
val offset_top : precise_offset
val inject_ival : Ival.t -> precise_offset
val is_bottom_offset : precise_offset -> bool
val imprecise_offset : precise_offset -> Ival.t
val shift_offset_by_singleton : Integer.t -> precise_offset -> precise_offset
val shift_offset : Ival.t -> precise_offset -> precise_offset

Precise location_bits

type precise_location_bits
val pretty_loc_bits : Format.formatter -> precise_location_bits -> unit
val bottom_location_bits : precise_location_bits
val inject_location_bits : Locations.Location_Bits.t -> precise_location_bits
val combine_base_precise_offset : Base.t -> precise_offset -> precise_location_bits
val combine_loc_precise_offset : Locations.Location_Bits.t -> precise_offset -> precise_location_bits
val imprecise_location_bits : precise_location_bits -> Locations.Location_Bits.t

Precise locations

type precise_location
val equal_loc : precise_location -> precise_location -> bool
val loc_size : precise_location -> Int_Base.t
val make_precise_loc : precise_location_bits -> size:Int_Base.t -> precise_location
val imprecise_location : precise_location -> Locations.location
val loc_bottom : precise_location
val is_bottom_loc : precise_location -> bool
val loc_top : precise_location
val is_top_loc : precise_location -> bool
val fold : (Locations.location -> 'a -> 'a) -> precise_location -> 'a -> 'a
val enumerate_valid_bits : Locations.access -> precise_location -> Locations.Zone.t
val valid_cardinal_zero_or_one : for_writing:bool -> precise_location -> bool

Is the restriction of the given location to its valid part precise enough to perform a strong read, or a strong update.

val cardinal_zero_or_one : precise_location -> bool

Should not be used, valid_cardinal_zero_or_one is almost always more useful

val valid_part : Locations.access -> bitfield:bool -> precise_location -> precise_location

Overapproximation of the valid part of the given location (without any access, or for a read or write access). bitfield indicates whether the location may be the one of a bitfield, and is true by default. If it is set to false, the location is assumed to be byte aligned, and its offset (expressed in bits) is reduced to be congruent to 0 modulo 8.