package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

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-Copper.tar.gz
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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 -> VCS.prover -> VCS.result
Sourceval get_results : t -> (VCS.prover * 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

Prover Interface

Sourceval prove : t -> ?config:VCS.config -> ?mode:VCS.mode -> ?start:(t -> unit) -> ?progress:(t -> string -> unit) -> ?result:(t -> VCS.prover -> VCS.result -> unit) -> VCS.prover -> 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 -> VCS.prover -> VCS.result -> unit) -> ?success:(t -> VCS.prover option -> unit) -> ?pool:Frama_c_kernel.Task.pool -> (VCS.mode * VCS.prover) 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 -> ?tip:bool -> t Frama_c_kernel.Bag.t -> unit

Run the provers with the command-line interface. If ~provers is set, it is used for computing the list of provers to spawn. If ~tip is set, it is used to compute the script execution mode.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct