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

module Chunk = Chunk

module Sigma = Sigma

val name : string

type nonrec loc = loc

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

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 to_addr : 'a -> 'b

val to_region_pointer : 'a -> int * 'b

val of_region_pointer : 'a -> 'b -> 'c -> 'd

val value_footprint : 'a -> 'b -> Sigma.Chunk.Set.t

val init_footprint : 'a -> 'b -> Sigma.Chunk.Set.t

val frames : 
  Ctypes.c_object ->
  Lang.F.term ->
  Chunk.t ->
  (string
   * (Lang.F.var, Lang.lfun) Qed.Engine.ftrigger list
   * Lang.F.pred list
   * Lang.F.term
   * Lang.F.term)
    list

val last : Sigma.t -> Ctypes.c_object -> Lang.F.term -> Lang.F.term

val havoc : 
  Ctypes.c_object ->
  Lang.F.term ->
  length:Lang.F.term ->
  Chunk.t ->
  fresh:Lang.F.term ->
  current:Lang.F.term ->
  Lang.F.term

val eqmem : 
  Ctypes.c_object ->
  Lang.F.term ->
  'a ->
  Lang.F.term ->
  Lang.F.term ->
  Lang.F.pred

val eqmem_forall : 
  Ctypes.c_object ->
  Lang.F.term ->
  'a ->
  Lang.F.term ->
  Lang.F.term ->
  Lang.F.var list * Lang.F.pred * Lang.F.pred

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

val is_init_range : 
  Sigma.t ->
  Ctypes.c_object ->
  Lang.F.term ->
  Lang.F.term ->
  Lang.F.pred

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

val set_init : 
  Ctypes.c_object ->
  Lang.F.term ->
  length:Lang.F.term ->
  'a ->
  current:Lang.F.term ->
  Lang.F.term