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