MemBytes (frama-c-wp.Wp.MemBytes)

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 -> 'b

module Chunk : sig ... end

module Heap : sig ... end

module Sigma : sig ... end

type loc = Lang.F.term

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

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 =

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

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

module ShiftFieldDef : sig ... end

module ShiftField : sig ... end

module Cobj : sig ... end

module ShiftGen : sig ... end

module Shift : sig ... end

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

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

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

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

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 -> 'b

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

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

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

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

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

val load_float : Sigma.t -> CODEC_FLOAT.key -> 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_int : 
  Sigma.t ->
  Ctypes.c_int ->
  Lang.F.term ->
  Lang.F.term ->
  Chunk.t * Lang.F.term

val store_float : 
  Sigma.t ->
  Ctypes.c_float ->
  Lang.F.term ->
  Lang.F.term ->
  Chunk.t * 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

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

module Model : sig ... end

include sig ... end

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

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

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

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

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

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

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

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

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

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

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

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 cvar : Frama_c_kernel.Cil_types.varinfo -> 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 lookup : Chunk.t Lang.F.Tmap.t -> Lang.F.term -> Sigs.mval

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

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

val pointer_loc : 'a -> 'b

val pointer_val : 'a -> 'b

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

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

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

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