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-wp.core/Wp/Tactical/index.html

Module Wp.TacticalSource

Tactics Entry Points

Tactical

Tactical Selection

Sourcetype clause =
  1. | Goal of Lang.F.pred
  2. | Step of Conditions.step
Sourcetype process = Conditions.sequent -> (string * Conditions.sequent) list
Sourcetype status =
  1. | Not_applicable
  2. | Not_configured
  3. | Applicable of process
Sourcetype selection =
  1. | Empty
  2. | Clause of clause
  3. | Inside of clause * Lang.F.term
  4. | Compose of compose
  5. | Multi of selection list
Sourceand compose = private
  1. | Cint of Frama_c_kernel.Integer.t
  2. | Range of int * int
  3. | Code of Lang.F.term * string * selection list
Sourceval int : int -> selection
Sourceval range : int -> int -> selection
Sourceval compose : string -> selection list -> selection
Sourceval multi : selection list -> selection
Sourceval get_int : selection -> int option
Sourceval get_bool : selection -> bool option
Sourceval destruct : selection -> selection list
Sourceval equal : selection -> selection -> bool
Sourceval is_empty : selection -> bool
Sourceval selected : selection -> Lang.F.term
Sourceval subclause : clause -> Lang.F.pred -> bool

When subclause clause p, we have clause = Step H and H -> p, or clause = Goal G and p -> G.

Sourceval pp_clause : Format.formatter -> clause -> unit

Debug only

Sourceval pp_selection : Format.formatter -> selection -> unit

Debug only

Tactical Parameters

Sourcetype 'a field
Sourcemodule Fmap : sig ... end

Tactical Parameter Editors

Sourcetype 'a named = {
  1. title : string;
  2. descr : string;
  3. vid : string;
  4. value : 'a;
}
Sourcetype 'a range = {
  1. vmin : 'a option;
  2. vmax : 'a option;
  3. vstep : 'a;
}
Sourcetype 'a browser = ('a named -> unit) -> selection -> unit
Sourcetype 'a finder = string -> 'a named
Sourcetype parameter =
  1. | Checkbox of bool field
  2. | Spinner of int field * int range
  3. | Composer of selection field * Lang.F.term -> bool
  4. | Selector : 'a field * 'a named list * ('a -> 'a -> bool) -> parameter
  5. | Search : 'a named option field * 'a browser * 'a finder -> parameter
Sourceval ident : 'a field -> string
Sourceval default : 'a field -> 'a
Sourceval signature : 'a field -> 'a named
Sourceval pident : parameter -> string
Sourceval checkbox : id:string -> title:string -> descr:string -> ?default:bool -> unit -> bool field * parameter

Unless specified, default is false.

Sourceval spinner : id:string -> title:string -> descr:string -> ?default:int -> ?vmin:int -> ?vmax:int -> ?vstep:int -> unit -> int field * parameter

Unless specified, default is vmin or 0 or vmax, whichever fits. Range must be non-empty, and default shall fit in.

Sourceval selector : id:string -> title:string -> descr:string -> ?default:'a -> options:'a named list -> ?equal:('a -> 'a -> bool) -> unit -> 'a field * parameter

Unless specified, default is head option. Default equality is (=). Options must be non-empty.

Sourceval composer : id:string -> title:string -> descr:string -> ?default:selection -> ?filter:(Lang.F.term -> bool) -> unit -> selection field * parameter

Unless specified, default is Empty selection.

Search field.

  • browse s n is the lookup function, used in the GUI only. Shall returns at most n results applying to selection s.
  • find n is used at script replay, and shall retrieve the selected item's id later on.
Sourcetype 'a formatter = ('a, Format.formatter, unit) format -> 'a
Sourceclass type feedback = object ... end

Tactical Utilities

Sourceval at : selection -> int option
Sourceval mapi : (int -> int -> 'a -> 'b) -> 'a list -> 'b list
Sourceval insert : ?at:int -> (string * Lang.F.pred) list -> process
Sourceval replace : at:int -> (string * Conditions.condition) list -> process
Sourceval replace_single : at:int -> (string * Conditions.condition) -> Conditions.sequent -> string * Conditions.sequent
Sourceval replace_step : at:int -> Conditions.condition list -> process
Sourceval split : (string * Lang.F.pred) list -> process
Sourceval rewrite : ?at:int -> (string * Lang.F.pred * Lang.F.term * Lang.F.term) list -> process

For each pattern (descr,guard,src,tgt) replace src with tgt under condition guard, inserted in position at.

Sourceval condition : string -> Lang.F.pred -> process -> process

Apply process, but only after proving some condition

Tactical Plug-in

Sourceclass type tactical = object ... end
Sourceclass virtual make : id:string -> title:string -> descr:string -> params:parameter list -> object ... end

Composer Factory

Sourceclass type composer = object ... end

Global Registry

Sourceval register : tactical -> unit
Sourceval export : tactical -> tactical

Register and returns the tactical

Sourceval iter : (tactical -> unit) -> unit
Sourceval lookup : id:string -> tactical
Sourceval lookup_param : tactical -> id:string -> parameter
Sourcetype computer = Lang.F.term list -> Lang.F.term
Sourceval add_computer : string -> computer -> unit
Sourceval add_composer : composer -> unit
Sourceval iter_composer : (composer -> unit) -> unit