Frama-C:
Plug-ins:
Libraries:

Frama-C API - engine

method sanitize : string -> string
method virtual datatype : T.ADT.t -> string
method virtual field : T.Field.t -> string
method env : Env.t

A safe copy of the environment

method set_env : Env.t -> unit

Set the environment

method marks : Env.t * T.marks

The current environment with empty marks

method lookup : T.term -> Qed.Engine.scope
method set_env : Env.t -> unit
method scope : Env.t -> (unit -> unit) -> unit
method local : (unit -> unit) -> unit
method global : (unit -> unit) -> unit
method bind : T.var -> string
method find : T.var -> string
method virtual t_int : string
method virtual t_real : string
method virtual t_bool : string
method virtual t_prop : string
method virtual t_atomic : T.tau -> bool
method virtual pp_tvar : int Qed.Plib.printer
method virtual pp_array : T.tau Qed.Plib.printer
method virtual pp_farray : T.tau Qed.Plib.printer2
method virtual pp_datatype : T.ADT.t -> T.tau list Qed.Plib.printer
method pp_subtau : T.tau Qed.Plib.printer
method mode : Qed.Engine.mode
method with_mode : Qed.Engine.mode -> (Qed.Engine.mode -> unit) -> unit
method virtual e_true : Qed.Engine.cmode -> string
method virtual e_false : Qed.Engine.cmode -> string
method virtual pp_int : Qed.Engine.amode -> Z.t Qed.Plib.printer
method virtual pp_real : Q.t Qed.Plib.printer
method virtual is_atomic : T.term -> bool
method virtual op_spaced : string -> bool
method virtual callstyle : Qed.Engine.callstyle
method virtual pp_apply : Qed.Engine.cmode -> T.term -> T.term list Qed.Plib.printer
method pp_fun : Qed.Engine.cmode -> T.Fun.t -> T.term list Qed.Plib.printer
method virtual op_scope : Qed.Engine.amode -> string option
method virtual op_real_of_int : Qed.Engine.op
method virtual op_add : Qed.Engine.amode -> Qed.Engine.op
method virtual op_sub : Qed.Engine.amode -> Qed.Engine.op
method virtual op_mul : Qed.Engine.amode -> Qed.Engine.op
method virtual op_div : Qed.Engine.amode -> Qed.Engine.op
method virtual op_mod : Qed.Engine.amode -> Qed.Engine.op
method virtual op_minus : Qed.Engine.amode -> Qed.Engine.op
method pp_times : Stdlib.Format.formatter -> Z.t -> T.term -> unit
method virtual op_equal : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_noteq : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_eq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method virtual op_neq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method virtual op_lt : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method virtual op_leq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method virtual pp_array_cst : Stdlib.Format.formatter -> T.tau -> T.term -> unit
method virtual pp_array_get : Stdlib.Format.formatter -> T.term -> T.term -> unit
method virtual pp_array_set : Stdlib.Format.formatter -> T.term -> T.term -> T.term -> unit
method virtual pp_get_field : Stdlib.Format.formatter -> T.term -> T.Field.t -> unit
method virtual pp_def_fields : T.record Qed.Plib.printer
method virtual op_not : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_and : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_or : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_imply : Qed.Engine.cmode -> Qed.Engine.op
method virtual op_equiv : Qed.Engine.cmode -> Qed.Engine.op
method pp_not : T.term Qed.Plib.printer
method pp_imply : Stdlib.Format.formatter -> T.term list -> T.term -> unit
method pp_equal : T.term Qed.Plib.printer2
method pp_noteq : T.term Qed.Plib.printer2
method virtual pp_conditional : Stdlib.Format.formatter -> T.term -> T.term -> T.term -> unit
method virtual pp_forall : T.tau -> string list Qed.Plib.printer
method virtual pp_exists : T.tau -> string list Qed.Plib.printer
method virtual pp_lambda : (string * T.tau) list Qed.Plib.printer
method shared : T.term -> bool
method shareable : T.term -> bool
method subterms : (T.term -> unit) -> T.term -> unit
method virtual pp_let : Stdlib.Format.formatter -> Qed.Engine.pmode -> string -> T.term -> unit
method pp_atom : T.term Qed.Plib.printer
method pp_flow : T.term Qed.Plib.printer
method pp_repr : T.term Qed.Plib.printer
method pp_tau : T.tau Qed.Plib.printer
method pp_var : string Qed.Plib.printer
method pp_term : T.term Qed.Plib.printer
method pp_prop : T.term Qed.Plib.printer
method pp_sort : T.term Qed.Plib.printer
method pp_expr : T.tau -> T.term Qed.Plib.printer