Module `Warray_.WArray`

type array = Word0.word Gen_map.Mz.t

val arr_data : BinNums.coq_Z -> array -> Word0.word Gen_map.Mz.t

val empty : BinNums.coq_Z -> array

val coq_PointerZ : Memory_model.pointer_op

val in_bound : BinNums.coq_Z -> array -> BinNums.coq_Z -> bool

val in_boundP : BinNums.coq_Z -> array -> BinNums.coq_Z -> Datatypes.reflect

val is_init : BinNums.coq_Z -> array -> BinNums.coq_Z -> bool

val is_initb : BinNums.coq_Z -> array -> BinNums.coq_Z -> bool

val get8 : 
  BinNums.coq_Z ->
  array ->
  BinNums.coq_Z ->
  (Utils0.error, Word0.word) Utils0.result

val set8 : 
  BinNums.coq_Z ->
  array ->
  BinNums.coq_Z ->
  Word0.word ->
  (Utils0.error, array) Utils0.result

val valid8P : 
  BinNums.coq_Z ->
  array ->
  BinNums.coq_Z ->
  Word0.word ->
  Datatypes.reflect

val array_CM : BinNums.coq_Z -> array Memory_model.coreMem

val in_range : BinNums.coq_Z -> BinNums.coq_Z -> Wsize.wsize -> bool

val in_rangeP : 
  BinNums.coq_Z ->
  BinNums.coq_Z ->
  Wsize.wsize ->
  Datatypes.reflect

val get : 
  BinNums.coq_Z ->
  Memory_model.aligned ->
  arr_access ->
  Wsize.wsize ->
  array ->
  BinNums.coq_Z ->
  Word0.word Utils0.exec

val set : 
  BinNums.coq_Z ->
  Wsize.wsize ->
  array ->
  Memory_model.aligned ->
  arr_access ->
  BinNums.coq_Z ->
  Word0.word ->
  array Utils0.exec

val fcopy : 
  Wsize.wsize ->
  BinNums.coq_Z ->
  array ->
  array ->
  BinNums.coq_Z ->
  BinNums.coq_Z ->
  (Utils0.error, array) Utils0.result

val copy : 
  Wsize.wsize ->
  BinNums.coq_Z ->
  array ->
  (Utils0.error, array) Utils0.result

val fill_aux : 
  BinNums.coq_Z ->
  Word0.word list ->
  (BinNums.coq_Z * array) Utils0.exec

val fill : BinNums.coq_Z -> Word0.word list -> array Utils0.exec

val get_sub_data : 
  arr_access ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  Word0.word Gen_map.Mz.t ->
  BinNums.coq_Z ->
  Word0.word Gen_map.Mz.t

val get_sub : 
  BinNums.coq_Z ->
  arr_access ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  array ->
  BinNums.coq_Z ->
  array Utils0.exec

val set_sub_data : 
  arr_access ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  Word0.word Gen_map.Mz.t ->
  BinNums.coq_Z ->
  Word0.word Gen_map.Mz.t ->
  Word0.word Gen_map.Mz.t

val set_sub : 
  BinNums.coq_Z ->
  arr_access ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  array ->
  BinNums.coq_Z ->
  array ->
  array Utils0.exec

val cast : 
  BinNums.coq_Z ->
  BinNums.coq_Z ->
  array ->
  (Utils0.error, array) Utils0.result

val of_list : Wsize.wsize -> Word0.word list -> array

val is_uincl : BinNums.coq_Z -> BinNums.coq_Z -> array -> array -> bool

val is_uinclP : 
  BinNums.coq_Z ->
  BinNums.coq_Z ->
  array ->
  array ->
  Datatypes.reflect

package jasmin

Module Warray_.WArray

Module `Warray_.WArray`