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/frama-c-wp.core/Wp/Lang/index.html

Module Wp.LangSource

Low-Level Logic Terms and Predicates

Logic Language based on Qed

Library

Sourcetype library = string

Naming - Unique identifiers

Sourceval comp_init_id : Frama_c_kernel.Cil_types.compinfo -> string
Sourceval field_init_id : Frama_c_kernel.Cil_types.fieldinfo -> string
Sourceval lemma_id : string -> string

Symbols

Sourcetype datakind =
  1. | KValue
  2. | KInit
Sourcetype adt = private
  1. | Mtype of mdt
    (*

    External type

    *)
  2. | Mrecord of mdt * fields
    (*

    External record-type

    *)
  3. | Atype of Frama_c_kernel.Cil_types.logic_type_info
    (*

    Logic Type

    *)
  4. | Comp of Frama_c_kernel.Cil_types.compinfo * datakind
    (*

    C-code struct or union

    *)

A type is never registered in a Definition.t

Sourceand mdt = string extern

name to print to the provers

Sourceand 'a extern = {
  1. ext_id : int;
  2. ext_library : library;
    (*

    a library which it depends on

    *)
  3. ext_debug : string;
    (*

    just for printing during debugging

    *)
}
Sourceand fields = {
  1. mutable fields : field list;
}
Sourceand field = private
  1. | Mfield of mdt * fields * string * tau
  2. | Cfield of Frama_c_kernel.Cil_types.fieldinfo * datakind
Sourcetype t_builtin =
  1. | E_mdt of mdt
  2. | E_poly of tau list -> tau
Sourcetype lfun = private
  1. | ACSL of Frama_c_kernel.Cil_types.logic_info
    (*

    Registered in Definition.t, only

    *)
  2. | CTOR of Frama_c_kernel.Cil_types.logic_ctor_info
    (*

    Not registered in Definition.t directly converted/printed

    *)
  3. | FUN of lsymbol
    (*

    External or Generated logic symbol

    *)
Sourceand lsymbol = {
  1. m_category : lfun Qed.Logic.category;
  2. m_params : Qed.Logic.sort list;
  3. m_result : Qed.Logic.sort;
  4. m_typeof : tau option list -> tau;
  5. m_source : source;
  6. m_coloring : bool;
}
Sourceand source =
  1. | Generated of WpContext.context option * string
  2. | Extern of Qed.Engine.link extern
Sourceval mem_builtin_type : name:string -> bool
Sourceval is_builtin_type : name:string -> tau -> bool
Sourceval get_builtin_type : name:string -> adt
Sourceval datatype : library:string -> string -> adt
Sourceval record : link:string -> library:string -> (string * tau) list -> adt
Sourceval field : adt -> string -> field
Sourceval fields_of_adt : adt -> field list
Sourceval fields_of_tau : tau -> field list
Sourceval fields_of_field : field -> field list

Must not be a builtin

Sourcetype balance =
  1. | Nary
  2. | Left
  3. | Right
Sourceval on_lfun : (lfun -> unit) -> unit
Sourceval on_field : (field -> unit) -> unit
Sourceval extern_s : library:library -> ?link:Qed.Engine.link -> ?category:lfun Qed.Logic.category -> ?params:Qed.Logic.sort list -> ?sort:Qed.Logic.sort -> ?result:tau -> ?coloring:bool -> ?typecheck:(tau option list -> tau) -> string -> lfun
Sourceval extern_f : library:library -> ?link:Qed.Engine.link -> ?balance:balance -> ?category:lfun Qed.Logic.category -> ?params:Qed.Logic.sort list -> ?sort:Qed.Logic.sort -> ?result:tau -> ?coloring:bool -> ?typecheck:(tau option list -> tau) -> ('a, Format.formatter, unit, lfun) format4 -> 'a

balance just give a default when link is not specified

Sourceval extern_p : library:library -> ?bool:string -> ?prop:string -> ?link:Qed.Engine.link -> ?params:Qed.Logic.sort list -> ?coloring:bool -> unit -> lfun
Sourceval extern_fp : library:library -> ?params:Qed.Logic.sort list -> ?link:string -> ?coloring:bool -> string -> lfun
Sourceval generated_f : ?context:bool -> ?category:lfun Qed.Logic.category -> ?params:Qed.Logic.sort list -> ?sort:Qed.Logic.sort -> ?result:tau -> ?coloring:bool -> ('a, Format.formatter, unit, lfun) format4 -> 'a
Sourceval generated_p : ?context:bool -> ?coloring:bool -> string -> lfun
Sourceval extern_t : string -> link:string -> library:library -> mdt

Sorting and Typing

Sourceval tau_of_object : Ctypes.c_object -> tau
Sourceval tau_of_return : Frama_c_kernel.Cil_types.logic_type option -> tau
Sourceval tau_of_lfun : lfun -> tau option list -> tau
Sourceval tau_of_field : field -> tau
Sourceval tau_of_record : field -> tau
Sourceval init_of_object : Ctypes.c_object -> tau
Sourceval t_int : tau
Sourceval t_real : tau
Sourceval t_bool : tau
Sourceval t_prop : tau
Sourceval t_addr : unit -> tau
Sourceval t_float : Ctypes.c_float -> tau
Sourceval t_array : tau -> tau
Sourceval t_farray : tau -> tau -> tau
Sourceval t_datatype : adt -> tau list -> tau
Sourceval t_matrix : tau -> int -> tau
Sourceval pointer : tau Context.value

type of pointers

type of floats

Sourceval poly : string list Context.value

polymorphism

Sourceval builtin_types : (string -> t_builtin) Context.value
Sourceval parameters : (lfun -> Qed.Logic.sort list) -> unit

definitions

Sourceval name_of_lfun : lfun -> string
Sourceval name_of_field : field -> string
Sourceval context_of_lfun : lfun -> WpContext.context option

LFuns are unique by name and context

Sourceval is_coloring_lfun : lfun -> bool

Logic Formulae

Sourcemodule ADT : Qed.Logic.Data with type t = adt
Sourcemodule Field : Qed.Logic.Field with type t = field
Sourcemodule Fun : Qed.Logic.Function with type t = lfun
Sourceclass virtual idprinting : object ... end
Sourcemodule F : sig ... end
Sourcemodule N : sig ... end

simpler notation for writing F.term and F.pred

Fresh Variables and Constraints

Sourcetype gamma
Sourceval new_pool : ?copy:F.pool -> ?vars:F.Vars.t -> unit -> F.pool
Sourceval new_gamma : ?copy:gamma -> unit -> gamma
Sourceval local : ?pool:F.pool -> ?vars:F.Vars.t -> ?gamma:gamma -> ('a -> 'b) -> 'a -> 'b
Sourceval freshvar : ?basename:string -> F.tau -> F.var
Sourceval freshen : F.var -> F.var
Sourceval assume : F.pred -> unit
Sourceval without_assume : ('a -> 'b) -> 'a -> 'b
Sourceval hypotheses : gamma -> F.pred list
Sourceval get_pool : unit -> F.pool
Sourceval get_gamma : unit -> gamma
Sourceval has_gamma : unit -> bool
Sourceval get_hypotheses : unit -> F.pred list
Sourceval filter_hypotheses : F.var list -> F.pred list

Substitutions

Sourceval sigma : unit -> F.sigma

uses current pool

Sourceval alpha : unit -> F.sigma

freshen all variables

Sourceval subst : F.var list -> F.term list -> F.sigma

replace variables

Sourceval e_subst : (F.term -> F.term) -> F.term -> F.term

uses current pool

Sourceval p_subst : (F.term -> F.term) -> F.pred -> F.pred

uses current pool

Simplifiers

Sourceexception Contradiction
Sourceval is_literal : F.term -> bool
Sourceval iter_consequence_literals : (F.term -> unit) -> F.term -> unit

iter_consequence_literals assume_from_litteral hypothesis applies the function assume_from_litteral on literals that are a consequence of the hypothesis (i.e. in the hypothesis not (A && (B || C) ==> D), only A and not D are considered as consequence literals).

Sourceclass type simplifier = object ... end
Sourcemodule For_export : sig ... end

For why3_api but circular dependency