@@ -47,9 +47,9 @@ class FunctionInput extends TFunctionInput {
4747 deprecated final predicate isInParameter ( ParameterIndex index ) { this .isParameter ( index ) }
4848
4949 /**
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`.
5353 *
5454 * Example:
5555 * ```
@@ -206,8 +206,8 @@ class FunctionInput extends TFunctionInput {
206206 predicate isReturnValueDeref ( int ind ) { ind = 1 and this .isReturnValueDeref ( ) }
207207
208208 /**
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.
211211 */
212212 final predicate isParameterDerefOrQualifierObject ( ParameterIndex i , int ind ) {
213213 i >= 0 and this .isParameterDeref ( i , ind )
@@ -378,6 +378,22 @@ class FunctionOutput extends TFunctionOutput {
378378 */
379379 predicate isParameterDeref ( ParameterIndex i ) { this .isParameterDeref ( i , 1 ) }
380380
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+ */
381397 predicate isParameterDeref ( ParameterIndex i , int ind ) { ind = 1 and this .isParameterDeref ( i ) }
382398
383399 /**
@@ -501,8 +517,8 @@ class FunctionOutput extends TFunctionOutput {
501517 deprecated final predicate isOutReturnPointer ( ) { this .isReturnValueDeref ( ) }
502518
503519 /**
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.
506522 */
507523 final predicate isParameterDerefOrQualifierObject ( ParameterIndex i , int ind ) {
508524 i >= 0 and this .isParameterDeref ( i , ind )
0 commit comments