sig
type kind = CPtr | Ptr | Data of Cil_types.typ
type action = Strip | Id
type param = string * Mem_utils.kind * Mem_utils.action
type proto = Mem_utils.kind * Mem_utils.param list
module type Function =
sig
val name : string
val prototype : unit -> Mem_utils.proto
val well_typed : Cil_types.typ option -> Cil_types.typ list -> bool
end
module Make :
functor (F : Function) ->
sig
val generate_function_type : Cil_types.typ -> Cil_types.typ
val generate_prototype : Cil_types.typ -> string * Cil_types.typ
val well_typed_call :
Cil_types.lval option ->
Cil_types.varinfo -> Cil_types.exp list -> bool
val retype_args :
Cil_types.typ -> Cil_types.exp list -> Cil_types.exp list
val key_from_call :
Cil_types.lval option ->
Cil_types.varinfo -> Cil_types.exp list -> Cil_types.typ
end
type 'a spec_gen =
Cil_types.location ->
Cil_types.typ ->
Cil_types.term -> Cil_types.term -> Cil_types.term -> 'a
val mem2s_spec :
requires:Cil_types.identified_predicate list Mem_utils.spec_gen ->
assigns:Cil_types.assigns Mem_utils.spec_gen ->
ensures:(Cil_types.termination_kind * Cil_types.identified_predicate)
list Mem_utils.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 Mem_utils.spec_gen
val memcpy_memmove_common_assigns : Cil_types.assigns Mem_utils.spec_gen
val memcpy_memmove_common_ensures :
string ->
(Cil_types.termination_kind * Cil_types.identified_predicate) list
Mem_utils.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 -> Mem_utils.pointed_expr_type
end