Module type Sigs.CodeSemantics

module type CodeSemantics = sig .. end
Compiler for C expressions

module M: Sigs.Model 
The underlying memory model
type loc = M.loc 
type value = loc Sigs.value 
type result = loc Sigs.result 
type sigma = M.Sigma.t 
val pp_value : Format.formatter -> value -> unit
val cval : value -> Lang.F.term
Evaluate an abstract value. May fail because of M.pointer_val.
val cloc : value -> loc
Interpret a value as a location. May fail because of M.pointer_loc.
val cast : Cil_types.typ ->
Cil_types.typ -> value -> value
Applies a pointer cast or a conversion.

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
Computes the value of (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
Computes the value of (a==b) provided both a and b are values with the given type.
val equal_obj : Ctypes.c_object ->
value -> value -> Lang.F.pred
Same as equal_typ with an object type.
val not_equal_obj : Ctypes.c_object ->
value -> value -> Lang.F.pred
Same as not_equal_typ with an object type.
val exp : sigma -> Cil_types.exp -> value
Evaluate the expression on the given memory state.
val cond : sigma -> Cil_types.exp -> Lang.F.pred
Evaluate the conditional expression on the given memory state.
val lval : sigma -> Cil_types.lval -> loc
Evaluate the left-value on the given memory state.
val call : sigma -> Cil_types.exp -> loc
Address of a function pointer. Handles AddrOf, StartOf and Lval as usual.
val instance_of : loc -> Cil_types.kernel_function -> Lang.F.pred
Check whether a function pointer is (an instance of) some kernel function. Currently, the meaning of "being an instance of" is simply equality.
val loc_of_exp : sigma -> Cil_types.exp -> loc
Compile an expression as a location. May (also) fail because of M.pointer_val.
val val_of_exp : sigma -> Cil_types.exp -> Lang.F.term
Compile an expression as a term. May (also) fail because of M.pointer_loc.
val result : sigma ->
Cil_types.typ -> result -> Lang.F.term
Value of an abstract result container.
val return : sigma -> Cil_types.typ -> Cil_types.exp -> Lang.F.term
Return an expression with a given type. Short cut for compiling the expression, cast into the desired type, and finally converted to a term.
val is_zero : sigma ->
Ctypes.c_object -> loc -> Lang.F.pred
Express that the object (of specified type) at the given location is filled with zeroes.
val is_exp_range : sigma ->
loc ->
Ctypes.c_object ->
Lang.F.term -> Lang.F.term -> value option -> Lang.F.pred
Express that all objects in a range of locations have a given value.

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
Express that a given variable has the same value in two memory states.
type warned_hyp = Warning.Set.t * Lang.F.pred 
val init : sigma:M.sigma ->
Cil_types.varinfo ->
Cil_types.init option -> warned_hyp list
Express that some variable has some initial value at the given memory state.

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.