Frama-C:
Plug-ins:
Libraries:

Frama-C API - Symbol

Qed Symbols

type data

Abstract Data Types

val constructors : data -> Why3.Decl.constructor list

Returns an empty list for pure ADT

type field

Record Fields

val fields : data -> field list

Returns an empty list for non-record data

val field : data -> string -> field
  • raises Not_found

    for non-record data

val by_field_rank : field -> field -> int

Ordering with respect to field declaration order in record

type tau = (field, data) Logic.datatype

Logic Types

val data : data -> tau list -> tau

Converts builtin Qed types from external data symbols

type lfun

Logic Functions

val signature : lfun -> int * tau * tau list

Returns a triple a,r,vs with a the number of polymorphic variables, r the type of result and vs the type of arguments.

val definition : lfun -> (Why3.Term.vsymbol list * Why3.Term.term) option

Returns an optional pair Some(xs,def) with xs the formal parameters and def the defining term. Returns None when the function is abstract.

val apply : lfun -> ?result:tau -> tau list -> tau

Unifies the polymorphic types of the function with the provided type of arguments and of the result, when available. If you provide a result type, it will be unified with the expected result type of the logic symbol, so use ~result:Prop for predicates.

Symbol Lookup

val find_ts : Why3.Env.env -> string -> (Why3.Theory.theory -> Why3.Ty.tysymbol -> 'a) -> 'a
val find_ls : Why3.Env.env -> string -> (Why3.Theory.theory -> Why3.Term.lsymbol -> 'a) -> 'a
val find_pr : Why3.Env.env -> string -> (Why3.Theory.theory -> Why3.Decl.prsymbol -> 'a) -> 'a
val find_use : context:Why3.Theory.theory -> Why3.Ident.ident -> Why3.Theory.theory
val of_ts : Why3.Theory.theory -> Why3.Ty.tysymbol -> data

Memoized.

  • raises Invalid_argument

    if undefined in context

type sigma = tau Why3.Ty.Mtv.t
val of_infix : string -> string

Converts infix, prefix and mixfix names to user names. Typically: of_infix "infix +" = "(+)". Returns identity for usual identifiers

val to_infix : string -> string

Reverse of of_infix. Typically: to_infix "(+)" = "infix +".

val of_ty : Why3.Theory.theory -> ?sigma:sigma -> Why3.Ty.ty -> tau

Memoized.

  • raises Invalid_argument

    if undefined in context

val of_oty : Why3.Theory.theory -> ?sigma:sigma -> Why3.Ty.ty option -> tau

Memoized. None means Prop.

  • raises Invalid_argument

    if undefined in context

val of_ls : Why3.Theory.theory -> Why3.Term.lsymbol -> lfun

Memoized.

  • raises Invalid_argument

    if undefined in context

val find_data : Why3.Env.env -> string -> data

Memoized in environment. Expect fully qualified identifiers, typically "int.Int.int".

  • raises Invalid_argument

    if not found in environment

val find_lfun : Why3.Env.env -> string -> lfun

Memoized in environment. Expect fully qualified identifiers, typically "int.Int.(+)".

  • raises Invalid_argument

    if not found in environment

Symbol Factory

type cluster
val cluster : ?path:string list -> ?loc:Why3.Loc.position -> string -> cluster
val add : cluster -> Why3.Decl.decl -> unit
val use : cluster -> Why3.Theory.theory -> unit
val use_data : cluster -> data -> unit
val use_lfun : cluster -> lfun -> unit
val new_data : cluster -> Why3.Ty.tysymbol -> data
val new_lfun : cluster -> Why3.Term.lsymbol -> lfun
val close : cluster -> Why3.Theory.theory

Symbol Modules

module type Symbol = sig ... end
module Data : Symbol with type t = data and type symbol = Why3.Ty.tysymbol
module Field : Symbol with type t = field and type symbol = Why3.Term.lsymbol
module Fun : Symbol with type t = lfun and type symbol = Why3.Term.lsymbol
module Tau : sig ... end