Tactical (frama-c-wp.Wp.Tactical)

Tactical Selection

type clause =

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

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

type status =

| Not_applicable
| Not_configured
| Applicable of process

type selection =

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

and compose = private

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

val int : int -> selection

val cint : Frama_c_kernel.Integer.t -> 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 = {

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

}

type 'a range = {

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

}

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

type 'a finder = string -> 'a named

type 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

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.

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.

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

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