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/Parameters/index.html

Module Eva.ParametersSource

Command-line parameters of the analysis.

Meta-option

Domains

module DomainsFunction : Frama_c_kernel.Parameter_sig.Multiple_map with type key = string and type value = Frama_c_kernel.Kernel_function.t * Eva__.Domain_mode.mode

Precision

State partitioning

module SplitReturnFunction : Frama_c_kernel.Parameter_sig.Map with type key = Frama_c_kernel.Cil_types.kernel_function and type value = Eva__.Split_strategy.split_strategy
module SplitReturn : Frama_c_kernel.Parameter_sig.Custom with type t = Eva__.Split_strategy.split_strategy

Performance

Initial context of the analysis

module InitializationPaddingGlobals : Frama_c_kernel.Parameter_sig.S with type t = [ `Initialized | `Uninitialized | `MaybeInitialized ]

Builtins

Analysis behavior

Non standard alarms

module WarnPointerComparison : Frama_c_kernel.Parameter_sig.S with type t = [ `All | `Pointer | `None ]

Verbosity and outputs

Experimental

Sourcetype descending_strategy =
  1. | NoIteration
  2. | FullIteration
  3. | ExitIteration

Utility functions

Sourceval enabled_domains : unit -> (string * string) list

Returns the list (name, descr) of currently enabled abstract domains.

Sourceval use_builtin : Frama_c_kernel.Cil_types.kernel_function -> string -> unit

use_builtin kf name instructs the analysis to use the builtin name to interpret calls to function kf. Raises Not_found if there is no builtin of name name.

Sourceval use_global_value_partitioning : Frama_c_kernel.Cil_types.varinfo -> unit

use_global_value_partitioning vi instructs the analysis to use value partitioning on the global variable vi.

Sourceval change_correctness : unit -> unit

This function should be called whenever the correctness of the analysis is externally changed through the Eva API, to ensure that the property statuses emitted by Eva are properly reset.

Internal use only

Sourceval configure_precision : unit -> unit
Sourceval parameters_correctness : Frama_c_kernel.Typed_parameter.t list

List of parameters having an impact on the correctness of the analysis.

Sourceval parameters_tuning : Frama_c_kernel.Typed_parameter.t list

List of parameters having an impact only on the analysis precision.

Sourceval register_builtin : string -> unit

Registers available cvalue builtins for the -eva-builtin option.

Sourceval unregister_builtin : string -> unit

Unregister a cvalue builtin.

Sourceval register_domain : name:string -> descr:string -> priority:int -> unit

Registers available domain names for the -eva-domains option.