Frama-C API - F
Types and Variables
type var = QED.var
type tau = QED.tau
type pool = QED.pool
module Tau = QED.Tau
module Var = QED.Var
module Vars : Qed.Idxset.S with type elt = var
module Vmap : Qed.Idxmap.S with type key = var
Expressions
type term = QED.term
val hash : term -> int
Constant time
module Tset : Qed.Idxset.S with type elt = term
module Tmap : Qed.Idxmap.S with type key = term
val e_zero : term
val e_one : term
val e_minus_one : term
val e_minus_one_real : term
val e_one_real : term
val e_zero_real : term
val e_int64 : int64 -> term
val e_bigint : Frama_c_kernel.Integer.t -> term
val e_float : float -> term
val is_zero : term -> bool
val e_true : term
val e_false : term
val e_bool : bool -> term
val e_int : int -> term
val e_zint : Z.t -> term
val e_real : Q.t -> term
val e_bind : Qed.Logic.binder -> var -> term -> term
val e_open : pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool -> term -> (Qed.Logic.binder * var) list * term
Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default). The pool must contain all free variables of the term.
val e_close : (Qed.Logic.binder * var) list -> term -> term
Closes all specified binders
Predicates
module Pmap : Qed.Idxmap.S with type key = pred
module Pset : Qed.Idxset.S with type elt = pred
val p_true : pred
val p_false : pred
val is_ptrue : pred -> Qed.Logic.maybe
val is_pfalse : pred -> Qed.Logic.maybe
val is_equal : term -> term -> Qed.Logic.maybe
val p_bind : Qed.Logic.binder -> var -> pred -> pred
module Subst : sig ... end
val pp_tau : Stdlib.Format.formatter -> tau -> unit
val pp_var : Stdlib.Format.formatter -> var -> unit
val pp_vars : Stdlib.Format.formatter -> Vars.t -> unit
val pp_term : Stdlib.Format.formatter -> term -> unit
val pp_pred : Stdlib.Format.formatter -> pred -> unit
val debugp : Stdlib.Format.formatter -> pred -> unit
val context_pp : env Context.value
Context used by pp_term, pp_pred, pp_var, ppvars for printing the term. Allows to keep the same disambiguation.
type marks = QED.marks
Returns a list of terms to be shared among all shared or marked subterms. The order of terms is consistent with definition order: head terms might be used in tail ones.
val p_expr : pred -> pred QED.expression
val e_expr : pred -> term QED.expression
Binders
val lc_closed : term -> bool
Utilities
val decide : term -> bool
Return true
if and only the term is e_true
. Constant time.
val basename : term -> string
val is_true : term -> Qed.Logic.maybe
Constant time.
val is_false : term -> Qed.Logic.maybe
Constant time.
val is_prop : term -> bool
Boolean or Property
val is_int : term -> bool
Integer sort
val is_real : term -> bool
Real sort
val is_arith : term -> bool
Integer or Real sort
val is_closed : term -> bool
No bound variables
val is_simple : term -> bool
Constants, variables, functions of arity 0
val is_atomic : term -> bool
Constants and variables
val is_primitive : term -> bool
Constants only
val are_equal : term -> term -> Qed.Logic.maybe
Computes equality
val sort : term -> Qed.Logic.sort
Constant time
val typeof : ?field:(Field.t -> tau) -> ?record:(Field.t -> tau) -> ?call:(Fun.t -> tau option list -> tau) -> term -> tau
Try to extract a type of term. Parameterized by optional extractors for field and functions. Extractors may raise Not_found
; however, they are only used when the provided kinds for fields and functions are not precise enough.
Builtins
The functions below register simplifiers for function f
. The computation code may raise Not_found
, in which case the symbol is not interpreted.
If f
is an operator with algebraic rules (see type operator
), the children are normalized before builtin call.
Highest priority is 0
. Recursive calls must be performed on strictly smaller terms.