@@ -47,9 +47,9 @@ class FunctionInput extends TFunctionInput {
47
47
deprecated final predicate isInParameter ( ParameterIndex index ) { this .isParameter ( index ) }
48
48
49
49
/**
50
- * Holds if this is the input value pointed to by a pointer parameter to a function, or the input
51
- * value referred to by a reference parameter to a function, where the parameter has index
52
- * `index`.
50
+ * Holds if this is the input value pointed to (through `ind` number of indirections) by a
51
+ * pointer parameter to a function, or the input value referred to by a reference parameter
52
+ * to a function, where the parameter has index `index`.
53
53
*
54
54
* Example:
55
55
* ```
@@ -206,8 +206,8 @@ class FunctionInput extends TFunctionInput {
206
206
predicate isReturnValueDeref ( int ind ) { ind = 1 and this .isReturnValueDeref ( ) }
207
207
208
208
/**
209
- * Holds if `i >= 0` and `isParameterDeref(i)` holds for this value, or
210
- * if `i = -1` and `isQualifierObject()` holds for this value.
209
+ * Holds if `i >= 0` and `isParameterDeref(i, ind )` holds for this value, or
210
+ * if `i = -1` and `isQualifierObject(ind )` holds for this value.
211
211
*/
212
212
final predicate isParameterDerefOrQualifierObject ( ParameterIndex i , int ind ) {
213
213
i >= 0 and this .isParameterDeref ( i , ind )
@@ -378,6 +378,22 @@ class FunctionOutput extends TFunctionOutput {
378
378
*/
379
379
predicate isParameterDeref ( ParameterIndex i ) { this .isParameterDeref ( i , 1 ) }
380
380
381
+ /**
382
+ * Holds if this is the output value pointed to by a pointer parameter (through `ind` number
383
+ * of indirections) to a function, or the output value referred to by a reference parameter to
384
+ * a function, where the parameter has index `index`.
385
+ *
386
+ * Example:
387
+ * ```
388
+ * void func(int n, char* p, float& r);
389
+ * ```
390
+ * - `isParameterDeref(1, 1)` holds for the `FunctionOutput` that represents the value of `*p` (with
391
+ * type `char`) on return from the function.
392
+ * - `isParameterDeref(2, 1)` holds for the `FunctionOutput` that represents the value of `r` (with
393
+ * type `float`) on return from the function.
394
+ * - There is no `FunctionOutput` for which `isParameterDeref(0, _)` holds, because `n` is neither a
395
+ * pointer nor a reference.
396
+ */
381
397
predicate isParameterDeref ( ParameterIndex i , int ind ) { ind = 1 and this .isParameterDeref ( i ) }
382
398
383
399
/**
@@ -501,8 +517,8 @@ class FunctionOutput extends TFunctionOutput {
501
517
deprecated final predicate isOutReturnPointer ( ) { this .isReturnValueDeref ( ) }
502
518
503
519
/**
504
- * Holds if `i >= 0` and `isParameterDeref(i)` holds for this is the value, or
505
- * if `i = -1` and `isQualifierObject()` holds for this value.
520
+ * Holds if `i >= 0` and `isParameterDeref(i, ind )` holds for this is the value, or
521
+ * if `i = -1` and `isQualifierObject(ind )` holds for this value.
506
522
*/
507
523
final predicate isParameterDerefOrQualifierObject ( ParameterIndex i , int ind ) {
508
524
i >= 0 and this .isParameterDeref ( i , ind )
0 commit comments