Functor Wp.CodeSemantics.Make

module Make: 
functor (M : Wp.Memory.Model) -> sig .. end
Parameters:
M : Wp.Memory.Model

type loc = M.loc 
type value = loc Wp.Memory.value 
type sigma = M.Sigma.t 
val cval : value -> Wp.Lang.F.term
val cloc : value -> loc
val cast : Cil_types.typ ->
Cil_types.typ -> value -> value
val equal_typ : Cil_types.typ ->
value -> value -> Wp.Lang.F.pred
val equal_obj : Wp.Ctypes.c_object ->
value -> value -> Wp.Lang.F.pred
val exp : sigma -> Cil_types.exp -> value
val cond : sigma -> Cil_types.exp -> Wp.Lang.F.pred
val lval : sigma -> Cil_types.lval -> loc
val call : sigma -> Cil_types.exp -> loc
val loc_of_exp : sigma -> Cil_types.exp -> loc
val val_of_exp : sigma -> Cil_types.exp -> Wp.Lang.F.term
val return : sigma ->
Cil_types.typ -> Cil_types.exp -> Wp.Lang.F.term
val is_zero : sigma ->
Wp.Ctypes.c_object -> loc -> Wp.Lang.F.pred
val is_exp_range : sigma ->
loc ->
Wp.Ctypes.c_object ->
Wp.Lang.F.term ->
Wp.Lang.F.term -> value option -> Wp.Lang.F.pred
val instance_of : loc -> Cil_types.kernel_function -> Wp.Lang.F.pred