@@ -46,6 +46,26 @@ class FunctionInput extends TFunctionInput {
4646 */
4747 deprecated final predicate isInParameter ( ParameterIndex index ) { this .isParameter ( index ) }
4848
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`.
53+ *
54+ * Example:
55+ * ```
56+ * void func(int n, char* p, float& r);
57+ * ```
58+ * - `isParameterDeref(1, 1)` holds for the `FunctionInput` that represents the value of `*p` (with
59+ * type `char`) on entry to the function.
60+ * - `isParameterDeref(2, 1)` holds for the `FunctionInput` that represents the value of `r` (with type
61+ * `float`) on entry to the function.
62+ * - There is no `FunctionInput` for which `isParameterDeref(0, _)` holds, because `n` is neither a
63+ * pointer nor a reference.
64+ */
65+ predicate isParameterDeref ( ParameterIndex index , int ind ) {
66+ ind = 1 and this .isParameterDeref ( index )
67+ }
68+
4969 /**
5070 * Holds if this is the input value pointed to by a pointer parameter to a function, or the input
5171 * value referred to by a reference parameter to a function, where the parameter has index
@@ -62,7 +82,7 @@ class FunctionInput extends TFunctionInput {
6282 * - There is no `FunctionInput` for which `isParameterDeref(0)` holds, because `n` is neither a
6383 * pointer nor a reference.
6484 */
65- predicate isParameterDeref ( ParameterIndex index ) { none ( ) }
85+ predicate isParameterDeref ( ParameterIndex index ) { this . isParameterDeref ( index , 1 ) }
6686
6787 /**
6888 * 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 {
87107 * - `isQualifierObject()` holds for the `FunctionInput` that represents the value of `*this`
88108 * (with type `C const`) on entry to the function.
89109 */
90- predicate isQualifierObject ( ) { none ( ) }
110+ predicate isQualifierObject ( int ind ) { ind = 1 and this .isQualifierObject ( ) }
111+
112+ /**
113+ * Holds if this is the input value pointed to by the `this` pointer of an instance member
114+ * function.
115+ *
116+ * Example:
117+ * ```
118+ * struct C {
119+ * void mfunc(int n, char* p, float& r) const;
120+ * };
121+ * ```
122+ * - `isQualifierObject()` holds for the `FunctionInput` that represents the value of `*this`
123+ * (with type `C const`) on entry to the function.
124+ */
125+ predicate isQualifierObject ( ) { this .isQualifierObject ( 1 ) }
91126
92127 /**
93128 * 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 {
143178 * rare, but they do occur when a function returns a reference to itself,
144179 * part of itself, or one of its other inputs.
145180 */
146- predicate isReturnValueDeref ( ) { none ( ) }
181+ predicate isReturnValueDeref ( ) { this .isReturnValueDeref ( 1 ) }
182+
183+ /**
184+ * Holds if this is the input value pointed to by the return value of a
185+ * function, if the function returns a pointer, or the input value referred
186+ * to by the return value of a function, if the function returns a reference.
187+ *
188+ * Example:
189+ * ```
190+ * char* getPointer();
191+ * float& getReference();
192+ * int getInt();
193+ * ```
194+ * - `isReturnValueDeref(1)` holds for the `FunctionInput` that represents the
195+ * value of `*getPointer()` (with type `char`).
196+ * - `isReturnValueDeref(1)` holds for the `FunctionInput` that represents the
197+ * value of `getReference()` (with type `float`).
198+ * - There is no `FunctionInput` of `getInt()` for which
199+ * `isReturnValueDeref(_)` holds because the return type of `getInt()` is
200+ * neither a pointer nor a reference.
201+ *
202+ * Note that data flows in through function return values are relatively
203+ * rare, but they do occur when a function returns a reference to itself,
204+ * part of itself, or one of its other inputs.
205+ */
206+ predicate isReturnValueDeref ( int ind ) { ind = 1 and this .isReturnValueDeref ( ) }
147207
148208 /**
149209 * Holds if `i >= 0` and `isParameterDeref(i)` holds for this value, or
150210 * if `i = -1` and `isQualifierObject()` holds for this value.
151211 */
152- final predicate isParameterDerefOrQualifierObject ( ParameterIndex i ) {
153- i >= 0 and this .isParameterDeref ( i )
212+ final predicate isParameterDerefOrQualifierObject ( ParameterIndex i , int ind ) {
213+ i >= 0 and this .isParameterDeref ( i , ind )
154214 or
155- i = - 1 and this .isQualifierObject ( )
215+ i = - 1 and this .isQualifierObject ( ind )
216+ }
217+
218+ /**
219+ * Holds if `i >= 0` and `isParameterDeref(i)` holds for this value, or
220+ * if `i = -1` and `isQualifierObject()` holds for this value.
221+ */
222+ final predicate isParameterDerefOrQualifierObject ( ParameterIndex i ) {
223+ this .isParameterDerefOrQualifierObject ( i , 1 )
156224 }
157225}
158226
@@ -308,7 +376,9 @@ class FunctionOutput extends TFunctionOutput {
308376 * - There is no `FunctionOutput` for which `isParameterDeref(0)` holds, because `n` is neither a
309377 * pointer nor a reference.
310378 */
311- predicate isParameterDeref ( ParameterIndex i ) { none ( ) }
379+ predicate isParameterDeref ( ParameterIndex i ) { this .isParameterDeref ( i , 1 ) }
380+
381+ predicate isParameterDeref ( ParameterIndex i , int ind ) { ind = 1 and this .isParameterDeref ( i ) }
312382
313383 /**
314384 * Holds if this is the output value pointed to by a pointer parameter to a function, or the
@@ -333,7 +403,9 @@ class FunctionOutput extends TFunctionOutput {
333403 * - `isQualifierObject()` holds for the `FunctionOutput` that represents the value of `*this`
334404 * (with type `C`) on return from the function.
335405 */
336- predicate isQualifierObject ( ) { none ( ) }
406+ predicate isQualifierObject ( ) { this .isQualifierObject ( 1 ) }
407+
408+ predicate isQualifierObject ( int ind ) { ind = 1 and this .isQualifierObject ( ) }
337409
338410 /**
339411 * Holds if this is the output value pointed to by the `this` pointer of an instance member
@@ -385,7 +457,9 @@ class FunctionOutput extends TFunctionOutput {
385457 * - There is no `FunctionOutput` of `getInt()` for which `isReturnValueDeref()` holds because the
386458 * return type of `getInt()` is neither a pointer nor a reference.
387459 */
388- predicate isReturnValueDeref ( ) { none ( ) }
460+ predicate isReturnValueDeref ( ) { this .isReturnValueDeref ( _) }
461+
462+ predicate isReturnValueDeref ( int ind ) { ind = 1 and this .isReturnValueDeref ( ) }
389463
390464 /**
391465 * Holds if this is the output value pointed to by the return value of a function, if the function
@@ -399,10 +473,14 @@ class FunctionOutput extends TFunctionOutput {
399473 * Holds if `i >= 0` and `isParameterDeref(i)` holds for this is the value, or
400474 * if `i = -1` and `isQualifierObject()` holds for this value.
401475 */
402- final predicate isParameterDerefOrQualifierObject ( ParameterIndex i ) {
403- i >= 0 and this .isParameterDeref ( i )
476+ final predicate isParameterDerefOrQualifierObject ( ParameterIndex i , int ind ) {
477+ i >= 0 and this .isParameterDeref ( i , ind )
404478 or
405- i = - 1 and this .isQualifierObject ( )
479+ i = - 1 and this .isQualifierObject ( ind )
480+ }
481+
482+ final predicate isParameterDerefOrQualifierObject ( ParameterIndex i ) {
483+ this .isParameterDerefOrQualifierObject ( i , 1 )
406484 }
407485}
408486
@@ -431,6 +509,10 @@ class OutParameterDeref extends FunctionOutput, TOutParameterDeref {
431509 ParameterIndex getIndex ( ) { result = index }
432510
433511 override predicate isParameterDeref ( ParameterIndex i ) { i = index }
512+
513+ override predicate isParameterDeref ( ParameterIndex i , int ind ) {
514+ this .isParameterDeref ( i ) and ind = 1
515+ }
434516}
435517
436518/**
0 commit comments