package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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