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. S
    Sylvain Chiron
  16. L
    Loïc Correnson
  17. J
    Julien Crétin
  18. P
    Pascal Cuoq
  19. Z
    Zaynah Dargaye
  20. B
    Basile Desloges
  21. J
    Jean-Christophe Filliâtre
  22. P
    Philippe Herrmann
  23. M
    Maxime Jacquemin
  24. B
    Benjamin Jorge
  25. F
    Florent Kirchner
  26. A
    Alexander Kogtenkov
  27. R
    Remi Lazarini
  28. T
    Tristan Le Gall
  29. K
    Kilyan Le Gallic
  30. J
    Jean-Christophe Léchenet
  31. M
    Matthieu Lemerre
  32. D
    Dara Ly
  33. D
    David Maison
  34. C
    Claude Marché
  35. A
    André Maroneze
  36. T
    Thibault Martin
  37. F
    Fonenantsoa Maurica
  38. M
    Melody Méaulle
  39. B
    Benjamin Monate
  40. Y
    Yannick Moy
  41. P
    Pierre Nigron
  42. A
    Anne Pacalet
  43. V
    Valentin Perrelle
  44. G
    Guillaume Petiot
  45. D
    Dario Pinto
  46. V
    Virgile Prevosto
  47. A
    Armand Puccetti
  48. F
    Félix Ridoux
  49. V
    Virgile Robles
  50. J
    Jan Rochel
  51. M
    Muriel Roger
  52. C
    Cécile Ruet-Cros
  53. J
    Julien Signoles
  54. N
    Nicolas Stouls
  55. K
    Kostyantyn Vorobyov
  56. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-31.0-Gallium.tar.gz
sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-wp.core/Wp/WpPropId/index.html

Module Wp.WpPropIdSource

Beside the property identification, it can be found in different contexts depending on which part of the computation is involved. For instance, properties on loops are split in 2 parts : establishment and preservation.

Sourcetype prop_id

Property.t information and kind of PO (establishment, preservation, etc)

returns the annotation which lead to the given PO.

Sourceval doomed_if_valid : prop_id -> Frama_c_kernel.Property.t list

Properties that are False-if-unreachable in case the PO is valid.

Sourceval unreachable_if_valid : prop_id -> Frama_c_kernel.Property.other_loc

Stmt that is unreachable in case the PO is valid.

Sourceval compare_prop_id : prop_id -> prop_id -> int
Sourceval tactical : gid:string -> prop_id
Sourceval is_check : prop_id -> bool
Sourceval is_tactic : prop_id -> bool
Sourceval is_assigns : prop_id -> bool
Sourceval is_requires : Frama_c_kernel.Property.t -> bool
Sourceval is_loop_preservation : prop_id -> Frama_c_kernel.Cil_types.stmt option
Sourceval is_smoke_test : prop_id -> bool
Sourceval select_default : prop_id -> bool

test if the prop_id does not have a no_wp: in its name(s).

Sourceval select_by_name : string list -> prop_id -> bool

test if the prop_id has to be selected for the asked names.

Sourceval select_for_behaviors : string list -> prop_id -> bool

test if the prop_id has to be selected for the asked behavior names.

Sourceval select_call_pre : Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Property.t option -> prop_id -> bool

test if the prop_id has to be selected when we want to select the call.

Sourceval ident_names : string list -> string list

From a list of names (of an identified terms), returns usable names.

Sourceval prop_id_keys : prop_id -> string list * string list
Sourceval get_propid : prop_id -> string

Unique identifier of prop_id

Sourceval pp_propid : Format.formatter -> prop_id -> unit

Print unique id of prop_id

Sourceval user_pred_names : Frama_c_kernel.Cil_types.toplevel_predicate -> string list
Sourceval user_bhv_names : Frama_c_kernel.Property.identified_property -> string list
Sourceval user_prop_names : Frama_c_kernel.Property.identified_property -> string list
Sourceval are_selected_names : string list -> string list -> bool

are_selected_names asked names checks if names of a property are selected according to asked names.

Sourceval pretty : Format.formatter -> prop_id -> unit
Sourceval pretty_local : Format.formatter -> prop_id -> unit
Sourceval label_of_prop_id : prop_id -> string

Short description of the kind of PO

Sourceval string_of_termination_kind : Frama_c_kernel.Cil_types.termination_kind -> string

TODO: should probably be somewhere else

Sourceval mk_smoke : Frama_c_kernel.Cil_types.kernel_function -> id:string -> ?doomed:Frama_c_kernel.Property.t list -> ?unreachable:Frama_c_kernel.Cil_types.stmt -> unit -> prop_id

Invariant establishment and preservation

Invariant establishment and preservation, in this order

Invariant used as hypothesis

Variant decrease

Variant positive

Variant for

\from property of loop assigns. Must not be FromAny

\from property of function or statement behavior assigns. Must not be FromAny

\from property of function behavior assigns. Must not be FromAny. The boolean indicate whether the function has exit node or not.

Sourceval mk_disj_bhv_id : (Frama_c_kernel.Cil_types.kernel_function * Frama_c_kernel.Cil_types.kinstr * string list * string list) -> prop_id

disjoint behaviors property. See Property.ip_of_disjoint for more information

Sourceval mk_compl_bhv_id : (Frama_c_kernel.Cil_types.kernel_function * Frama_c_kernel.Cil_types.kinstr * string list * string list) -> prop_id

complete behaviors property. See Property.ip_of_complete for more information

axiom identification

function assigns The boolean indicate whether the function has exit node or not.

Sourceval mk_post_id : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.kinstr -> Frama_c_kernel.Cil_types.funbehavior -> (Frama_c_kernel.Cil_types.termination_kind * Frama_c_kernel.Cil_types.identified_predicate) -> prop_id
Sourceval mk_stmt_post_id : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.funbehavior -> (Frama_c_kernel.Cil_types.termination_kind * Frama_c_kernel.Cil_types.identified_predicate) -> prop_id
Sourceval mk_fct_post_id : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.funbehavior -> (Frama_c_kernel.Cil_types.termination_kind * Frama_c_kernel.Cil_types.identified_predicate) -> prop_id

mk_call_pre_id called_kf s_call called_pre

Sourcetype a_kind =
  1. | LoopAssigns
  2. | StmtAssigns
Sourcetype assigns_desc = private {
  1. a_label : Clabels.c_label;
  2. a_stmt : Frama_c_kernel.Cil_types.stmt option;
  3. a_kind : a_kind;
  4. a_assigns : Frama_c_kernel.Cil_types.assigns;
}
Sourceval pp_assigns_desc : Format.formatter -> assigns_desc -> unit
Sourcetype assigns_info = prop_id * assigns_desc
Sourceval assigns_info_id : assigns_info -> prop_id
Sourcetype assigns_full_info = private
  1. | AssignsLocations of assigns_info
  2. | AssignsAny of assigns_desc
  3. | NoAssignsInfo
Sourceval empty_assigns_info : assigns_full_info
Sourceval mk_assigns_info : prop_id -> assigns_desc -> assigns_full_info
Sourceval mk_stmt_any_assigns_info : Frama_c_kernel.Cil_types.stmt -> assigns_full_info
Sourceval mk_kf_any_assigns_info : unit -> assigns_full_info
Sourceval mk_loop_any_assigns_info : Frama_c_kernel.Cil_types.stmt -> assigns_full_info
Sourceval pp_assign_info : string -> Format.formatter -> assigns_full_info -> unit
Sourceval mk_stmt_assigns_any_desc : Frama_c_kernel.Cil_types.stmt -> assigns_desc
Sourceval mk_kf_assigns_desc : Frama_c_kernel.Cil_types.from list -> assigns_desc
Sourceval mk_init_assigns : assigns_desc
Sourceval is_call_assigns : assigns_desc -> bool
Sourceval pp_axiom_info : Format.formatter -> axiom_info -> unit
Sourceval pred_info_id : pred_info -> prop_id
Sourceval pp_pred_of_pred_info : Format.formatter -> pred_info -> unit
Sourceval pp_pred_info : Format.formatter -> pred_info -> unit
Sourceval split_bag : (prop_id -> 'a -> unit) -> prop_id -> 'a Frama_c_kernel.Bag.t -> unit
Sourceval split_map : (prop_id -> 'a -> 'b) -> prop_id -> 'a list -> 'b list
Sourceval mk_part : prop_id -> (int * int) -> prop_id

mk_part pid (k, n) build the identification for the k/n part of pid.

Sourceval parts_of_id : prop_id -> (int * int) option

get the 'part' information.

Sourceval subproofs : prop_id -> int

How many subproofs

Sourceval subproof_idx : prop_id -> int

subproof index of this propr_id

Sourceval get_induction : prop_id -> Frama_c_kernel.Cil_types.stmt option
Sourcetype proof

A proof accumulator for a set of related prop_id

Sourceval create_proof : prop_id -> proof

to be used only once for one of the related prop_id

Sourceval add_proof : proof -> prop_id -> Frama_c_kernel.Property.t list -> unit

accumulate in the proof the partial proof for this prop_id

Sourceval add_invalid_proof : proof -> unit

add an invalid proof result ; can not revert a complete proof

Sourceval is_composed : proof -> bool

whether a proof needs several lemma to be complete

Sourceval is_proved : proof -> bool

whether all partial proofs have been accumulated or not

Sourceval is_invalid : proof -> bool

whether an invalid proof result has been registered or not

Sourceval dependencies : proof -> Frama_c_kernel.Property.t list
Sourceval filter_status : prop_id -> bool