package frama-c

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module MemBytes.Why3Source

Sourceval library : string
Sourceval t_vblock : ('a, 'b) Qed.Logic.datatype
Sourceval t_memory : ('a, 'b) Qed.Logic.datatype
Sourceval t_iblock : ('a, 'b) Qed.Logic.datatype
Sourceval t_init : ('a, 'b) Qed.Logic.datatype
Sourceval ty_fst_arg : 'a option list -> 'a
Sourceval l_havoc : Qed.Engine.link
Sourceval f_havoc : Lang.lfun
Sourceval p_cinits : Lang.lfun
Sourceval p_sconst : Lang.lfun
Sourceval p_eqmem : Lang.lfun
Sourceval p_is_init_range : Lang.lfun
Sourceval f_set_init_range : Lang.lfun
Sourceval ty_fst_arg_val : ('a, 'b) Qed.Logic.datatype option list -> ('a, 'b) Qed.Logic.datatype
Sourceval f_raw_get : Lang.lfun
Sourceval f_raw_set : Lang.lfun
Sourceval p_bytes : Lang.lfun
Sourceval f_read_uint8 : Lang.lfun
Sourceval f_read_uint16 : Lang.lfun
Sourceval read_uint16 : Lang.F.term -> Lang.F.term -> Lang.F.term
Sourceval f_read_uint32 : Lang.lfun
Sourceval read_uint32 : Lang.F.term -> Lang.F.term -> Lang.F.term
Sourceval f_read_uint64 : Lang.lfun
Sourceval read_uint64 : Lang.F.term -> Lang.F.term -> Lang.F.term
Sourceval f_read_sint8 : Lang.lfun
Sourceval f_read_sint16 : Lang.lfun
Sourceval read_sint16 : Lang.F.term -> Lang.F.term -> Lang.F.term
Sourceval f_read_sint32 : Lang.lfun
Sourceval read_sint32 : Lang.F.term -> Lang.F.term -> Lang.F.term
Sourceval f_read_sint64 : Lang.lfun
Sourceval read_sint64 : Lang.F.term -> Lang.F.term -> Lang.F.term
Sourceval f_write_uint8 : Lang.lfun
Sourceval f_write_uint16 : Lang.lfun
Sourceval f_write_uint32 : Lang.lfun
Sourceval f_write_uint64 : Lang.lfun
Sourceval f_write_sint8 : Lang.lfun
Sourceval f_write_sint16 : Lang.lfun
Sourceval f_write_sint32 : Lang.lfun
Sourceval f_write_sint64 : Lang.lfun
Sourceval f_read_init8 : Lang.lfun
Sourceval f_read_init16 : Lang.lfun
Sourceval read_init16 : Lang.F.term -> Lang.F.term -> Lang.F.term
Sourceval f_read_init32 : Lang.lfun
Sourceval read_init32 : Lang.F.term -> Lang.F.term -> Lang.F.term
Sourceval f_read_init64 : Lang.lfun
Sourceval read_init64 : Lang.F.term -> Lang.F.term -> Lang.F.term
Sourceval f_write_init8 : Lang.lfun
Sourceval f_write_init16 : Lang.lfun
Sourceval f_write_init32 : Lang.lfun
Sourceval f_write_init64 : Lang.lfun
OCaml

Innovation. Community. Security.