package frama-c

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

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.Integer.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 : Format.formatter -> clause -> unit

Debug only

val pp_selection : 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, Format.formatter, unit) 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
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