package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
module QED : Qed.Logic.Term with module ADT = ADT and module Field = Field and module Fun = Fun

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
val pool : ?copy:pool -> unit -> pool
val fresh : pool -> ?basename:string -> tau -> var
val alpha : pool -> var -> var
val add_var : pool -> var -> unit
val add_vars : pool -> Vars.t -> unit
val tau_of_var : var -> tau

Expressions

type term = QED.term
type record = (field * term) list
val hash : term -> int

Constant time

val equal : term -> term -> bool

Same as ==

val compare : term -> term -> int
module Tset : Qed.Idxset.S with type elt = term
module Tmap : Qed.Idxmap.S with type key = term
type unop = term -> term
type binop = term -> term -> 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 constant : term -> term
val e_fact : int -> term -> term
val e_int64 : int64 -> term
val e_bigint : Frama_c_kernel.Integer.t -> term
val e_float : float -> term
val e_setfield : term -> field -> term -> term
val e_range : term -> term -> term

e_range a b = b+1-a

val is_zero : term -> bool
val e_true : term
val e_false : term
val e_bool : bool -> term
val e_literal : bool -> term -> term
val e_int : int -> term
val e_zint : Z.t -> term
val e_real : Q.t -> term
val e_var : var -> term
val e_opp : term -> term
val e_times : Z.t -> term -> term
val e_sum : term list -> term
val e_prod : term list -> term
val e_add : term -> term -> term
val e_sub : term -> term -> term
val e_mul : term -> term -> term
val e_div : term -> term -> term
val e_mod : term -> term -> term
val e_eq : term -> term -> term
val e_neq : term -> term -> term
val e_leq : term -> term -> term
val e_lt : term -> term -> term
val e_imply : term list -> term -> term
val e_equiv : term -> term -> term
val e_and : term list -> term
val e_or : term list -> term
val e_not : term -> term
val e_if : term -> term -> term -> term
val e_const : tau -> term -> term
val e_get : term -> term -> term
val e_set : term -> term -> term -> term
val e_getfield : term -> Field.t -> term
val e_record : record -> term
val e_fun : ?result:tau -> Fun.t -> term list -> 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

type pred
type cmp = term -> term -> pred
type operator = pred -> pred -> pred
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 p_equal : term -> term -> pred
val p_equals : (term * term) list -> pred list
val p_neq : term -> term -> pred
val p_leq : term -> term -> pred
val p_lt : term -> term -> pred
val p_positive : term -> pred
val is_ptrue : pred -> Qed.Logic.maybe
val is_pfalse : pred -> Qed.Logic.maybe
val is_equal : term -> term -> Qed.Logic.maybe
val eqp : pred -> pred -> bool
val comparep : pred -> pred -> int
val p_bool : term -> pred
val e_prop : pred -> term
val p_bools : term list -> pred list
val e_props : pred list -> term list
val e_lift : (term -> term) -> pred -> pred
val p_lift : (pred -> pred) -> term -> term
val p_not : pred -> pred
val p_and : pred -> pred -> pred
val p_or : pred -> pred -> pred
val p_imply : pred -> pred -> pred
val p_equiv : pred -> pred -> pred
val p_hyps : pred list -> pred -> pred
val p_if : pred -> pred -> pred -> pred
val p_conj : pred list -> pred
val p_disj : pred list -> pred
val p_any : ('a -> pred) -> 'a list -> pred
val p_all : ('a -> pred) -> 'a list -> pred
val p_call : lfun -> term list -> pred
val e_lambda : var list -> term -> term
val e_apply : term -> term list -> term
val p_forall : var list -> pred -> pred
val p_exists : var list -> pred -> pred
val p_bind : Qed.Logic.binder -> var -> pred -> pred
type sigma
module Subst : sig ... end
val e_subst : sigma -> term -> term
val p_subst : sigma -> pred -> pred
val p_subst_var : var -> term -> pred -> pred
val e_vars : term -> var list

Sorted

val p_vars : pred -> var list

Sorted

val p_close : pred -> pred

Quantify over (sorted) free variables

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
type env
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
val env : Vars.t -> env
val marker : env -> marks
val mark_e : marks -> term -> unit
val mark_p : marks -> pred -> unit

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 defs : marks -> term list
val define : (env -> string -> term -> unit) -> env -> marks -> env
val pp_eterm : env -> Stdlib.Format.formatter -> term -> unit
val pp_epred : env -> Stdlib.Format.formatter -> pred -> unit
val p_expr : pred -> pred QED.expression
val e_expr : pred -> term QED.expression

Binders

val lc_closed : term -> bool
val lc_iter : (term -> unit) -> term -> unit

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 is_neutral : Fun.t -> term -> bool
val is_absorbant : Fun.t -> term -> bool
val record_with : record -> (term * record) option
val are_equal : term -> term -> Qed.Logic.maybe

Computes equality

val eval_eq : term -> term -> bool

Same as are_equal is Yes

val eval_neq : term -> term -> bool

Same as are_equal is No

val eval_lt : term -> term -> bool

Same as e_lt is e_true

val eval_leq : term -> term -> bool

Same as e_leq is e_true

val repr : term -> QED.repr

Constant time

val sort : term -> Qed.Logic.sort

Constant time

val vars : term -> Vars.t

Constant time

val varsp : pred -> Vars.t

Constant time

val occurs : var -> term -> bool
val occursp : var -> pred -> bool
val intersect : term -> term -> bool
val intersectp : pred -> pred -> bool
val is_subterm : term -> term -> bool
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.

  • parameter field

    type of a field value

  • parameter record

    type of the record containing a field

  • parameter call

    type of the values returned by the function

  • raises Not_found

    if no type is found.

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.

val set_builtin : lfun -> (term list -> term) -> unit
val set_builtin_get : lfun -> (term list -> term list -> term) -> unit
val set_builtin_field : lfun -> field -> (term list -> term) -> unit
val set_builtin_1 : lfun -> unop -> unit
val set_builtin_2 : lfun -> binop -> unit
val set_builtin_2' : lfun -> (term -> term -> tau option -> term) -> unit
val set_builtin_eq : lfun -> binop -> unit
val set_builtin_leq : lfun -> binop -> unit
val set_builtin_eqp : lfun -> cmp -> unit
val release : unit -> unit

Empty local caches

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