|
|
|
|
@@ -46,6 +46,26 @@ class FunctionInput extends TFunctionInput {
|
|
|
|
|
*/
|
|
|
|
|
deprecated final predicate isInParameter(ParameterIndex index) { this.isParameter(index) }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this is the input value pointed to by a pointer parameter to a function, or the input
|
|
|
|
|
* value referred to by a reference parameter to a function, where the parameter has index
|
|
|
|
|
* `index`.
|
|
|
|
|
*
|
|
|
|
|
* Example:
|
|
|
|
|
* ```
|
|
|
|
|
* void func(int n, char* p, float& r);
|
|
|
|
|
* ```
|
|
|
|
|
* - `isParameterDeref(1, 1)` holds for the `FunctionInput` that represents the value of `*p` (with
|
|
|
|
|
* type `char`) on entry to the function.
|
|
|
|
|
* - `isParameterDeref(2, 1)` holds for the `FunctionInput` that represents the value of `r` (with type
|
|
|
|
|
* `float`) on entry to the function.
|
|
|
|
|
* - There is no `FunctionInput` for which `isParameterDeref(0, _)` holds, because `n` is neither a
|
|
|
|
|
* pointer nor a reference.
|
|
|
|
|
*/
|
|
|
|
|
predicate isParameterDeref(ParameterIndex index, int ind) {
|
|
|
|
|
ind = 1 and this.isParameterDeref(index)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this is the input value pointed to by a pointer parameter to a function, or the input
|
|
|
|
|
* value referred to by a reference parameter to a function, where the parameter has index
|
|
|
|
|
@@ -62,7 +82,7 @@ class FunctionInput extends TFunctionInput {
|
|
|
|
|
* - There is no `FunctionInput` for which `isParameterDeref(0)` holds, because `n` is neither a
|
|
|
|
|
* pointer nor a reference.
|
|
|
|
|
*/
|
|
|
|
|
predicate isParameterDeref(ParameterIndex index) { none() }
|
|
|
|
|
predicate isParameterDeref(ParameterIndex index) { this.isParameterDeref(index, 1) }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this is the input value pointed to by a pointer parameter to a function, or the input
|
|
|
|
|
@@ -87,7 +107,22 @@ class FunctionInput extends TFunctionInput {
|
|
|
|
|
* - `isQualifierObject()` holds for the `FunctionInput` that represents the value of `*this`
|
|
|
|
|
* (with type `C const`) on entry to the function.
|
|
|
|
|
*/
|
|
|
|
|
predicate isQualifierObject() { none() }
|
|
|
|
|
predicate isQualifierObject(int ind) { ind = 1 and this.isQualifierObject() }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this is the input value pointed to by the `this` pointer of an instance member
|
|
|
|
|
* function.
|
|
|
|
|
*
|
|
|
|
|
* Example:
|
|
|
|
|
* ```
|
|
|
|
|
* struct C {
|
|
|
|
|
* void mfunc(int n, char* p, float& r) const;
|
|
|
|
|
* };
|
|
|
|
|
* ```
|
|
|
|
|
* - `isQualifierObject()` holds for the `FunctionInput` that represents the value of `*this`
|
|
|
|
|
* (with type `C const`) on entry to the function.
|
|
|
|
|
*/
|
|
|
|
|
predicate isQualifierObject() { this.isQualifierObject(1) }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this is the input value pointed to by the `this` pointer of an instance member
|
|
|
|
|
@@ -143,16 +178,49 @@ class FunctionInput extends TFunctionInput {
|
|
|
|
|
* rare, but they do occur when a function returns a reference to itself,
|
|
|
|
|
* part of itself, or one of its other inputs.
|
|
|
|
|
*/
|
|
|
|
|
predicate isReturnValueDeref() { none() }
|
|
|
|
|
predicate isReturnValueDeref() { this.isReturnValueDeref(1) }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this is the input value pointed to by the return value of a
|
|
|
|
|
* function, if the function returns a pointer, or the input value referred
|
|
|
|
|
* to by the return value of a function, if the function returns a reference.
|
|
|
|
|
*
|
|
|
|
|
* Example:
|
|
|
|
|
* ```
|
|
|
|
|
* char* getPointer();
|
|
|
|
|
* float& getReference();
|
|
|
|
|
* int getInt();
|
|
|
|
|
* ```
|
|
|
|
|
* - `isReturnValueDeref(1)` holds for the `FunctionInput` that represents the
|
|
|
|
|
* value of `*getPointer()` (with type `char`).
|
|
|
|
|
* - `isReturnValueDeref(1)` holds for the `FunctionInput` that represents the
|
|
|
|
|
* value of `getReference()` (with type `float`).
|
|
|
|
|
* - There is no `FunctionInput` of `getInt()` for which
|
|
|
|
|
* `isReturnValueDeref(_)` holds because the return type of `getInt()` is
|
|
|
|
|
* neither a pointer nor a reference.
|
|
|
|
|
*
|
|
|
|
|
* Note that data flows in through function return values are relatively
|
|
|
|
|
* rare, but they do occur when a function returns a reference to itself,
|
|
|
|
|
* part of itself, or one of its other inputs.
|
|
|
|
|
*/
|
|
|
|
|
predicate isReturnValueDeref(int ind) { ind = 1 and this.isReturnValueDeref() }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if `i >= 0` and `isParameterDeref(i)` holds for this value, or
|
|
|
|
|
* if `i = -1` and `isQualifierObject()` holds for this value.
|
|
|
|
|
*/
|
|
|
|
|
final predicate isParameterDerefOrQualifierObject(ParameterIndex i, int ind) {
|
|
|
|
|
i >= 0 and this.isParameterDeref(i, ind)
|
|
|
|
|
or
|
|
|
|
|
i = -1 and this.isQualifierObject(ind)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if `i >= 0` and `isParameterDeref(i)` holds for this value, or
|
|
|
|
|
* if `i = -1` and `isQualifierObject()` holds for this value.
|
|
|
|
|
*/
|
|
|
|
|
final predicate isParameterDerefOrQualifierObject(ParameterIndex i) {
|
|
|
|
|
i >= 0 and this.isParameterDeref(i)
|
|
|
|
|
or
|
|
|
|
|
i = -1 and this.isQualifierObject()
|
|
|
|
|
this.isParameterDerefOrQualifierObject(i, 1)
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
@@ -308,7 +376,9 @@ class FunctionOutput extends TFunctionOutput {
|
|
|
|
|
* - There is no `FunctionOutput` for which `isParameterDeref(0)` holds, because `n` is neither a
|
|
|
|
|
* pointer nor a reference.
|
|
|
|
|
*/
|
|
|
|
|
predicate isParameterDeref(ParameterIndex i) { none() }
|
|
|
|
|
predicate isParameterDeref(ParameterIndex i) { this.isParameterDeref(i, 1) }
|
|
|
|
|
|
|
|
|
|
predicate isParameterDeref(ParameterIndex i, int ind) { ind = 1 and this.isParameterDeref(i) }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this is the output value pointed to by a pointer parameter to a function, or the
|
|
|
|
|
@@ -333,7 +403,22 @@ class FunctionOutput extends TFunctionOutput {
|
|
|
|
|
* - `isQualifierObject()` holds for the `FunctionOutput` that represents the value of `*this`
|
|
|
|
|
* (with type `C`) on return from the function.
|
|
|
|
|
*/
|
|
|
|
|
predicate isQualifierObject() { none() }
|
|
|
|
|
predicate isQualifierObject() { this.isQualifierObject(1) }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this is the output value pointed to by the `this` pointer of an instance member
|
|
|
|
|
* function.
|
|
|
|
|
*
|
|
|
|
|
* Example:
|
|
|
|
|
* ```
|
|
|
|
|
* struct C {
|
|
|
|
|
* void mfunc(int n, char* p, float& r);
|
|
|
|
|
* };
|
|
|
|
|
* ```
|
|
|
|
|
* - `isQualifierObject()` holds for the `FunctionOutput` that represents the value of `*this`
|
|
|
|
|
* (with type `C`) on return from the function.
|
|
|
|
|
*/
|
|
|
|
|
predicate isQualifierObject(int ind) { ind = 1 and this.isQualifierObject() }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this is the output value pointed to by the `this` pointer of an instance member
|
|
|
|
|
@@ -385,7 +470,27 @@ class FunctionOutput extends TFunctionOutput {
|
|
|
|
|
* - There is no `FunctionOutput` of `getInt()` for which `isReturnValueDeref()` holds because the
|
|
|
|
|
* return type of `getInt()` is neither a pointer nor a reference.
|
|
|
|
|
*/
|
|
|
|
|
predicate isReturnValueDeref() { none() }
|
|
|
|
|
predicate isReturnValueDeref() { this.isReturnValueDeref(_) }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this is the output value pointed to by the return value of a function, if the function
|
|
|
|
|
* returns a pointer, or the output value referred to by the return value of a function, if the
|
|
|
|
|
* function returns a reference.
|
|
|
|
|
*
|
|
|
|
|
* Example:
|
|
|
|
|
* ```
|
|
|
|
|
* char* getPointer();
|
|
|
|
|
* float& getReference();
|
|
|
|
|
* int getInt();
|
|
|
|
|
* ```
|
|
|
|
|
* - `isReturnValueDeref(1)` holds for the `FunctionOutput` that represents the value of
|
|
|
|
|
* `*getPointer()` (with type `char`).
|
|
|
|
|
* - `isReturnValueDeref(1)` holds for the `FunctionOutput` that represents the value of
|
|
|
|
|
* `getReference()` (with type `float`).
|
|
|
|
|
* - There is no `FunctionOutput` of `getInt()` for which `isReturnValueDeref(_)` holds because the
|
|
|
|
|
* return type of `getInt()` is neither a pointer nor a reference.
|
|
|
|
|
*/
|
|
|
|
|
predicate isReturnValueDeref(int ind) { ind = 1 and this.isReturnValueDeref() }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this is the output value pointed to by the return value of a function, if the function
|
|
|
|
|
@@ -399,10 +504,18 @@ class FunctionOutput extends TFunctionOutput {
|
|
|
|
|
* Holds if `i >= 0` and `isParameterDeref(i)` holds for this is the value, or
|
|
|
|
|
* if `i = -1` and `isQualifierObject()` holds for this value.
|
|
|
|
|
*/
|
|
|
|
|
final predicate isParameterDerefOrQualifierObject(ParameterIndex i) {
|
|
|
|
|
i >= 0 and this.isParameterDeref(i)
|
|
|
|
|
final predicate isParameterDerefOrQualifierObject(ParameterIndex i, int ind) {
|
|
|
|
|
i >= 0 and this.isParameterDeref(i, ind)
|
|
|
|
|
or
|
|
|
|
|
i = -1 and this.isQualifierObject()
|
|
|
|
|
i = -1 and this.isQualifierObject(ind)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if `i >= 0` and `isParameterDeref(i)` holds for this is the value, or
|
|
|
|
|
* if `i = -1` and `isQualifierObject()` holds for this value.
|
|
|
|
|
*/
|
|
|
|
|
final predicate isParameterDerefOrQualifierObject(ParameterIndex i) {
|
|
|
|
|
this.isParameterDerefOrQualifierObject(i, 1)
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
@@ -431,6 +544,10 @@ class OutParameterDeref extends FunctionOutput, TOutParameterDeref {
|
|
|
|
|
ParameterIndex getIndex() { result = index }
|
|
|
|
|
|
|
|
|
|
override predicate isParameterDeref(ParameterIndex i) { i = index }
|
|
|
|
|
|
|
|
|
|
override predicate isParameterDeref(ParameterIndex i, int ind) {
|
|
|
|
|
this.isParameterDeref(i) and ind = 1
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
|