package frama-c

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

Module Wp.MemBytesSource

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