Frama-C API - Tactical
Tactics Entry Points
Tactical
Tactical Selection
type process = Conditions.sequent -> (string * Conditions.sequent) list
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 get_int : selection -> int option
val get_bool : selection -> bool option
val head : clause -> Lang.F.pred
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
module Fmap : sig ... end
Tactical Parameter Editors
type 'a finder = string -> 'a named
val ident : 'a field -> string
val default : 'a field -> 'a
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 mostn
results applying to selections
.find n
is used at script replay, and shall retrieve the selected item'sid
later on.
class type feedback = object ... end
Tactical Utilities
val at : selection -> int option
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
Composer Factory
class type composer = object ... end
Global Registry
type t = tactical
val register : tactical -> unit
val iter : (tactical -> unit) -> unit
val lookup : id:string -> tactical
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