package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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

Module `Wp.Tactical`Source

Tactics Entry Points

Tactical

Tactical Selection

Sourcetype clause =

| Goal of Lang.F.pred
| Step of Conditions.step

Sourcetype process = Conditions.sequent -> (string * Conditions.sequent) list

Sourcetype status =

| Not_applicable
| Not_configured
| Applicable of process

Sourcetype selection =

| Empty
| Clause of clause
| Inside of clause * Lang.F.term
| Compose of compose
| Multi of selection list

Sourceand compose = private

| Cint of Frama_c_kernel.Integer.t
| Range of int * int
| Code of Lang.F.term * string * selection list

Sourceval int : int -> selection

Sourceval cint : Frama_c_kernel.Integer.t -> 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 head : clause -> Lang.F.pred

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 = {

title : string;
descr : string;
vid : string;
value : 'a;

}

Sourcetype 'a range = {

vmin : 'a option;
vmax : 'a option;
vstep : 'a;

}

Sourcetype 'a browser = ('a named -> unit) -> selection -> unit

Sourcetype 'a finder = string -> 'a named

Sourcetype parameter =

| Checkbox of bool field
| Spinner of int field * int range
| Composer of selection field * Lang.F.term -> bool
| Selector : 'a field * 'a named list * ('a -> 'a -> bool) -> parameter
| 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

Source

val checkbox : 
  id:string ->
  title:string ->
  descr:string ->
  ?default:bool ->
  unit ->
  bool field * parameter

Unless specified, default is false.

Source

val 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.

Source

val 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.

Source

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

Unless specified, default is Empty selection.

Source

val search : 
  id:string ->
  title:string ->
  descr:string ->
  browse:'a browser ->
  find:'a finder ->
  unit ->
  'a named option field * parameter

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

Source

val 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

Source

val 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

Sourcetype t = tactical

Sourceval register : tactical -> unit

Sourceval export : tactical -> 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

On This Page

Tactical Selection
Tactical Parameters
Tactical Parameter Editors
Tactical Utilities
Tactical Plug-in
Composer Factory
Global Registry

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Wp.TacticalSource

Tactical Selection

Tactical Parameters

Tactical Parameter Editors

Tactical Utilities

Tactical Plug-in

Composer Factory

Global Registry

Module `Wp.Tactical`Source