Module CodeSemantics.MakeSource

Parameters

module M : Sigs.Model

Signature

Sourcemodule M = M

The underlying memory model

Sourcetype loc = M.loc
Sourcetype nonrec value = loc Sigs.value
Sourcetype nonrec result = loc Sigs.result
Sourcetype sigma = M.Sigma.t
Sourceval pp_value : Format.formatter -> value -> unit
Sourceval cval : value -> Lang.F.term

Evaluate an abstract value. May fail because of M.pointer_val.

Sourceval cloc : value -> loc

Interpret a value as a location. May fail because of M.pointer_loc.

Applies a pointer cast or a conversion.

cast tr te ve transforms a value ve with type te into a value with type tr.

Computes the value of (a==b) provided both a and b are values with the given type.

Computes the value of (a==b) provided both a and b are values with the given type.

Sourceval equal_obj : Ctypes.c_object -> value -> value -> Lang.F.pred

Same as equal_typ with an object type.

Sourceval not_equal_obj : Ctypes.c_object -> value -> value -> Lang.F.pred

Same as not_equal_typ with an object type.

Evaluate the expression on the given memory state.

Evaluate the conditional expression on the given memory state.

Evaluate the left-value on the given memory state.

Address of a function pointer. Handles AddrOf, StartOf and Lval as usual.

Check whether a function pointer is (an instance of) some kernel function. Currently, the meaning of "being an instance of" is simply equality.

Compile an expression as a location. May (also) fail because of M.pointer_val.

Compile an expression as a term. May (also) fail because of M.pointer_loc.

Value of an abstract result container.

Return an expression with a given type. Short cut for compiling the expression, cast into the desired type, and finally converted to a term.

Express that the object (of specified type) at the given location is filled with zeroes.

Sourceval 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.

Express that a given variable has the same value in two memory states.

Express that some variable has some initial value at the given memory state. The first predicate states the value, the second, the initialization status.

Note: we DO NOT merge values and initialization status hypotheses as the factorization performed by Qed can make predicates too hard to simplify later.

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. This function is called for global initializers and local initializers (Cil.Local_init). It is not called for local variables without initializers as they do not have a Cil.init option.