Frama-C:
Plug-ins:
Libraries:

Frama-C API - engine

Linking

method sanitize : string -> string
method virtual datatype : 'adt -> string
method virtual field : 'field -> string

Global and Local Environment

method env : 'env

Returns a fresh copy of the current environment.

method set_env : 'env -> unit

Set environment.

method lookup : 'term -> scope

Term scope in the current environment.

method scope : 'env -> (unit -> unit) -> unit

Calls the continuation in the provided environment. Previous environment is restored after return.

method local : (unit -> unit) -> unit

Calls the continuation in a local copy of the environment. Previous environment is restored after return, but allocators are left unchanged to enforce on-the-fly alpha-conversion.

method global : (unit -> unit) -> unit

Calls the continuation in a fresh local environment. Previous environment is restored after return.

method bind : 'var -> string
method find : 'var -> string

Types

method t_int : string
method t_real : string
method t_bool : string
method t_prop : string
method t_atomic : 'tau -> bool
method pp_array : 'tau Qed.Plib.printer

For Z->a arrays

method pp_farray : 'tau Qed.Plib.printer2

For k->a arrays

method pp_tvar : int Qed.Plib.printer

Type variables.

method pp_datatype : 'adt -> 'tau list Qed.Plib.printer
method pp_tau : 'tau Qed.Plib.printer

Without parentheses.

method pp_subtau : 'tau Qed.Plib.printer

With parentheses if non-atomic.

Current Mode

The mode represents the expected type for a term to printed. A requirement for all term printers in the engine is that current mode must be correctly set before call. Each term printer is then responsible for setting appropriate modes for its sub-terms.

method mode : mode
method with_mode : mode -> (mode -> unit) -> unit

Calls the continuation with given mode for sub-terms. The englobing mode is passed to continuation and then restored.

method op_scope : amode -> string option

Optional scoping post-fix operator when entering arithmetic mode.

Primitives

method e_true : cmode -> string

"true"

method e_false : cmode -> string

"false"

method pp_int : amode -> 'z Qed.Plib.printer
method pp_real : Q.t Qed.Plib.printer

Variables

method pp_var : string Qed.Plib.printer

Calls

These printers only applies to connective, operators and functions that are morphisms w.r.t current mode.

method callstyle : callstyle
method pp_fun : cmode -> 'logic -> 'term list Qed.Plib.printer
method pp_apply : cmode -> 'term -> 'term list Qed.Plib.printer

Arithmetics Operators

method op_real_of_int : op
method op_add : amode -> op
method op_sub : amode -> op
method op_mul : amode -> op
method op_div : amode -> op
method op_mod : amode -> op
method op_minus : amode -> op
method pp_times : Stdlib.Format.formatter -> 'z -> 'term -> unit

Defaults to self#op_minus or self#op_mul

Comparison Operators

method op_equal : cmode -> op
method op_noteq : cmode -> op
method op_eq : cmode -> amode -> op
method op_neq : cmode -> amode -> op
method op_lt : cmode -> amode -> op
method op_leq : cmode -> amode -> op
method pp_equal : 'term Qed.Plib.printer2
method pp_noteq : 'term Qed.Plib.printer2

Arrays

method pp_array_cst : Stdlib.Format.formatter -> 'tau -> 'term -> unit

Constant array "[v...]".

method pp_array_get : Stdlib.Format.formatter -> 'term -> 'term -> unit

Access "a[k]".

method pp_array_set : Stdlib.Format.formatter -> 'term -> 'term -> 'term -> unit

Update "a[k <- v]".

Records

method pp_get_field : Stdlib.Format.formatter -> 'term -> 'field -> unit

Field access.

method pp_def_fields : ('field * 'term) list Qed.Plib.printer

Record construction.

Logical Connectives

method op_not : cmode -> op
method op_and : cmode -> op
method op_or : cmode -> op
method op_imply : cmode -> op
method op_equiv : cmode -> op

Conditionals

method pp_not : 'term Qed.Plib.printer
method pp_imply : Stdlib.Format.formatter -> 'term list -> 'term -> unit
method pp_conditional : Stdlib.Format.formatter -> 'term -> 'term -> 'term -> unit

Binders

method pp_forall : 'tau -> string list Qed.Plib.printer
method pp_exists : 'tau -> string list Qed.Plib.printer
method pp_lambda : (string * 'tau) list Qed.Plib.printer

Bindings

method shared : 'term -> bool
method shareable : 'term -> bool
method subterms : ('term -> unit) -> 'term -> unit
method pp_let : Stdlib.Format.formatter -> pmode -> string -> 'term -> unit

Terms

method is_atomic : 'term -> bool

Sub-terms that require parentheses. Shared sub-terms are detected on behalf of this method.

method pp_flow : 'term Qed.Plib.printer

Printer with shared sub-terms printed with their name and without parentheses.

method pp_atom : 'term Qed.Plib.printer

Printer with shared sub-terms printed with their name and within parentheses for non-atomic expressions. Additional scope terminates the expression when required (typically for Coq).

method pp_repr : 'term Qed.Plib.printer

Raw representation of a term, as it is. This is where you should hook a printer to keep sharing, parentheses, and such.

Top Level

method pp_term : 'term Qed.Plib.printer

Prints in term mode. Default uses self#pp_shared with mode Mterm inside an <hov> box.

method pp_prop : 'term Qed.Plib.printer

Prints in prop mode. Default uses self#pp_shared with mode Mprop inside an <hv> box.

method pp_expr : 'tau -> 'term Qed.Plib.printer

Prints in term, arithmetic or prop mode with respect to provided type.

method pp_sort : 'term Qed.Plib.printer

Prints in term, arithmetic or prop mode with respect to the sort of term. Boolean expression that also have a property form are printed in Mprop mode.