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