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-wp.core/Wp/VC/index.html

Module Wp.VCSource

WP Proof Obligation Generator and Management

Proof Obligations

Sourcetype t

elementary proof obligation

Sourceval get_id : t -> string
Sourceval get_model : t -> WpContext.model
Sourceval get_scope : t -> WpContext.scope
Sourceval get_context : t -> WpContext.context
Sourceval get_description : t -> string
Sourceval get_property : t -> Frama_c_kernel.Property.t
Sourceval get_result : t -> Prover.t -> VCS.result
Sourceval get_results : t -> (Prover.t * VCS.result) list
Sourceval get_sequent : t -> Conditions.sequent
Sourceval get_formula : t -> Lang.F.pred
Sourceval is_trivial : t -> bool
Sourceval is_valid : t -> bool

One prover at least returns a valid verdict.

Sourceval has_unknown : t -> bool

At least one non-valid verdict.

Sourceval is_passed : t -> bool

Same as is_valid for non-smoke tests. For smoke-tests, same as is_unknown.

Database

Notice that a property or a function have no proof obligation until you explicitly generate them via the generate_xxx functions below.

Sourceval clear : unit -> unit

List of proof obligations computed for a given property. Might be empty if you don't have used one of the generators below.

Sourceval remove : Frama_c_kernel.Property.t -> unit
Sourceval iter_ip : (t -> unit) -> Frama_c_kernel.Property.t -> unit
Sourceval iter_kf : (t -> unit) -> ?bhv:string list -> Frama_c_kernel.Kernel_function.t -> unit

Generators

The generated VCs are also added to the database, so they can be accessed later. The default value for model is what has been given on the command line (-wp-model option)

Sourceval generate_ip : ?model:string -> Frama_c_kernel.Property.t -> t Frama_c_kernel.Bag.t
Sourceval generate_kf : ?model:string -> ?bhv:string list -> ?prop:string list -> Frama_c_kernel.Kernel_function.t -> t Frama_c_kernel.Bag.t
Sourceval generate_call : ?model:string -> Frama_c_kernel.Cil_types.stmt -> t Frama_c_kernel.Bag.t
Sourceval generate_all : ?model:string -> ?bhv:string list -> ?prop:string list -> unit -> t Frama_c_kernel.Bag.t
  • since 33.0-Arsenic

Prover Interface

Sourceval prove : t -> ?config:VCS.config -> ?mode:Prover.InteractiveMode.t -> ?start:(t -> unit) -> ?progress:(t -> string -> unit) -> ?result:(t -> Prover.t -> VCS.result -> unit) -> Prover.t -> bool Frama_c_kernel.Task.task

Returns a ready-to-schedule task.

Sourceval spawn : t -> ?config:VCS.config -> ?start:(t -> unit) -> ?progress:(t -> string -> unit) -> ?result:(t -> Prover.t -> VCS.result -> unit) -> ?success:(t -> Prover.t option -> unit) -> (Prover.InteractiveMode.t * Prover.t) list -> unit

Same as prove but schedule the tasks into the global server returned by server function below.

The first succeeding prover cancels the other ones.

Sourceval server : ?procs:int -> unit -> Frama_c_kernel.Task.server

Default number of parallel tasks is given by -wp-par command-line option. The returned server is global to Frama-C, but the number of parallel task allowed will be updated to fit the ~procs or command-line options.

Sourceval command : ?provers:Why3.Whyconf.prover list -> ?interactive_mode:Prover.InteractiveMode.t -> ?scripts:bool -> ?strategies:bool -> t Frama_c_kernel.Bag.t -> unit

Run proofs on the provided bag of WPOs. The defaults for the different optional variables are obtained from the current configuration status. That is, the command line when in CLI mode, or what has been configured so far by the user in the GUI mode.

  • before 33.0-Arsenic

    only provers and tip were configurable and the default were computed from the CLI.