package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Logic = Qed.Logic
module Why3 : sig ... end
val datatype : string
val lc_name : string
val dkey_state : Wp_parameters.category
val dkey_model : Wp_parameters.category
val configure : unit -> unit -> unit
val no_binder : 'a Sigs.binder
val configure_ia : 'a -> 'b Sigs.binder
val hypotheses : 'a -> 'a
module Chunk : sig ... end
module Heap : sig ... end
module Sigma : sig ... end
type loc = Lang.F.term
val occurs : Lang.F.var -> Lang.F.term -> bool
type chunk = Chunk.t
type sigma = Sigma.t
type domain = Sigma.domain
type segment = loc Sigs.rloc
val comp_cluster : unit -> Definitions.cluster
val shift_cluster : unit -> Definitions.cluster
module OPAQUE_COMP_LENGTH : sig ... end
val protected_sizeof_object : Ctypes.c_object -> Lang.F.term
type shift =
  1. | RS_Field of Frama_c_kernel.Cil_types.fieldinfo * Lang.F.term
  2. | RS_Index of Lang.F.term
val phi_base : Lang.F.term list -> Lang.F.term
val phi_field : Lang.F.term -> Lang.F.term list -> Lang.F.term
val phi_index : Lang.F.term -> Lang.F.term list -> Lang.F.term
module RegisterShift : sig ... end
module ShiftFieldDef : sig ... end
module ShiftField : sig ... end
module Cobj : sig ... end
module ShiftGen : sig ... end
module Shift : sig ... end
val allocated : Sigma.t -> Lang.F.term -> Lang.F.term
val s_invalid : Sigma.t -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val segment : (Lang.F.term -> Lang.F.term -> 'a) -> Lang.F.term Sigs.rloc -> 'a
val float_cluster : unit -> Definitions.cluster
module Float : sig ... end
module CODEC_FLOAT : sig ... end
val float_to_int : CODEC_FLOAT.key -> Lang.F.term -> Lang.F.term
val int_to_float : CODEC_FLOAT.key -> Lang.F.term -> Lang.F.term
val load_int_raw : Lang.F.term -> Ctypes.c_int -> Lang.F.term -> Lang.F.term
val load_pointer_raw : Lang.F.term -> 'a -> Lang.F.term -> Lang.F.term
val load_pointer : Sigma.t -> 'a -> Lang.F.term -> Lang.F.term
val is_init_atom : Sigma.t -> Ctypes.c_object -> Lang.F.term -> Lang.F.term
val store_pointer : Sigma.t -> 'a -> Lang.F.term -> Lang.F.term -> Chunk.t * Lang.F.term
val store_init_raw : Lang.F.term -> int -> Lang.F.term -> Lang.F.term -> Lang.F.term
module Model : sig ... end
include sig ... end
val cluster_globals : unit -> Definitions.cluster
val globals : int
val locals : int
val formals : int
module RegisterBASE : sig ... end
module BASE : sig ... end
module LITERAL : sig ... end
module EID : sig ... end
module STRING : sig ... end
val pretty : Stdlib.Format.formatter -> Lang.F.term -> unit
val null : Lang.F.term
val literal : eid:int -> Cstring.cst -> Lang.F.term
val global : 'a -> Lang.F.term -> Lang.F.pred
type state = chunk Lang.F.Tmap.t
val lookup_a : Lang.F.term -> Sigs.s_lval
val lookup_f : Lang.Fun.t -> Lang.F.QED.term list -> Sigs.s_lval
val lookup_lv : Lang.F.QED.term -> Sigs.s_lval
val mchunk : Chunk.t -> Sigs.mval
val iter : (Sigs.mval -> Lang.F.Tmap.key -> unit) -> Chunk.t Lang.F.Tmap.t -> unit
val updates : 'a -> 'b -> 'c Frama_c_kernel.Bag.t
val pointer_loc : 'a -> 'a
val pointer_val : 'a -> 'a
val base_addr : Lang.F.term -> Lang.F.term
val base_offset : Lang.F.term -> Lang.F.term
val block_length : Sigma.t -> 'a -> Lang.F.term -> Lang.F.term
val cast : 'a -> Lang.F.term -> Lang.F.term
val loc_of_int : 'a -> Lang.F.term -> Lang.F.term
val int_of_loc : 'a -> Lang.F.term -> Lang.F.term
val domain : 'a -> 'b -> Sigma.Chunk.Set.t
val is_null : Lang.F.term -> Lang.F.pred
val loc_leq : Lang.F.term -> Lang.F.term -> Lang.F.pred
val loc_neq : Lang.F.term -> Lang.F.term -> Lang.F.pred
val loc_diff : 'a -> Lang.F.term -> Lang.F.term -> Lang.F.term
val pointer_cluster : unit -> Definitions.cluster
module PointersProperties : sig ... end
val framed : Lang.F.term -> Lang.F.pred
val frame : Sigma.t -> Lang.F.pred list
val is_well_formed : Sigma.t -> Lang.F.pred
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