package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Low-Level Logic Terms and Predicates

Logic Language based on Qed

Library

type library = string

Naming - Unique identifiers

val comp_id : Frama_c_kernel.Cil_types.compinfo -> string
val comp_init_id : Frama_c_kernel.Cil_types.compinfo -> string
val field_id : Frama_c_kernel.Cil_types.fieldinfo -> string
val field_init_id : Frama_c_kernel.Cil_types.fieldinfo -> string
val logic_id : Frama_c_kernel.Cil_types.logic_info -> string
val lemma_id : string -> string

Symbols

type datakind =
  1. | KValue
  2. | KInit
type adt = private
  1. | Mtype of mdt
    (*

    External type

    *)
  2. | Mrecord of mdt * fields
    (*

    External record-type

    *)
  3. | Atype of Frama_c_kernel.Cil_types.logic_type_info
    (*

    Logic Type

    *)
  4. | Comp of Frama_c_kernel.Cil_types.compinfo * datakind
    (*

    C-code struct or union

    *)
  5. | Wtype of string list * string * string list
    (*

    Why3 imported type

    *)

A type is never registered in a Definition.t

and mdt = string extern

name to print to the provers

and 'a extern = {
  1. ext_id : int;
  2. ext_library : library;
    (*

    a library which it depends on

    *)
  3. ext_debug : string;
    (*

    just for printing during debugging

    *)
}
and fields = {
  1. mutable fields : field list;
}
and field = private
  1. | Mfield of mdt * fields * string * tau
  2. | Cfield of Frama_c_kernel.Cil_types.fieldinfo * datakind
type t_builtin =
  1. | E_mdt of mdt
  2. | E_why3 of string list * string * string list
  3. | E_poly of tau list -> tau
type lfun = private
  1. | ACSL of Frama_c_kernel.Cil_types.logic_info
    (*

    Registered in Definition.t, only

    *)
  2. | CTOR of Frama_c_kernel.Cil_types.logic_ctor_info
    (*

    Not registered in Definition.t directly converted/printed

    *)
  3. | FUN of lsymbol
    (*

    External or Generated logic symbol

    *)
and lsymbol = {
  1. m_category : lfun Qed.Logic.category;
  2. m_params : Qed.Logic.sort list;
  3. m_result : Qed.Logic.sort;
  4. m_typeof : tau option list -> tau;
  5. m_source : source;
  6. m_coloring : bool;
}
and source =
  1. | Generated of WpContext.context option * string
  2. | Extern of Qed.Engine.link extern
  3. | Wsymbol of string list * string * string list
    (*

    Why3 imported logic symbol

    *)
val mem_builtin_type : name:string -> bool
val is_builtin_type : name:string -> tau -> bool
val get_builtin_type : name:string -> adt
val datatype : library:string -> string -> adt
val record : link:string -> library:string -> (string * tau) list -> adt
val field : adt -> string -> field
val fields_of_adt : adt -> field list
val fields_of_tau : tau -> field list
val fields_of_field : field -> field list

Must not be a builtin

type balance =
  1. | Nary
  2. | Left
  3. | Right
val on_lfun : (lfun -> unit) -> unit
val on_field : (field -> unit) -> unit
val extern_s : library:library -> ?link:Qed.Engine.link -> ?category:lfun Qed.Logic.category -> ?params:Qed.Logic.sort list -> ?sort:Qed.Logic.sort -> ?result:tau -> ?coloring:bool -> ?typecheck:(tau option list -> tau) -> string -> lfun
val extern_f : library:library -> ?link:Qed.Engine.link -> ?balance:balance -> ?category:lfun Qed.Logic.category -> ?params:Qed.Logic.sort list -> ?sort:Qed.Logic.sort -> ?result:tau -> ?coloring:bool -> ?typecheck:(tau option list -> tau) -> ('a, Stdlib.Format.formatter, unit, lfun) Stdlib.format4 -> 'a

balance just give a default when link is not specified

val extern_p : library:library -> ?bool:string -> ?prop:string -> ?link:Qed.Engine.link -> ?params:Qed.Logic.sort list -> ?coloring:bool -> unit -> lfun
val extern_fp : library:library -> ?params:Qed.Logic.sort list -> ?link:string -> ?coloring:bool -> string -> lfun
val generated_f : ?context:bool -> ?category:lfun Qed.Logic.category -> ?params:Qed.Logic.sort list -> ?sort:Qed.Logic.sort -> ?result:tau -> ?coloring:bool -> ('a, Stdlib.Format.formatter, unit, lfun) Stdlib.format4 -> 'a
val generated_p : ?context:bool -> ?coloring:bool -> string -> lfun
val extern_t : string -> link:string -> library:library -> mdt
val imported_t : package:string list -> theory:string -> name:string list -> adt
val imported_f : package:string list -> theory:string -> name:string list -> ?params:Qed.Logic.sort list -> ?result:Qed.Logic.sort -> ?typecheck:(tau option list -> tau) -> unit -> lfun

Sorting and Typing

val tau_of_object : Ctypes.c_object -> tau
val tau_of_ctype : Frama_c_kernel.Cil_types.typ -> tau
val tau_of_return : Frama_c_kernel.Cil_types.logic_type option -> tau
val tau_of_lfun : lfun -> tau option list -> tau
val tau_of_field : field -> tau
val tau_of_record : field -> tau
val init_of_object : Ctypes.c_object -> tau
val init_of_ctype : Frama_c_kernel.Cil_types.typ -> tau
val t_int : tau
val t_real : tau
val t_bool : tau
val t_prop : tau
val t_addr : unit -> tau
val t_float : Ctypes.c_float -> tau
val t_array : tau -> tau
val t_farray : tau -> tau -> tau
val t_datatype : adt -> tau list -> tau
val t_matrix : tau -> int -> tau
val pointer : tau Context.value

type of pointers

val floats : (Ctypes.c_float -> tau) Context.value

type of floats

val poly : string list Context.value

polymorphism

val builtin_types : (string -> t_builtin) Context.value
val parameters : (lfun -> Qed.Logic.sort list) -> unit

definitions

val name_of_lfun : lfun -> string
val name_of_field : field -> string
val context_of_lfun : lfun -> WpContext.context option

LFuns are unique by name and context

val is_coloring_lfun : lfun -> bool

Logic Formulae

module ADT : Qed.Logic.Data with type t = adt
module Field : Qed.Logic.Field with type t = field
module Fun : Qed.Logic.Function with type t = lfun
class virtual idprinting : object ... end
module F : sig ... end
module N : sig ... end

simpler notation for writing F.term and F.pred

Fresh Variables and Constraints

type gamma
val new_pool : ?copy:F.pool -> ?vars:F.Vars.t -> unit -> F.pool
val new_gamma : ?copy:gamma -> unit -> gamma
val local : ?pool:F.pool -> ?vars:F.Vars.t -> ?gamma:gamma -> ('a -> 'b) -> 'a -> 'b
val freshvar : ?basename:string -> F.tau -> F.var
val freshen : F.var -> F.var
val assume : F.pred -> unit
val without_assume : ('a -> 'b) -> 'a -> 'b
val hypotheses : gamma -> F.pred list
val get_pool : unit -> F.pool
val get_gamma : unit -> gamma
val has_gamma : unit -> bool
val get_hypotheses : unit -> F.pred list
val filter_hypotheses : F.var list -> F.pred list

Substitutions

val sigma : unit -> F.sigma

uses current pool

val alpha : unit -> F.sigma

freshen all variables

val subst : F.var list -> F.term list -> F.sigma

replace variables

val e_subst : (F.term -> F.term) -> F.term -> F.term

uses current pool

val p_subst : (F.term -> F.term) -> F.pred -> F.pred

uses current pool

Simplifiers

exception Contradiction
val is_literal : F.term -> bool
val iter_consequence_literals : (F.term -> unit) -> F.term -> unit

iter_consequence_literals assume_from_litteral hypothesis applies the function assume_from_litteral on literals that are a consequence of the hypothesis (i.e. in the hypothesis not (A && (B || C) ==> D), only A and not D are considered as consequence literals).

class type simplifier = object ... end
module For_export : sig ... end

For why3_api but circular dependency

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