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. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. A
    Anne Pacalet
  36. V
    Valentin Perrelle
  37. G
    Guillaume Petiot
  38. D
    Dario Pinto
  39. V
    Virgile Prevosto
  40. A
    Armand Puccetti
  41. F
    Félix Ridoux
  42. V
    Virgile Robles
  43. M
    Muriel Roger
  44. J
    Julien Signoles
  45. N
    Nicolas Stouls
  46. K
    Kostyantyn Vorobyov
  47. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-27.0-Cobalt.tar.gz
sha256=25885f89daa478aeafdd1e4205452c7a30695d4b3b3ee8fc98b4a9c5f83f79c2

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