package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 -> 'a
val l_havoc : Qed.Engine.link
val f_havoc : Lang.lfun
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 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 -> ('a, 'b) 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 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
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