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

val library : string

val t_vblock : ('a, 'b) Qed.Logic.datatype

val t_memory : ('a, 'b) Qed.Logic.datatype

val t_iblock : ('a, 'b) Qed.Logic.datatype

val t_init : ('a, 'b) Qed.Logic.datatype

val ty_fst_arg : 'a option list -> 'b

val l_havoc : Qed.Engine.link

val f_havoc : Lang.lfun

val havoc : 
  Lang.F.term ->
  Lang.F.term ->
  Lang.F.term ->
  Lang.F.term ->
  Lang.F.term

val p_cinits : Lang.lfun

val cinits : Lang.F.term -> Lang.F.pred

val p_sconst : Lang.lfun

val sconst : Lang.F.term -> Lang.F.pred

val p_eqmem : Lang.lfun

val eqmem : 
  Lang.F.term ->
  Lang.F.term ->
  Lang.F.term ->
  Lang.F.term ->
  Lang.F.pred

val p_is_init_range : Lang.lfun

val is_init_range : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.pred

val f_set_init_range : Lang.lfun

val set_init_range : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val ty_fst_arg_val : 
  ('a, 'b) Qed.Logic.datatype option list ->
  ('c, 'd) Qed.Logic.datatype

val f_raw_get : Lang.lfun

val raw_get : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_raw_set : Lang.lfun

val raw_set : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val p_bytes : Lang.lfun

val bytes : Lang.F.term -> Lang.F.pred

val f_read_uint8 : Lang.lfun

val read_uint8 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_read_uint16 : Lang.lfun

val read_uint16 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_read_uint32 : Lang.lfun

val read_uint32 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_read_uint64 : Lang.lfun

val read_uint64 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_read_sint8 : Lang.lfun

val read_sint8 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_read_sint16 : Lang.lfun

val read_sint16 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_read_sint32 : Lang.lfun

val read_sint32 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_read_sint64 : Lang.lfun

val read_sint64 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_uint8 : Lang.lfun

val write_uint8 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_uint16 : Lang.lfun

val write_uint16 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_uint32 : Lang.lfun

val write_uint32 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_uint64 : Lang.lfun

val write_uint64 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_sint8 : Lang.lfun

val write_sint8 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_sint16 : Lang.lfun

val write_sint16 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_sint32 : Lang.lfun

val write_sint32 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_sint64 : Lang.lfun

val write_sint64 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val f_read_init8 : Lang.lfun

val read_init8 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_read_init16 : Lang.lfun

val read_init16 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_read_init32 : Lang.lfun

val read_init32 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_read_init64 : Lang.lfun

val read_init64 : Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_init8 : Lang.lfun

val write_init8 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_init16 : Lang.lfun

val write_init16 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_init32 : Lang.lfun

val write_init32 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

val f_write_init64 : Lang.lfun

val write_init64 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term