Module Mem_utils

module Mem_utils: sig .. end

type kind = 
| CPtr
| Ptr
| Data of Cil_types.typ
type action = 
| Strip
| Id
type param = string * kind * action 
type proto = kind * param list 
module type Function = sig .. end
module Make: 
functor (F : Function-> sig .. end
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 = 
| Of_null of Cil_types.typ
| Value_of of Cil_types.typ
| No_pointed
val exp_type_of_pointed : Cil_types.exp -> pointed_expr_type