Frama-C:
Plug-ins:
Libraries:

Frama-C API - Tactical

Tactics Entry Points

Tactical

Tactical Selection

type clause =
  1. | Goal of Lang.F.pred
  2. | Step of Conditions.step
type process = Conditions.sequent -> (string * Conditions.sequent) list
type status =
  1. | Not_applicable
  2. | Not_configured
  3. | Applicable of process
type selection =
  1. | Empty
  2. | Clause of clause
  3. | Inside of clause * Lang.F.term
  4. | Compose of compose
  5. | Multi of selection list
and compose = private
  1. | Cint of Frama_c_kernel.Z.t
  2. | Range of int * int
  3. | Code of Lang.F.term * string * selection list
val int : int -> selection
val range : int -> int -> selection
val compose : string -> selection list -> selection
val multi : selection list -> selection
val get_int : selection -> int option
val get_bool : selection -> bool option
val destruct : selection -> selection list
val head : clause -> Lang.F.pred
val equal : selection -> selection -> bool
val is_empty : selection -> bool
val selected : selection -> Lang.F.term
val 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.

val pp_clause : Stdlib.Format.formatter -> clause -> unit

Debug only

val pp_selection : Stdlib.Format.formatter -> selection -> unit

Debug only

Tactical Parameters

type 'a field
module Fmap : sig ... end

Tactical Parameter Editors

type 'a named = {
  1. title : string;
  2. descr : string;
  3. vid : string;
  4. value : 'a;
}
type 'a range = {
  1. vmin : 'a option;
  2. vmax : 'a option;
  3. vstep : 'a;
}
type 'a browser = ('a named -> unit) -> selection -> unit
type 'a finder = string -> 'a named
type 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
val ident : 'a field -> string
val default : 'a field -> 'a
val signature : 'a field -> 'a named
val pident : parameter -> string
val checkbox : id:string -> title:string -> descr:string -> ?default:bool -> unit -> bool field * parameter

Unless specified, default is false.

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.

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.

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.

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.
type 'a formatter = ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a
class type feedback = object ... end

Tactical Utilities

val at : selection -> int option
val mapi : (int -> int -> 'a -> 'b) -> 'a list -> 'b list
val insert : ?at:int -> (string * Lang.F.pred) list -> process
val replace : at:int -> (string * Conditions.condition) list -> process
val replace_single : at:int -> (string * Conditions.condition) -> Conditions.sequent -> string * Conditions.sequent
val replace_step : at:int -> Conditions.condition list -> process
val split : (string * Lang.F.pred) list -> process
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.

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

Apply process, but only after proving some condition

Tactical Plug-in

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

Composer Factory

class type composer = object ... end

Global Registry

type t = tactical
val register : tactical -> unit
val export : tactical -> tactical

Register and returns the tactical

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