module C:Sigs.CodeSemantics
with module M = M
module M:Sigs.Model
typeloc =
M.loc
typevalue =
loc Sigs.value
typeresult =
loc Sigs.result
typesigma =
M.Sigma.t
val pp_value : Format.formatter -> value -> unit
val cval : value -> Lang.F.term
M.pointer_val
.val cloc : value -> loc
M.pointer_loc
.val cast : Cil_types.typ ->
Cil_types.typ -> value -> value
cast tr te ve
transforms a value ve
with type te
into a value
with type tr
.
val equal_typ : Cil_types.typ ->
value -> value -> Lang.F.pred
(a==b)
provided both a
and b
are values
with the given type.val not_equal_typ : Cil_types.typ ->
value -> value -> Lang.F.pred
(a==b)
provided both a
and b
are values
with the given type.val equal_obj : Ctypes.c_object ->
value -> value -> Lang.F.pred
equal_typ
with an object type.val not_equal_obj : Ctypes.c_object ->
value -> value -> Lang.F.pred
not_equal_typ
with an object type.val exp : sigma -> Cil_types.exp -> value
val cond : sigma -> Cil_types.exp -> Lang.F.pred
val lval : sigma -> Cil_types.lval -> loc
val call : sigma -> Cil_types.exp -> loc
AddrOf
, StartOf
and Lval
as usual.val instance_of : loc -> Cil_types.kernel_function -> Lang.F.pred
val loc_of_exp : sigma -> Cil_types.exp -> loc
M.pointer_val
.val val_of_exp : sigma -> Cil_types.exp -> Lang.F.term
M.pointer_loc
.val result : sigma ->
Cil_types.typ -> result -> Lang.F.term
val return : sigma -> Cil_types.typ -> Cil_types.exp -> Lang.F.term
val is_zero : sigma ->
Ctypes.c_object -> loc -> Lang.F.pred
val is_exp_range : sigma ->
loc ->
Ctypes.c_object ->
Lang.F.term -> Lang.F.term -> value option -> Lang.F.pred
More precisely, is_exp_range sigma loc ty a b v
express that
value at ( ty* )loc + k
equals v
, forall a <= k < b
.
Value v=None
stands for zero.
val unchanged : M.sigma -> M.sigma -> Cil_types.varinfo -> Lang.F.pred
typewarned_hyp =
Warning.Set.t * Lang.F.pred
val init : sigma:M.sigma ->
Cil_types.varinfo ->
Cil_types.init option -> warned_hyp list
Remark: None
initializer are interpreted as zeroes. This is consistent
with the init option
associated with global variables in CIL,
for which the default initializer are zeroes. There is no
init option
value associated with local initializers.