module Mem_utils: sig
.. end
type
kind =
type
action =
type
param = string * kind * action
type
proto = kind * param list
module type Function = sig
.. end
module Make:
type 'a
spec_gen = Cil_types.location ->
Cil_types.typ -> Cil_types.term -> Cil_types.term -> Cil_types.term -> 'a
location -> key -> s1 -> s2 -> len -> spec_result
val mem2s_spec : requires:Cil_types.identified_predicate list spec_gen ->
assigns:Cil_types.assigns spec_gen ->
ensures:(Cil_types.termination_kind * Cil_types.identified_predicate) list
spec_gen ->
Cil_types.typ -> Cil_types.location -> Cil_types.fundec -> Cil_types.funspec
val mem2s_typing : Cil_types.typ option -> Cil_types.typ list -> bool
val memcpy_memmove_common_requires : Cil_types.identified_predicate list spec_gen
val memcpy_memmove_common_assigns : Cil_types.assigns spec_gen
val memcpy_memmove_common_ensures : string ->
(Cil_types.termination_kind * Cil_types.identified_predicate) list
spec_gen
type
pointed_expr_type =
val exp_type_of_pointed : Cil_types.exp -> pointed_expr_type