package frama-c

  1. Overview
  2. Docs
package frama-c
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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct