package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install

Dune 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.1-Cobalt.tar.gz
sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

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

Module Api.ProjectSource

Slicing project management.

Sourceval reset_slicing : unit -> unit

Init/reset a slicing project.

Sourceval change_slicing_level : Frama_c_kernel.Cil_types.kernel_function -> int -> unit

Change the slicing level of this function (see the -slicing-level option documentation to know the meaning of the number)

  • raises SlicingTypes.ExternalFunction

    if kf has no definition.

Sourceval extract : ?f_slice_names: (Frama_c_kernel.Cil_types.kernel_function -> bool -> int -> string) -> string -> Frama_c_kernel.Project.t

Build a new Db.Project.t from all Slice.t of a project. Can optionally specify how to name the sliced functions by defining f_slice_names. f_slice_names kf src_visi num_slice has to return the name of the exported functions based on the source function kf.

  • src_visi tells if the source function name is used (if not, it can be used for a slice)
  • num_slice gives the number of the slice to name. The entry point function is only exported once : it is VERY recommended to give to it its original name, even if it is sliced.
Sourceval print_dot : filename:string -> title:string -> unit

Print a representation of the slicing project (call graph) in a dot file which name is the given string.

No needs of Journalization

Sourceval default_slice_names : Frama_c_kernel.Cil_types.kernel_function -> bool -> int -> string

Return true iff the source function is called (even indirectly via transitivity) from a Slice.t.

Sourceval has_persistent_selection : Frama_c_kernel.Cil_types.kernel_function -> bool

Return true iff the source function has persistent selection

Sourceval is_directly_called_internal : Frama_c_kernel.Cil_types.kernel_function -> bool

Return true if the source function is directly (even via pointer function) called from a Slice.t.

Debug

Sourceval pretty : Format.formatter -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct