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

Maintainers

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

Sources

frama-c-29.0-beta-Copper.tar.gz
sha256=3ac8b38e0dab0e14d6ad0d244d8dfcfb17c912f661c77079096436f48377cf8a

doc/frama-c-eva.core/Eva/Logic_inout/index.html

Module Eva.Logic_inout

Functions used by the Inout and From plugins to interpret predicate and assigns clauses. This API may change according to these plugins development.

predicate_deps ~pre ~here p computes the logic dependencies needed to evaluate the predicate p in cvalue state here, in a function whose pre-state is pre. Returns None on either an evaluation error or on unsupported construct.

Returns the list of behaviors of the given function that are active for the given initial state.

Evaluation of the memory zone read by the \from part of an assigns clause, in the given cvalue state.

Evaluation of the memory zone written by an assigns clauses, in the given cvalue state.

type tlval_zones = {
  1. under : Frama_c_kernel.Locations.Zone.t;
    (*

    Under-approximation of the memory zone.

    *)
  2. over : Frama_c_kernel.Locations.Zone.t;
    (*

    Over-approximation of the memory zone.

    *)
  3. deps : Frama_c_kernel.Locations.Zone.t;
    (*

    Dependencies needed to evaluate the address.

    *)
}

Zones of an lvalue term of an assigns clause.

Evaluation of the memory zones and dependencies of an lvalue term from an assigns clause, in the given cvalue state for a read or write access.

Evaluate the assigns clauses of the given function in its given pre-state, and compare them with the dependencies computed by the from plugin. Emits warnings if needed, and sets statuses to the assigns clauses.

val accept_base : formals:bool -> locals:bool -> Frama_c_kernel.Kernel_function.t -> Frama_c_kernel.Base.t -> bool

accept_base ~formals ~locals kf b returns true if and only if b is:

  • a global
  • a formal or local of one of the callers of kf
  • a formal or local of kf and the corresponding argument is true.