module Mem_utils: sig
.. end
receives the type of the lvalue and the types of the arguments received
for a call to the function and returns
true
iff they are correct.
The received types depend on the
prototype
of the module.
- if the kind is
Data t
-> it is the exact type of the expr/lvalue
- it the kind is
(C)Ptr
-> it is the pointed type of the expr/lvalue
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.fundec -> Cil_types.location -> 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