package frama-c

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

Generated Logic Definitions

type cluster
val dummy : unit -> cluster
val cluster : id:string -> ?title:string -> ?position:Frama_c_kernel.Filepath.position -> unit -> cluster
val axiomatic : LogicUsage.axiomatic -> cluster
val matrix : unit -> cluster
val cluster_id : cluster -> string

Unique

val cluster_title : cluster -> string
val cluster_position : cluster -> Frama_c_kernel.Filepath.position option
val cluster_age : cluster -> int
val cluster_compare : cluster -> cluster -> int
val pp_cluster : Format.formatter -> cluster -> unit
val iter : (cluster -> unit) -> unit
type dlemma = {
  1. l_name : string;
  2. l_cluster : cluster;
  3. l_kind : Frama_c_kernel.Cil_types.predicate_kind;
  4. l_types : int;
  5. l_forall : Lang.F.var list;
  6. l_triggers : trigger list list;
    (*

    OR of AND-triggers

    *)
  7. l_lemma : Lang.F.pred;
}
type definition =
  1. | Logic of Lang.F.tau
  2. | Function of Lang.F.tau * recursion * Lang.F.term
  3. | Predicate of recursion * Lang.F.pred
  4. | Inductive of dlemma list
and recursion =
  1. | Def
  2. | Rec
type dfun = {
  1. d_lfun : Lang.lfun;
  2. d_cluster : cluster;
  3. d_types : int;
  4. d_params : Lang.F.var list;
  5. d_definition : definition;
}
module Trigger : sig ... end
val find_symbol : Lang.lfun -> dfun
  • raises Not_found

    if symbol is not compiled (yet)

val define_symbol : dfun -> unit
val update_symbol : dfun -> unit
val find_name : string -> dlemma
val find_lemma : LogicUsage.logic_lemma -> dlemma
  • raises Not_found

    if lemma is not compiled (yet)

val compile_lemma : (LogicUsage.logic_lemma -> dlemma) -> LogicUsage.logic_lemma -> unit
val define_lemma : dlemma -> unit
val call_fun : result:Lang.F.tau -> Lang.lfun -> (Lang.lfun -> dfun) -> Lang.F.term list -> Lang.F.term
val call_pred : Lang.lfun -> (Lang.lfun -> dfun) -> Lang.F.term list -> Lang.F.pred
type axioms = cluster * LogicUsage.logic_lemma list
class virtual visitor : cluster -> object ... end
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