Why3 (p.frama-c.30.0~beta.doc.frama-c-wp.core.Wp.MemBytes.Why3)

frama-c
- README
- Library Pdg_types
  - Pdg_types
- Library frama-c-alias.core
  - Alias
- Library frama-c-aorai.core
  - Aorai
- Library frama-c-api-generator.core
  - Api_generator
- Library frama-c-callgraph.core
  - Callgraph
- Library frama-c-constant_propagation.core
  - Constant_Propagation
- Library frama-c-dive.core
  - Dive
- Library frama-c-e-acsl.core
  - E_ACSL
- Library frama-c-eva.core
  - Eva
- Library frama-c-eva.gui
  - Eva_gui
- Library frama-c-from.core
  - From
- Library frama-c-from.gui
  - From_gui
- Library frama-c-impact.core
  - Impact
- Library frama-c-impact.gui
  - Impact_gui
- Library frama-c-inout.core
  - Inout
- Library frama-c-instantiate.core
  - Instantiate
- Library frama-c-loop-analysis.core
  - LoopAnalysis
- Library frama-c-markdown-report.core
  - Markdown_report
- Library frama-c-markdown-report.eva-info
- Library frama-c-metrics.core
  - Metrics
- Library frama-c-metrics.gui
  - Metrics_gui
- Library frama-c-nonterm.core
  - Nonterm
- Library frama-c-obfuscator.core
  - Obfuscator
- Library frama-c-occurrence.core
  - Occurrence
- Library frama-c-occurrence.gui
  - Occurrence_gui
- Library frama-c-pdg.core
  - Pdg
- Library frama-c-pdg.types
- Library frama-c-reduc.core
  - Reduc
- Library frama-c-region.core
  - Region
- Library frama-c-report.core
  - Report
- Library frama-c-rtegen.core
  - RteGen
- Library frama-c-rtegen.gui
  - Rtegen_gui
- Library frama-c-scope.core
  - Scope
- Library frama-c-scope.gui
  - Scope_gui
- Library frama-c-security_slicing.core
  - Security_slicing
- Library frama-c-security_slicing.gui
  - Security_slicing_gui
- Library frama-c-server.core
  - Server
- Library frama-c-slicing.core
  - Slicing
- Library frama-c-slicing.gui
  - Slicing_gui
- Library frama-c-sparecode.core
  - Sparecode
- Library frama-c-studia.core
  - Studia
- Library frama-c-studia.gui
  - Studia_gui
- Library frama-c-users.core
  - Users
- Library frama-c-variadic.core
  - Variadic
- Library frama-c-wp.core
  - Wp
- Library frama-c-wp.gui
  - Wp_gui
- Library frama-c.analysis-scripts
  - Analysis_scripts
- Library frama-c.boot
  - Frama_c_boot
- Library frama-c.gui
  - Frama_c_gui
- Library frama-c.init
- Library frama-c.kernel
  - Frama_c_kernel
- Library frama_c_very_first_cmdline
- Library frama_c_very_first_gui
- Library markdown_report_eva_info
  - Markdown_report_eva_info
- Library qed
  - Qed
- Sources

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

Source

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

Sourceval p_cinits : Lang.lfun

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

Sourceval p_sconst : Lang.lfun

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

Sourceval p_eqmem : Lang.lfun

Source

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

Sourceval p_is_init_range : Lang.lfun

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

Sourceval f_set_init_range : Lang.lfun

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

Source

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

Sourceval f_raw_get : Lang.lfun

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

Sourceval f_raw_set : Lang.lfun

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

Sourceval p_bytes : Lang.lfun

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

Sourceval f_read_uint8 : Lang.lfun

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

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 read_sint8 : Lang.F.term -> Lang.F.term -> Lang.F.term

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 write_uint8 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

Sourceval f_write_uint16 : Lang.lfun

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

Sourceval f_write_uint32 : Lang.lfun

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

Sourceval f_write_uint64 : Lang.lfun

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

Sourceval f_write_sint8 : Lang.lfun

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

Sourceval f_write_sint16 : Lang.lfun

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

Sourceval f_write_sint32 : Lang.lfun

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

Sourceval f_write_sint64 : Lang.lfun

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

Sourceval f_read_init8 : Lang.lfun

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

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 write_init8 : Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term

Sourceval f_write_init16 : Lang.lfun

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

Sourceval f_write_init32 : Lang.lfun

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

Sourceval f_write_init64 : Lang.lfun

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