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-beta-Zinc.tar.gz
sha256=93a291a8764644df2f3618d7ea18258b5fbe0912ec98dfdfd180967afdf24474

doc/frama-c-slicing.core/Slicing/Api/Select/index.html

Module Api.SelectSource

Slicing selections.

Internal selection.

For dynamic type checking.

Set of colored selections.

For dynamic type checking.

Selectors.

Sourceval empty_selects : set

Empty selection.

Statement selectors.

To select a statement.

To select a statement reachability. Note: add also a transparent selection on the whole statement.

To select rw accesses to lvalues (given as string) related to a statement. Variables of ~rd and ~wr string are bounded relatively to the whole scope of the function. The interpretation of the address of the lvalues is done just before the execution of the statement ~eval. The selection preserve the ~rd and ~wr accesses contained into the statement ki. Note: add also a transparent selection on the whole statement.

To select lvalues (given as string) related to a statement. Variables of lval_str string are bounded relatively to the whole scope of the function. The interpretation of the address of the lvalue is done just before the execution of the statement ~eval. The selection preserve the value of these lvalues before or after (c.f. boolean ~before) the statement ki. Note: add also a transparent selection on the whole statement.

To select a zone value related to a statement. Note: add also a transparent selection on the whole statement.

To select a predicate value related to a statement. Note: add also a transparent selection on the whole statement.

To select a predicate value related to a statement. Note: add also a transparent selection on the whole statement.

To select the annotations related to a statement. Note: add also a transparent selection on the whole statement.

Sourceval select_stmt_annots : set -> Mark.t -> spare:bool -> threat:bool -> user_assert:bool -> slicing_annot:bool -> loop_inv:bool -> loop_var:bool -> Frama_c_kernel.Cil_datatype.Stmt.t -> Frama_c_kernel.Cil_types.kernel_function -> set

To select the annotations related to a statement. Note: add also a transparent selection on the whole statement.

Function selectors.

To select rw accesses to lvalues (given as a string) related to a function. Variables of ~rd and ~wr string are bounded relatively to the whole scope of the function. The interpretation of the address of the lvalues is done just before the execution of the statement ~eval. The selection preserve the value of these lvalues into the whole project.

To select lvalues (given as a string) related to a function. Variables of lval_str string are bounded relatively to the scope of the first statement of kf. The interpretation of the address of the lvalues is done just before the execution of the first statement kf. The selection preserve the value of these lvalues before execution of the return statement.

To select an output zone related to a function.

Sourceval select_func_return : set -> spare:bool -> Frama_c_kernel.Cil_types.kernel_function -> set

To select the function result (returned value).

Sourceval select_func_calls_to : set -> spare:bool -> Frama_c_kernel.Cil_types.kernel_function -> set

To select every calls to the given function, i.e. the call keeps its semantics in the slice.

Sourceval select_func_calls_into : set -> spare:bool -> Frama_c_kernel.Cil_types.kernel_function -> set

To select every calls to the given function without the selection of its inputs/outputs.

Sourceval select_func_annots : set -> Mark.t -> spare:bool -> threat:bool -> user_assert:bool -> slicing_annot:bool -> loop_inv:bool -> loop_var:bool -> Frama_c_kernel.Cil_types.kernel_function -> set

To select the annotations related to a function.

Pdg selectors.

Internal use only

The function related to an internal selection.

Sourceval merge_internal : t -> t -> t

The function related to an internal selection.

Sourceval add_to_selects_internal : t -> set -> set
Sourceval iter_selects_internal : (t -> unit) -> set -> unit
Sourceval fold_selects_internal : ('a -> t -> 'a) -> 'a -> set -> 'a

Internally used to select a statement :

  • if is_ctrl_mark m, propagate ctrl_mark on ctrl dependencies of the statement
  • if is_addr_mark m, propagate addr_mark on addr dependencies of the statement
  • if is_data_mark m, propagate data_mark on data dependencies of the statement Marks the node with a spare_mark and propagate so that the dependencies that were not selected yet will be marked spare. When the statement is a call, its functional inputs/outputs are also selected (The call is still selected even it has no output). When the statement is a composed one (block, if, etc...), all the sub-statements are selected.

Internally used to select a statement call without its inputs/outputs so that it doesn't select the statements computing the inputs of the called function as select_stmt_internal would do. Raise Invalid_argument when the stmt isn't a call.

Internally used to select a zone value at a program point.

Sourceval select_zone_at_entry_point_internal : Frama_c_kernel.Cil_types.kernel_function -> ?select:t -> Frama_c_kernel.Locations.Zone.t -> Mark.t -> t

Internally used to select a zone value at the beginning of a function. For a defined function, it is similar to select_stmt_zone_internal with the initial statement, but it can also be used for undefined functions.

Sourceval select_zone_at_end_internal : Frama_c_kernel.Cil_types.kernel_function -> ?select:t -> Frama_c_kernel.Locations.Zone.t -> Mark.t -> t

Internally used to select a zone value at the end of a function. For a defined function, it is similar to select_stmt_zone_internal with the return statement, but it can also be used for undefined functions.

Sourceval select_modified_output_zone_internal : Frama_c_kernel.Cil_types.kernel_function -> ?select:t -> Frama_c_kernel.Locations.Zone.t -> Mark.t -> t

Internally used to select the statements that modify the given zone considered as in output. Be careful that it is NOT the same as selecting the zone at the end! The 'undef' zone is not propagated...

Sourceval select_stmt_ctrl_internal : Frama_c_kernel.Cil_types.kernel_function -> ?select:t -> Frama_c_kernel.Cil_types.stmt -> t

Internally used to select a statement reachability : Only propagate a ctrl_mark on the statement control dependencies.

Sourceval select_entry_point_internal : Frama_c_kernel.Cil_types.kernel_function -> ?select:t -> Mark.t -> t
Sourceval select_return_internal : Frama_c_kernel.Cil_types.kernel_function -> ?select:t -> Mark.t -> t
Sourceval select_pdg_nodes_internal : Frama_c_kernel.Cil_types.kernel_function -> ?select:t -> Pdg_types.PdgTypes.Node.t list -> Mark.t -> t

Internally used to select PDG nodes :

  • if is_ctrl_mark m, propagate ctrl_mark on ctrl dependencies of the statement
  • if is_addr_mark m, propagate addr_mark on addr dependencies of the statement
  • if is_data_mark m, propagate data_mark on data dependencies of the statement Marks the node with a spare_mark and propagate so that the dependencies that were not selected yet will be marked spare.

Debug

Sourceval pretty : Format.formatter -> t -> unit