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. K
    Kilyan Le Gallic
  28. J
    Jean-Christophe Léchenet
  29. M
    Matthieu Lemerre
  30. D
    Dara Ly
  31. D
    David Maison
  32. C
    Claude Marché
  33. A
    André Maroneze
  34. T
    Thibault Martin
  35. F
    Fonenantsoa Maurica
  36. M
    Melody Méaulle
  37. B
    Benjamin Monate
  38. Y
    Yannick Moy
  39. P
    Pierre Nigron
  40. A
    Anne Pacalet
  41. V
    Valentin Perrelle
  42. G
    Guillaume Petiot
  43. D
    Dario Pinto
  44. V
    Virgile Prevosto
  45. A
    Armand Puccetti
  46. F
    Félix Ridoux
  47. V
    Virgile Robles
  48. J
    Jan Rochel
  49. M
    Muriel Roger
  50. C
    Cécile Ruet-Cros
  51. J
    Julien Signoles
  52. N
    Nicolas Stouls
  53. K
    Kostyantyn Vorobyov
  54. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-30.0-Zinc.tar.gz
sha256=3ac0f995261ec829a7bd042bf70fc29ac6379029eb9df30bcc044748eb4d2a56

doc/qed/Qed/Export_whycore/Make/class-engine/index.html

Class Make.engineSource

method sanitize : string -> string
method virtual datatype : T.ADT.t -> string
method virtual field : T.Field.t -> string
method env : Env.t
method set_env : Env.t -> unit
method marks : Env.t * T.marks
method lookup : T.t -> Qed.Engine.scope
method scope : Env.t -> (unit -> unit) -> unit
method local : (unit -> unit) -> unit
method global : (unit -> unit) -> unit
method t_int : string
method t_real : string
method t_bool : string
method t_prop : string
method virtual t_atomic : T.tau -> bool
method pp_tvar : int Qed.Plib.printer
method virtual pp_array : T.tau Qed.Plib.printer
method virtual pp_farray : T.tau Qed.Plib.printer2
method virtual pp_datatype : T.ADT.t -> T.tau list Qed.Plib.printer
method pp_subtau : T.tau Qed.Plib.printer
method mode : Qed.Engine.mode
method with_mode : Qed.Engine.mode -> (Qed.Engine.mode -> unit) -> unit
method virtual e_true : Qed.Engine.cmode -> string
method virtual e_false : Qed.Engine.cmode -> string
method virtual pp_int : Qed.Engine.amode -> Z.t Qed.Plib.printer
method virtual pp_real : Q.t Qed.Plib.printer
method virtual is_atomic : T.term -> bool
method virtual op_spaced : string -> bool
method virtual callstyle : Qed.Engine.callstyle
method pp_apply : Qed.Engine.cmode -> T.term -> T.term list Qed.Plib.printer
method pp_fun : Qed.Engine.cmode -> T.Fun.t -> T.term list Qed.Plib.printer
method op_scope : Qed.Engine.amode -> string option
method virtual op_real_of_int : Qed.Engine.op
method virtual op_add : Qed.Engine.amode -> Qed.Engine.op
method virtual op_sub : Qed.Engine.amode -> Qed.Engine.op
method virtual op_mul : Qed.Engine.amode -> Qed.Engine.op
method virtual op_div : Qed.Engine.amode -> Qed.Engine.op
method virtual op_mod : Qed.Engine.amode -> Qed.Engine.op
method virtual op_minus : Qed.Engine.amode -> Qed.Engine.op
method pp_times : Format.formatter -> Z.t -> T.term -> unit
method virtual op_equal : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_noteq : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_eq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method virtual op_neq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method virtual op_lt : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method virtual op_leq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method virtual pp_array_cst : Format.formatter -> T.tau -> T.term -> unit
method pp_array_get : Format.formatter -> T.term -> T.term -> unit
method pp_array_set : Format.formatter -> T.term -> T.term -> T.term -> unit
method virtual op_record : string * string
method pp_get_field : Format.formatter -> T.term -> T.Field.t -> unit
method pp_def_fields : T.record Qed.Plib.printer
method virtual op_not : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_and : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_or : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_imply : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_equiv : Qed.Engine.cmode -> Qed.Engine.op
method pp_not : T.term Qed.Plib.printer
method pp_imply : Format.formatter -> T.term list -> T.term -> unit
method pp_equal : T.term Qed.Plib.printer2
method pp_noteq : T.term Qed.Plib.printer2
method virtual pp_conditional : Format.formatter -> T.term -> T.term -> T.term -> unit
method virtual pp_forall : T.tau -> string list Qed.Plib.printer
method virtual pp_intros : T.tau -> string list Qed.Plib.printer
method virtual pp_exists : T.tau -> string list Qed.Plib.printer
method pp_lambda : (string * T.tau) list Qed.Plib.printer
method bind : T.var -> string
method find : T.var -> string
method virtual pp_let : Format.formatter -> Qed.Engine.pmode -> string -> T.term -> unit
method shared : T.term -> bool
method shareable : T.term -> bool
method subterms : (T.term -> unit) -> T.term -> unit
method pp_atom : T.term Qed.Plib.printer
method pp_flow : T.term Qed.Plib.printer
method pp_repr : T.term Qed.Plib.printer
method pp_tau : T.tau Qed.Plib.printer
method pp_var : string Qed.Plib.printer
method pp_term : T.term Qed.Plib.printer
method pp_prop : T.term Qed.Plib.printer
method pp_sort : T.term Qed.Plib.printer
method pp_expr : T.tau -> T.term Qed.Plib.printer
method pp_param : (string * T.tau) Qed.Plib.printer
method virtual pp_trigger : trigger Qed.Plib.printer
method virtual pp_declare_adt : Format.formatter -> T.ADT.t -> int -> unit
method virtual pp_declare_def : Format.formatter -> T.ADT.t -> int -> T.tau -> unit
method virtual pp_declare_sum : Format.formatter -> T.ADT.t -> int -> (T.Fun.t * T.tau list) list -> unit
method pp_declare_symbol : Qed.Engine.cmode -> Format.formatter -> T.Fun.t -> unit
method declare_type : Format.formatter -> T.ADT.t -> int -> typedef -> unit
method declare_axiom : Format.formatter -> string -> T.var list -> trigger list list -> T.term -> unit
method declare_prop : kind:string -> Format.formatter -> string -> T.var list -> trigger list list -> T.term -> unit