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 Edit opam file Versions (30)

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. S
    Sylvain Chiron
  16. L
    Loïc Correnson
  17. J
    Julien Crétin
  18. P
    Pascal Cuoq
  19. Z
    Zaynah Dargaye
  20. B
    Basile Desloges
  21. J
    Jean-Christophe Filliâtre
  22. P
    Philippe Herrmann
  23. J
    Jordan Ischard
  24. M
    Maxime Jacquemin
  25. B
    Benjamin Jorge
  26. F
    Florent Kirchner
  27. A
    Alexander Kogtenkov
  28. R
    Remi Lazarini
  29. T
    Tristan Le Gall
  30. K
    Kilyan Le Gallic
  31. J
    Jean-Christophe Léchenet
  32. M
    Matthieu Lemerre
  33. D
    Dara Ly
  34. D
    David Maison
  35. C
    Claude Marché
  36. A
    André Maroneze
  37. T
    Thibault Martin
  38. F
    Fonenantsoa Maurica
  39. M
    Melody Méaulle
  40. B
    Benjamin Monate
  41. N
    Nicky Mouha
  42. Y
    Yannick Moy
  43. P
    Pierre Nigron
  44. A
    Anne Pacalet
  45. V
    Valentin Perrelle
  46. G
    Guillaume Petiot
  47. D
    Dario Pinto
  48. V
    Virgile Prevosto
  49. A
    Armand Puccetti
  50. F
    Félix Ridoux
  51. V
    Virgile Robles
  52. J
    Jan Rochel
  53. M
    Muriel Roger
  54. C
    Cécile Ruet-Cros
  55. J
    Julien Signoles
  56. F
    Fabien Siron
  57. N
    Nicolas Stouls
  58. H
    Hugo Thievenaz
  59. K
    Kostyantyn Vorobyov
  60. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-33.0-Arsenic.tar.gz
sha256=9c1cbffd28bb33c17a668107e39c96e4ae7378a3d8249f69b47afc7ee964e9b8

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

Module EvaSource

Eva public API.

Apart from Analysis and Results, all modules exported here are development interfaces which may change with each Frama-C release.

Main stable API

module Analysis : sig ... end

Run the analysis and check analysis status.

module Results : sig ... end

Main API to access the results of an analysis, such as the possible values of expressions and memory locations of lvalues at each program point.

Statistics

Sourcemodule Eva_perf : sig ... end

Statistics about the analysis performance.

module Statistics : sig ... end

Various statistics collected during an analysis.

Types used in Eva

module Eva_ast : sig ... end

AST used by Eva.

module Position : sig ... end

Position in the analysis

module Callstack : sig ... end

Types of callstack.

module Deps : sig ... end

Types for the memory dependencies of an expression or lvalue.

Configuration of the analysis

Sourcemodule Parameters : sig ... end

Command-line parameters of the analysis.

module Eva_annotations : sig ... end

Add local annotations to guide the analysis.

Sourcemodule Builtins : sig ... end

Register OCaml builtins to be used by the cvalue domain instead of analysing the body of some C functions.

Registration of new abstractions

Sourcemodule Eval : sig ... end

Various types used in abstract domain signature.

module Abstract_domain : sig ... end

Signature of abstract domains, inferring properties about the program during the analysis.

module Abstract_value : sig ... end

Signature of abstract numerical values, representing the set of possible values of an expression or lvalue. Used to exchange information between abstract domains.

module Abstract_location : sig ... end

Signature of abstract memory locations, representing the set of possible memory locations pointed to by an lvalue.

module Abstract_context : sig ... end

Signature of abstract state, which can be used to transfer information from states of abstract domains to abstract values.

module Unit_context : sig ... end

Empty context.

module Domain_builder : sig ... end

Automatic builders to complete abstract domains from different simplified interfaces.

module Simpler_domains : sig ... end

Simplified interfaces for abstract domains. Complete abstract domains can be built from these interfaces through the functors in Domain_builder.

module Simple_memory : sig ... end

Build a domain upon a value abstraction with a very simple memory model for scalar non-volatile variables.

module Domain : sig ... end

Register new abstract domains.

module Main_values : sig ... end

Common value abstractions shared by many abstract domains.

module Main_locations : sig ... end

Common location abstractions shared by many abstract domains.

Internal API

These modules are for internal use only. They may be modified or removed in future versions. Please contact us if you need features from these modules.

module Export : sig ... end

Generation of annotations.

module Assigns : sig ... end

Types and operations for the From plugin.

Sourcemodule Cvalue_callbacks : sig ... end

Register hooks called during the analysis with states of the cvalue domain.

module Logic_inout : sig ... end

Interpretation of predicates and assigns clauses for Inout and From plugins.

module Eva_results : sig ... end

Undocumented.

module Unit_tests : sig ... end

Unit testing.