package frama-c

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

Locality

method set_local : cluster -> unit
method do_local : cluster -> bool

Visiting items

method vadt : Wp__.Lang.ADT.t -> unit
method vcomp : Frama_c_kernel.Cil_types.compinfo -> unit
method vicomp : Frama_c_kernel.Cil_types.compinfo -> unit
method vfield : Wp__.Lang.Field.t -> unit
method vtau : Wp__.Lang.F.tau -> unit
method vparam : Wp__.Lang.F.var -> unit
method vterm : Wp__.Lang.F.term -> unit
method vpred : Wp__.Lang.F.pred -> unit
method vsymbol : Wp__.Lang.lfun -> unit
method vlemma : Wp__.LogicUsage.logic_lemma -> unit
method vcluster : cluster -> unit
method vlibrary : string -> unit
method vgoal : axioms option -> Wp__.Lang.F.pred -> unit
method vtypes : unit

Visit all typedefs

method vsymbols : unit

Visit all definitions

method vlemmas : unit

Visit all lemmas

method vself : unit

Visit all records, types, defs and lemmas

Visited definitions

method virtual section : string -> unit

Comment

method virtual on_library : string -> unit

External library to import

method virtual on_cluster : cluster -> unit

Outer cluster to import

method virtual on_type : Frama_c_kernel.Cil_types.logic_type_info -> typedef -> unit

This local type must be defined

method virtual on_comp : Frama_c_kernel.Cil_types.compinfo -> (Wp__.Lang.field * Wp__.Lang.F.tau) list option -> unit

This local compinfo must be defined

method virtual on_icomp : Frama_c_kernel.Cil_types.compinfo -> (Wp__.Lang.field * Wp__.Lang.F.tau) list option -> unit

This local compinfo initialization must be defined

method virtual on_dlemma : dlemma -> unit

This local lemma must be defined

method virtual on_dfun : dfun -> unit

This local function must be defined

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