Wp.MemBytes
module Logic = Qed.Logic
module Why3 : sig ... end
val dkey_state : Wp_parameters.category
val dkey_model : Wp_parameters.category
val no_binder : 'a Sigs.binder
val configure_ia : 'a -> 'b Sigs.binder
module Chunk : sig ... end
module Heap : sig ... end
module Sigma : sig ... end
type loc = Lang.F.term
val vars : Lang.F.term -> Lang.F.Vars.t
val occurs : Lang.F.var -> Lang.F.term -> bool
type chunk = Chunk.t
type sigma = Sigma.t
type domain = Sigma.domain
val comp_cluster : unit -> Definitions.cluster
val shift_cluster : unit -> Definitions.cluster
module OPAQUE_COMP_LENGTH : sig ... end
val protected_sizeof_object : Ctypes.c_object -> Lang.F.term
type shift =
| RS_Field of Frama_c_kernel.Cil_types.fieldinfo * Lang.F.term
| RS_Index of Lang.F.term
val phi_base : Lang.F.term list -> Lang.F.term
val phi_field : Lang.F.term -> Lang.F.term list -> Lang.F.term
val phi_index : Lang.F.term -> Lang.F.term list -> Lang.F.term
module RegisterShift : sig ... end
val field_offset :
Frama_c_kernel.Cil_types.compinfo ->
Frama_c_kernel.Cil_types.fieldinfo ->
int
module ShiftFieldDef : sig ... end
module ShiftField : sig ... end
module Cobj : sig ... end
module ShiftGen : sig ... end
module Shift : sig ... end
val field : Lang.F.term -> Frama_c_kernel.Cil_types.fieldinfo -> Lang.F.term
val shift : Lang.F.term -> Ctypes.c_object -> Lang.F.term -> Lang.F.term
val allocated : Sigma.t -> Lang.F.term -> Lang.F.term
val s_valid : Sigma.t -> Sigs.acs -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val s_invalid : Sigma.t -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val segment : (Lang.F.term -> Lang.F.term -> 'a) -> Lang.F.term Sigs.rloc -> 'b
val valid : Sigma.t -> Sigs.acs -> Lang.F.term Sigs.rloc -> Lang.F.pred
val invalid : Sigma.t -> Lang.F.term Sigs.rloc -> Lang.F.pred
val included : Lang.F.term Sigs.rloc -> Lang.F.term Sigs.rloc -> Lang.F.pred
val separated : Lang.F.term Sigs.rloc -> Lang.F.term Sigs.rloc -> Lang.F.pred
val float_cluster : unit -> Definitions.cluster
module Float : sig ... end
module CODEC_FLOAT : sig ... end
val float_to_int : CODEC_FLOAT.key -> Lang.F.term -> Lang.F.term
val int_to_float : CODEC_FLOAT.key -> Lang.F.term -> Lang.F.term
val load_int_raw : Lang.F.term -> Ctypes.c_int -> Lang.F.term -> Lang.F.term
val load_int : Sigma.t -> Ctypes.c_int -> Lang.F.term -> Lang.F.term
val load_float : Sigma.t -> CODEC_FLOAT.key -> Lang.F.term -> Lang.F.term
val load_pointer_raw : Lang.F.term -> 'a -> Lang.F.term -> Lang.F.term
val load_pointer : Sigma.t -> 'a -> Lang.F.term -> Lang.F.term
val is_init_atom : Sigma.t -> Ctypes.c_object -> Lang.F.term -> Lang.F.term
val store_int :
Sigma.t ->
Ctypes.c_int ->
Lang.F.term ->
Lang.F.term ->
Chunk.t * Lang.F.term
val store_float :
Sigma.t ->
Ctypes.c_float ->
Lang.F.term ->
Lang.F.term ->
Chunk.t * Lang.F.term
val store_pointer :
Sigma.t ->
'a ->
Lang.F.term ->
Lang.F.term ->
Chunk.t * Lang.F.term
val store_init_raw :
Lang.F.term ->
int ->
Lang.F.term ->
Lang.F.term ->
Lang.F.term
val set_init_atom :
Sigma.t ->
Ctypes.c_object ->
Lang.F.term ->
Lang.F.term ->
Chunk.t * Lang.F.term
module Model : sig ... end
include sig ... end
val load :
Model.Sigma.t ->
Ctypes.c_object ->
Model.loc ->
Model.loc Sigs.value
val load_init : Model.Sigma.t -> Ctypes.c_object -> Model.loc -> Lang.F.term
val load_value : Model.Sigma.t -> Ctypes.c_object -> Model.loc -> Lang.F.term
val havoc :
Model.Sigma.t Sigs.sequence ->
Ctypes.c_object ->
Model.loc ->
Sigs.equation list
val havoc_length :
Model.Sigma.t Sigs.sequence ->
Ctypes.c_object ->
Model.loc ->
Lang.F.term ->
Sigs.equation list
val stored :
Model.Sigma.t Sigs.sequence ->
Ctypes.c_object ->
Model.loc ->
Lang.F.term ->
Sigs.equation list
val stored_init :
Model.Sigma.t Sigs.sequence ->
Ctypes.c_object ->
Model.loc ->
Lang.F.term ->
Sigs.equation list
val copied :
Model.Sigma.t Sigs.sequence ->
Ctypes.c_object ->
Model.loc ->
Model.loc ->
Sigs.equation list
val copied_init :
Model.Sigma.t Sigs.sequence ->
Ctypes.c_object ->
Model.loc ->
Model.loc ->
Sigs.equation list
val assigned :
Model.Sigma.t Sigs.sequence ->
Ctypes.c_object ->
Model.loc Sigs.sloc ->
Sigs.equation list
val initialized : Model.Sigma.t -> Model.loc Sigs.rloc -> Lang.F.pred
val cluster_globals : unit -> Definitions.cluster
module RegisterBASE : sig ... end
module BASE : sig ... end
module LITERAL : sig ... end
module EID : sig ... end
module STRING : sig ... end
val pretty : Stdlib.Format.formatter -> Lang.F.term -> unit
val null : Lang.F.term
val literal : eid:int -> Cstring.cst -> Lang.F.term
val cvar : Frama_c_kernel.Cil_types.varinfo -> Lang.F.term
val global : 'a -> Lang.F.term -> Lang.F.pred
type state = chunk Lang.F.Tmap.t
val lookup_a : Lang.F.term -> Sigs.s_lval
val lookup_f : Lang.Fun.t -> Lang.F.QED.term list -> Sigs.s_lval
val lookup_lv : Lang.F.QED.term -> Sigs.s_lval
val lookup : Chunk.t Lang.F.Tmap.t -> Lang.F.term -> Sigs.mval
val state : Sigma.t -> Sigma.chunk Lang.F.Tmap.t
val iter :
(Sigs.mval -> Lang.F.Tmap.key -> unit) ->
Chunk.t Lang.F.Tmap.t ->
unit
val updates : 'a -> 'b -> 'c Frama_c_kernel.Bag.t
val apply :
(Lang.F.Tmap.key -> Lang.F.Tmap.key) ->
'a Lang.F.Tmap.t ->
'b Lang.F.Tmap.t
val base_addr : Lang.F.term -> Lang.F.term
val base_offset : Lang.F.term -> Lang.F.term
val block_length : Sigma.t -> 'a -> Lang.F.term -> Lang.F.term
val cast : 'a -> Lang.F.term -> Lang.F.term
val loc_of_int : 'a -> Lang.F.term -> Lang.F.term
val int_of_loc : 'a -> Lang.F.term -> Lang.F.term
val domain : 'a -> 'b -> Sigma.Chunk.Set.t
val is_null : Lang.F.term -> Lang.F.pred
val loc_eq : Lang.F.term -> Lang.F.term -> Lang.F.pred
val loc_lt : Lang.F.term -> Lang.F.term -> Lang.F.pred
val loc_leq : Lang.F.term -> Lang.F.term -> Lang.F.pred
val loc_neq : Lang.F.term -> Lang.F.term -> Lang.F.pred
val loc_diff : 'a -> Lang.F.term -> Lang.F.term -> Lang.F.term
val pointer_cluster : unit -> Definitions.cluster
module PointersProperties : sig ... end
val framed : Lang.F.term -> Lang.F.pred
val frame : Sigma.t -> Lang.F.pred list
val is_well_formed : Sigma.t -> Lang.F.pred
val alloc : Sigma.t -> Frama_c_kernel.Cil_types.varinfo list -> Sigma.t
val scope :
Sigma.t Sigs.sequence ->
Sigs.scope ->
Frama_c_kernel.Cil_types.varinfo list ->
Lang.F.pred list