package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/Lang/F/index.html

Module `Lang.F`Source

Source

module QED : 
  Qed.Logic.Term
    with module ADT = ADT
     and module Field = Field
     and module Fun = Fun

Types and Variables

Sourcetype var = QED.var

Sourcetype tau = QED.tau

Sourcetype pool = QED.pool

Sourcemodule Tau = QED.Tau

Sourcemodule Var = QED.Var

Sourcemodule Vars : Qed.Idxset.S with type elt = var

Sourcemodule Vmap : Qed.Idxmap.S with type key = var

Sourceval pool : ?copy:pool -> unit -> pool

Sourceval fresh : pool -> ?basename:string -> tau -> var

Sourceval alpha : pool -> var -> var

Sourceval add_var : pool -> var -> unit

Sourceval add_vars : pool -> Vars.t -> unit

Sourceval tau_of_var : var -> tau

Expressions

Sourcetype term = QED.term

Sourcetype record = (field * term) list

Sourceval hash : term -> int

Constant time

Sourceval equal : term -> term -> bool

Same as ==

Sourceval compare : term -> term -> int

Sourcemodule Tset : Qed.Idxset.S with type elt = term

Sourcemodule Tmap : Qed.Idxmap.S with type key = term

Sourcetype unop = term -> term

Sourcetype binop = term -> term -> term

Sourceval e_zero : term

Sourceval e_one : term

Sourceval e_minus_one : term

Sourceval e_minus_one_real : term

Sourceval e_one_real : term

Sourceval e_zero_real : term

Sourceval constant : term -> term

Sourceval e_fact : int -> term -> term

Sourceval e_int64 : int64 -> term

Sourceval e_bigint : Frama_c_kernel.Integer.t -> term

Sourceval e_float : float -> term

Sourceval e_setfield : term -> field -> term -> term

Sourceval e_range : term -> term -> term

e_range a b = b+1-a

Sourceval is_zero : term -> bool

Sourceval e_true : term

Sourceval e_false : term

Sourceval e_bool : bool -> term

Sourceval e_literal : bool -> term -> term

Sourceval e_int : int -> term

Sourceval e_zint : Z.t -> term

Sourceval e_real : Q.t -> term

Sourceval e_var : var -> term

Sourceval e_opp : term -> term

Sourceval e_times : Z.t -> term -> term

Sourceval e_sum : term list -> term

Sourceval e_prod : term list -> term

Sourceval e_add : term -> term -> term

Sourceval e_sub : term -> term -> term

Sourceval e_mul : term -> term -> term

Sourceval e_div : term -> term -> term

Sourceval e_mod : term -> term -> term

Sourceval e_eq : term -> term -> term

Sourceval e_neq : term -> term -> term

Sourceval e_leq : term -> term -> term

Sourceval e_lt : term -> term -> term

Sourceval e_imply : term list -> term -> term

Sourceval e_equiv : term -> term -> term

Sourceval e_and : term list -> term

Sourceval e_or : term list -> term

Sourceval e_not : term -> term

Sourceval e_if : term -> term -> term -> term

Sourceval e_const : tau -> term -> term

Sourceval e_get : term -> term -> term

Sourceval e_set : term -> term -> term -> term

Sourceval e_getfield : term -> Field.t -> term

Sourceval e_record : record -> term

Sourceval e_fun : ?result:tau -> Fun.t -> term list -> term

Sourceval e_bind : Qed.Logic.binder -> var -> term -> term

Source

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.

Sourceval e_close : (Qed.Logic.binder * var) list -> term -> term

Closes all specified binders

Predicates

Sourcetype pred

Sourcetype cmp = term -> term -> pred

Sourcetype operator = pred -> pred -> pred

Sourcemodule Pmap : Qed.Idxmap.S with type key = pred

Sourcemodule Pset : Qed.Idxset.S with type elt = pred

Sourceval p_true : pred

Sourceval p_false : pred

Sourceval p_equal : term -> term -> pred

Sourceval p_equals : (term * term) list -> pred list

Sourceval p_neq : term -> term -> pred

Sourceval p_leq : term -> term -> pred

Sourceval p_lt : term -> term -> pred

Sourceval p_positive : term -> pred

Sourceval is_ptrue : pred -> Qed.Logic.maybe

Sourceval is_pfalse : pred -> Qed.Logic.maybe

Sourceval is_equal : term -> term -> Qed.Logic.maybe

Sourceval eqp : pred -> pred -> bool

Sourceval comparep : pred -> pred -> int

Sourceval p_bool : term -> pred

Sourceval e_prop : pred -> term

Sourceval p_bools : term list -> pred list

Sourceval e_props : pred list -> term list

Sourceval e_lift : (term -> term) -> pred -> pred

Sourceval p_lift : (pred -> pred) -> term -> term

Sourceval p_not : pred -> pred

Sourceval p_and : pred -> pred -> pred

Sourceval p_or : pred -> pred -> pred

Sourceval p_imply : pred -> pred -> pred

Sourceval p_equiv : pred -> pred -> pred

Sourceval p_hyps : pred list -> pred -> pred

Sourceval p_if : pred -> pred -> pred -> pred

Sourceval p_conj : pred list -> pred

Sourceval p_disj : pred list -> pred

Sourceval p_any : ('a -> pred) -> 'a list -> pred

Sourceval p_all : ('a -> pred) -> 'a list -> pred

Sourceval p_call : lfun -> term list -> pred

Sourceval e_lambda : var list -> term -> term

Sourceval e_apply : term -> term list -> term

Sourceval p_forall : var list -> pred -> pred

Sourceval p_exists : var list -> pred -> pred

Sourceval p_bind : Qed.Logic.binder -> var -> pred -> pred

Sourcetype sigma

Sourcemodule Subst : sig ... end

Sourceval e_subst : sigma -> term -> term

Sourceval p_subst : sigma -> pred -> pred

Sourceval p_subst_var : var -> term -> pred -> pred

Sourceval e_vars : term -> var list

Sorted

Sourceval p_vars : pred -> var list

Sorted

Sourceval p_close : pred -> pred

Quantify over (sorted) free variables

Sourceval pp_tau : Format.formatter -> tau -> unit

Sourceval pp_var : Format.formatter -> var -> unit

Sourceval pp_vars : Format.formatter -> Vars.t -> unit

Sourceval pp_term : Format.formatter -> term -> unit

Sourceval pp_pred : Format.formatter -> pred -> unit

Sourceval debugp : Format.formatter -> pred -> unit

Sourcetype env

Sourceval 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.

Sourcetype marks = QED.marks

Sourceval env : Vars.t -> env

Sourceval marker : env -> marks

Sourceval mark_e : marks -> term -> unit

Sourceval 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.

Sourceval defs : marks -> term list

Sourceval define : (env -> string -> term -> unit) -> env -> marks -> env

Sourceval pp_eterm : env -> Format.formatter -> term -> unit

Sourceval pp_epred : env -> Format.formatter -> pred -> unit

Sourceval p_expr : pred -> pred QED.expression

Sourceval e_expr : pred -> term QED.expression

Binders

Sourceval lc_closed : term -> bool

Sourceval lc_iter : (term -> unit) -> term -> unit

Utilities

Sourceval decide : term -> bool

Return true if and only the term is e_true. Constant time.

Sourceval basename : term -> string

Sourceval is_true : term -> Qed.Logic.maybe

Constant time.

Sourceval is_false : term -> Qed.Logic.maybe

Constant time.

Sourceval is_prop : term -> bool

Boolean or Property

Sourceval is_int : term -> bool

Integer sort

Sourceval is_real : term -> bool

Real sort

Sourceval is_arith : term -> bool

Integer or Real sort

Sourceval is_closed : term -> bool

No bound variables

Sourceval is_simple : term -> bool

Constants, variables, functions of arity 0

Sourceval is_atomic : term -> bool

Constants and variables

Sourceval is_primitive : term -> bool

Constants only

Sourceval is_neutral : Fun.t -> term -> bool

Sourceval is_absorbant : Fun.t -> term -> bool

Sourceval record_with : record -> (term * record) option

Sourceval are_equal : term -> term -> Qed.Logic.maybe

Computes equality

Sourceval eval_eq : term -> term -> bool

Same as are_equal is Yes

Sourceval eval_neq : term -> term -> bool

Same as are_equal is No

Sourceval eval_lt : term -> term -> bool

Same as e_lt is e_true

Sourceval eval_leq : term -> term -> bool

Same as e_leq is e_true

Sourceval repr : term -> QED.repr

Constant time

Sourceval sort : term -> Qed.Logic.sort

Constant time

Sourceval vars : term -> Vars.t

Constant time

Sourceval varsp : pred -> Vars.t

Constant time

Sourceval occurs : var -> term -> bool

Sourceval occursp : var -> pred -> bool

Sourceval intersect : term -> term -> bool

Sourceval intersectp : pred -> pred -> bool

Sourceval is_subterm : term -> term -> bool

Source

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.

Sourceval set_builtin : lfun -> (term list -> term) -> unit

Sourceval set_builtin_get : lfun -> (term list -> term list -> term) -> unit

Sourceval set_builtin_field : lfun -> field -> (term list -> term) -> unit

Sourceval set_builtin_1 : lfun -> unop -> unit

Sourceval set_builtin_2 : lfun -> binop -> unit

Sourceval set_builtin_2' : lfun -> (term -> term -> tau option -> term) -> unit

Sourceval set_builtin_eq : lfun -> binop -> unit

Sourceval set_builtin_leq : lfun -> binop -> unit

Sourceval set_builtin_eqp : lfun -> cmp -> unit

Sourceval release : unit -> unit

Empty local caches

On This Page

Types and Variables
Expressions
Predicates
Binders
Utilities
Builtins

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/Lang/F/index.html

Module Lang.FSource

Types and Variables

Expressions

Predicates

Binders

Utilities

Builtins

Module `Lang.F`Source