Module `Wp.MemBytes`Source

Sourcemodule Logic = Qed.Logic

Sourcemodule Why3 : sig ... end

Sourceval datatype : string

Sourceval lc_name : string

Sourceval dkey_state : Wp_parameters.category

Sourceval dkey_model : Wp_parameters.category

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

Sourcetype loc = Lang.F.term

Sourceval vars : Lang.F.term -> Lang.F.Vars.t

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 =

| RS_Field of Frama_c_kernel.Cil_types.fieldinfo * Lang.F.term
| 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

Source

val field_offset : 
  Frama_c_kernel.Cil_types.compinfo ->
  Frama_c_kernel.Cil_types.fieldinfo ->
  int

Sourcemodule ShiftFieldDef : sig ... end

Sourcemodule ShiftField : sig ... end

Sourcemodule Cobj : sig ... end

Sourcemodule ShiftGen : sig ... end

Sourcemodule Shift : sig ... end

Sourceval field : Lang.F.term -> Frama_c_kernel.Cil_types.fieldinfo -> Lang.F.term

Sourceval shift : Lang.F.term -> Ctypes.c_object -> Lang.F.term -> Lang.F.term

Sourceval allocated : Sigma.t -> Lang.F.term -> Lang.F.term

Sourceval s_valid : Sigma.t -> Sigs.acs -> Lang.F.term -> Lang.F.term -> Lang.F.pred

Sourceval s_invalid : Sigma.t -> Lang.F.term -> Lang.F.term -> Lang.F.pred

Sourceval segment : (Lang.F.term -> Lang.F.term -> 'a) -> Lang.F.term Sigs.rloc -> 'a

Sourceval valid : Sigma.t -> Sigs.acs -> Lang.F.term Sigs.rloc -> Lang.F.pred

Sourceval invalid : Sigma.t -> Lang.F.term Sigs.rloc -> Lang.F.pred

Sourceval included : Lang.F.term Sigs.rloc -> Lang.F.term Sigs.rloc -> Lang.F.pred

Sourceval separated : Lang.F.term Sigs.rloc -> Lang.F.term Sigs.rloc -> Lang.F.pred

Sourceval float_cluster : unit -> Definitions.cluster

Sourcemodule Float : sig ... end

Sourcemodule CODEC_FLOAT : sig ... end

Sourceval float_to_int : CODEC_FLOAT.key -> Lang.F.term -> Lang.F.term

Sourceval int_to_float : CODEC_FLOAT.key -> Lang.F.term -> Lang.F.term

Sourceval load_int_raw : Lang.F.term -> Ctypes.c_int -> Lang.F.term -> Lang.F.term

Sourceval load_int : Sigma.t -> Ctypes.c_int -> Lang.F.term -> Lang.F.term

Sourceval load_float : Sigma.t -> CODEC_FLOAT.key -> Lang.F.term -> Lang.F.term

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 is_init_atom : Sigma.t -> Ctypes.c_object -> Lang.F.term -> Lang.F.term

Source

val store_int : 
  Sigma.t ->
  Ctypes.c_int ->
  Lang.F.term ->
  Lang.F.term ->
  Chunk.t * Lang.F.term

Source

val store_float : 
  Sigma.t ->
  Ctypes.c_float ->
  Lang.F.term ->
  Lang.F.term ->
  Chunk.t * Lang.F.term

Source

val store_pointer : 
  Sigma.t ->
  'a ->
  Lang.F.term ->
  Lang.F.term ->
  Chunk.t * Lang.F.term

Source

val store_init_raw : 
  Lang.F.term ->
  int ->
  Lang.F.term ->
  Lang.F.term ->
  Lang.F.term

Source

val set_init_atom : 
  Sigma.t ->
  Ctypes.c_object ->
  Lang.F.term ->
  Lang.F.term ->
  Chunk.t * Lang.F.term

Sourcemodule Model : sig ... end

include sig ... end

Source

val load : 
  Model.Sigma.t ->
  Ctypes.c_object ->
  Model.loc ->
  Model.loc Sigs.value

Sourceval load_init : Model.Sigma.t -> Ctypes.c_object -> Model.loc -> Lang.F.term

Sourceval load_value : Model.Sigma.t -> Ctypes.c_object -> Model.loc -> Lang.F.term

Source

val havoc : 
  Model.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  Model.loc ->
  Sigs.equation list

Source

val havoc_length : 
  Model.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  Model.loc ->
  Lang.F.term ->
  Sigs.equation list

Source

val stored : 
  Model.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  Model.loc ->
  Lang.F.term ->
  Sigs.equation list

Source

val stored_init : 
  Model.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  Model.loc ->
  Lang.F.term ->
  Sigs.equation list

Source

val copied : 
  Model.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  Model.loc ->
  Model.loc ->
  Sigs.equation list

Source

val copied_init : 
  Model.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  Model.loc ->
  Model.loc ->
  Sigs.equation list

Source

val assigned : 
  Model.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  Model.loc Sigs.sloc ->
  Sigs.equation list

Sourceval initialized : Model.Sigma.t -> Model.loc Sigs.rloc -> Lang.F.pred

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 null : Lang.F.term

Sourceval literal : eid:int -> Cstring.cst -> Lang.F.term

Sourceval cvar : Frama_c_kernel.Cil_types.varinfo -> Lang.F.term

Sourceval global : 'a -> Lang.F.term -> Lang.F.pred

Sourcetype state = chunk Lang.F.Tmap.t

Sourceval lookup_a : Lang.F.term -> Sigs.s_lval

Sourceval lookup_f : Lang.Fun.t -> Lang.F.QED.term list -> Sigs.s_lval

Sourceval lookup_lv : Lang.F.QED.term -> Sigs.s_lval

Sourceval mchunk : Chunk.t -> Sigs.mval

Sourceval lookup : Chunk.t Lang.F.Tmap.t -> Lang.F.term -> Sigs.mval

Sourceval state : Sigma.t -> Sigma.chunk Lang.F.Tmap.t

Source

val 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

Source

val apply : 
  (Lang.F.Tmap.key -> Lang.F.Tmap.key) ->
  'a Lang.F.Tmap.t ->
  'a Lang.F.Tmap.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 is_null : Lang.F.term -> Lang.F.pred

Sourceval loc_eq : Lang.F.term -> Lang.F.term -> Lang.F.pred

Sourceval loc_lt : Lang.F.term -> Lang.F.term -> Lang.F.pred

Sourceval loc_leq : Lang.F.term -> Lang.F.term -> Lang.F.pred

Sourceval loc_neq : Lang.F.term -> Lang.F.term -> Lang.F.pred

Sourceval loc_diff : 'a -> Lang.F.term -> Lang.F.term -> Lang.F.term

Sourceval pointer_cluster : unit -> Definitions.cluster

Sourcemodule PointersProperties : sig ... end

Sourceval framed : Lang.F.term -> Lang.F.pred

Sourceval frame : Sigma.t -> Lang.F.pred list

Sourceval is_well_formed : Sigma.t -> Lang.F.pred

Sourceval alloc : Sigma.t -> Frama_c_kernel.Cil_types.varinfo list -> Sigma.t

Source

val scope : 
  Sigma.t Sigs.sequence ->
  Sigs.scope ->
  Frama_c_kernel.Cil_types.varinfo list ->
  Lang.F.pred list

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/MemBytes/index.html

Module `Wp.MemBytes`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/MemBytes/index.html

Module Wp.MemBytesSource

Module `Wp.MemBytes`Source