Taint.Rel
Relation between a value and an object that we track.
The framework tracks runtime values. Each value is a word, e.g., a byte, a bit, or a machine word, that can be somehow related to the actual object that we track.
There could be different kinds of relations, denoted with different values of this abstract type. So far, we distinguish between the direct
and indirect
relation.
Denotes the direct relation between a value and the object that we track, e.g., a value contains the runtime representation of the object or a part of it.
val direct : t
Denotes the direct relation between a value and the object that we track, e.g., a value contains the runtime representation of the object or a part of it.
val indirect : t
Denotes the indirect relation between a value and the object that we track, e.g., a value is a pointer that points to a value that has the direct relation with the object.
compare x y
returns a total ordering between two relations x
and y
. If x < y
then the result is less than 0
. If x = y
then the result is 0
. Otherwise, the result is greater than 0
.