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/qed/Qed/Logic/index.html

Module Qed.LogicSource

First Order Logic Definition

Sourcetype 'a element =
  1. | E_none
  2. | E_true
  3. | E_false
  4. | E_int of int
  5. | E_fun of 'a * 'a element list
Sourcetype 'a operator = {
  1. invertible : bool;
  2. associative : bool;
  3. commutative : bool;
  4. idempotent : bool;
  5. neutral : 'a element;
  6. absorbant : 'a element;
}

Algebraic properties for user operators.

Sourcetype 'a category =
  1. | Function
    (*

    logic function

    *)
  2. | Constructor
    (*

    f xs = g ys iff f=g && xi=yi

    *)
  3. | Injection
    (*

    f xs = f ys iff xi=yi

    *)
  4. | Operator of 'a operator

Algebraic properties for functions.

Sourcetype binder =
  1. | Forall
  2. | Exists
  3. | Lambda

Quantifiers and Binders

Sourcetype ('f, 'a) datatype =
  1. | Prop
  2. | Bool
  3. | Int
  4. | Real
  5. | Tvar of int
    (*

    ranges over 1..arity

    *)
  6. | Array of ('f, 'a) datatype * ('f, 'a) datatype
  7. | Record of ('f * ('f, 'a) datatype) list
  8. | Data of 'a * ('f, 'a) datatype list
Sourcetype sort =
  1. | Sprop
  2. | Sbool
  3. | Sint
  4. | Sreal
  5. | Sdata
  6. | Sarray of sort
Sourcetype maybe =
  1. | Yes
  2. | No
  3. | Maybe
Sourcemodule type Symbol = sig ... end

Ordered, hash-able and pretty-printable symbols

Sourcemodule type Data = sig ... end
Sourcemodule type Field = sig ... end
Sourcemodule type Function = sig ... end
Sourcemodule type Variable = sig ... end

Representation of Patterns, Functions and Terms

Sourcetype ('f, 'a) funtype = {
  1. result : ('f, 'a) datatype;
    (*

    Type of returned value

    *)
  2. params : ('f, 'a) datatype list;
    (*

    Type of parameters

    *)
}
Sourcetype ('f, 'a, 'd, 'x, 'b, 'e) term_repr =
  1. | True
  2. | False
  3. | Kint of Z.t
  4. | Kreal of Q.t
  5. | Times of Z.t * 'e
    (*

    mult: k1 * e2

    *)
  6. | Add of 'e list
    (*

    add: e11 + ... + e1n

    *)
  7. | Mul of 'e list
    (*

    mult: e11 * ... * e1n

    *)
  8. | Div of 'e * 'e
  9. | Mod of 'e * 'e
  10. | Eq of 'e * 'e
  11. | Neq of 'e * 'e
  12. | Leq of 'e * 'e
  13. | Lt of 'e * 'e
  14. | Aget of 'e * 'e
    (*

    access: array1idx2

    *)
  15. | Aset of 'e * 'e * 'e
    (*

    update: array1idx2 -> elem3

    *)
  16. | Acst of ('f, 'a) datatype * 'e
    (*

    constant array type -> value

    *)
  17. | Rget of 'e * 'f
  18. | Rdef of ('f * 'e) list
  19. | And of 'e list
    (*

    and: e11 && ... && e1n

    *)
  20. | Or of 'e list
    (*

    or: e11 || ... || e1n

    *)
  21. | Not of 'e
  22. | Imply of 'e list * 'e
    (*

    imply: (e11 && ... && e1n) ==> e2

    *)
  23. | If of 'e * 'e * 'e
    (*

    ite: if c1 then e2 else e3

    *)
  24. | Fun of 'd * 'e list
    (*

    Complete call (no partial app.)

    *)
  25. | Fvar of 'x
  26. | Bvar of int * ('f, 'a) datatype
  27. | Apply of 'e * 'e list
    (*

    High-Order application (Cf. binder)

    *)
  28. | Bind of binder * ('f, 'a) datatype * 'b

representation of terms. type arguments are the following:

  • 'z: representation of integral constants
  • 'f: representation of fields
  • 'a: representation of abstract data types
  • 'd: representation of functions
  • 'x: representation of free variables
  • 'b: representation of bound term (phantom type equal to 'e)
  • 'e: sub-expression
Sourcetype 'a affine = Z.t * (Z.t * 'a) list
Sourcemodule type Term = sig ... end