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-beta-Cobalt.tar.gz
sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

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