functor (M : Memory.Model) ->
sig
type loc = M.loc
type value = M.loc Memory.value
type sigma = M.Sigma.t
val cval : M.loc Memory.value -> Lang.F.term
val cloc : M.loc Memory.value -> M.loc
val is_zero_int : M.loc Memory.value -> Lang.F.pred
val is_zero_float : M.loc Memory.value -> Lang.F.pred
val is_zero_ptr : M.loc Memory.value -> Lang.F.pred
val is_zero : M.sigma -> Ctypes.c_object -> M.loc -> Lang.F.pred
val is_zero_range :
M.sigma ->
M.loc -> Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val s_exp :
(CodeSemantics.Make.sigma -> Cil_types.exp -> CodeSemantics.Make.value)
Pervasives.ref
val s_cond :
(CodeSemantics.Make.sigma -> Cil_types.exp -> Lang.F.pred)
Pervasives.ref
val val_of_exp : CodeSemantics.Make.sigma -> Cil_types.exp -> Lang.F.term
val loc_of_exp : CodeSemantics.Make.sigma -> Cil_types.exp -> M.loc
val loc_of_lhost : CodeSemantics.Make.sigma -> Cil_types.lhost -> M.loc
val loc_of_offset :
CodeSemantics.Make.sigma ->
M.loc -> Cil_types.typ -> Cil_types.offset -> M.loc
val lval :
CodeSemantics.Make.sigma -> Cil_types.lhost * Cil_types.offset -> M.loc
val exp_unop :
CodeSemantics.Make.sigma ->
Cil_types.typ -> Cil_types.unop -> Cil_types.exp -> 'a Memory.value
val arith :
CodeSemantics.Make.sigma ->
Cil_types.typ ->
(Ctypes.c_int -> Lang.F.term -> Lang.F.term -> Lang.F.term) ->
(Ctypes.c_float -> Lang.F.term -> Lang.F.term -> Lang.F.term) ->
Cil_types.exp -> Cil_types.exp -> 'a Memory.value
val arith_int :
CodeSemantics.Make.sigma ->
Cil_types.typ ->
(Ctypes.c_int -> Lang.F.term -> Lang.F.term -> Lang.F.term) ->
Cil_types.exp -> Cil_types.exp -> 'a Memory.value
val bool_of_comp :
CodeSemantics.Make.sigma ->
(Lang.F.term -> Lang.F.term -> Lang.F.term) ->
(M.loc -> M.loc -> Lang.F.pred) ->
Cil_types.exp -> Cil_types.exp -> Lang.F.term
val bool_of_exp :
CodeSemantics.Make.sigma -> Cil_types.exp -> Lang.F.term
val exp_binop :
CodeSemantics.Make.sigma ->
Cil_types.typ ->
Cil_types.binop -> Cil_types.exp -> Cil_types.exp -> M.loc Memory.value
val cast :
Cil_types.typ ->
Cil_types.typ -> M.loc Memory.value -> M.loc Memory.value
val exp_node :
CodeSemantics.Make.sigma -> Cil_types.exp -> CodeSemantics.Make.value
val call_node : CodeSemantics.Make.sigma -> Cil_types.exp -> M.loc
val exp_handler : Cil_types.exp -> 'a Memory.value
val exp_protected :
CodeSemantics.Make.sigma -> Cil_types.exp -> CodeSemantics.Make.value
val equal_typ :
Cil_types.typ ->
M.loc Memory.value -> M.loc Memory.value -> Lang.F.pred
val equal_obj :
Ctypes.c_object ->
M.loc Memory.value -> M.loc Memory.value -> Lang.F.pred
val compare :
CodeSemantics.Make.sigma ->
(Lang.F.term -> Lang.F.term -> 'a) ->
(M.loc -> M.loc -> 'a) -> Cil_types.exp -> Cil_types.exp -> 'a
val cond_node : CodeSemantics.Make.sigma -> Cil_types.exp -> 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 call : CodeSemantics.Make.sigma -> Cil_types.exp -> M.loc
val return :
CodeSemantics.Make.sigma ->
Cil_types.typ -> Cil_types.exp -> Lang.F.term
val instance_of : M.loc -> Kernel_function.t -> Lang.F.pred
end