@@ -46,6 +46,26 @@ class FunctionInput extends TFunctionInput {
46
46
*/
47
47
deprecated final predicate isInParameter ( ParameterIndex index ) { this .isParameter ( index ) }
48
48
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
+
49
69
/**
50
70
* Holds if this is the input value pointed to by a pointer parameter to a function, or the input
51
71
* value referred to by a reference parameter to a function, where the parameter has index
@@ -62,7 +82,7 @@ class FunctionInput extends TFunctionInput {
62
82
* - There is no `FunctionInput` for which `isParameterDeref(0)` holds, because `n` is neither a
63
83
* pointer nor a reference.
64
84
*/
65
- predicate isParameterDeref ( ParameterIndex index ) { none ( ) }
85
+ predicate isParameterDeref ( ParameterIndex index ) { this . isParameterDeref ( index , 1 ) }
66
86
67
87
/**
68
88
* 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 {
87
107
* - `isQualifierObject()` holds for the `FunctionInput` that represents the value of `*this`
88
108
* (with type `C const`) on entry to the function.
89
109
*/
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 ) }
91
126
92
127
/**
93
128
* 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 {
143
178
* rare, but they do occur when a function returns a reference to itself,
144
179
* part of itself, or one of its other inputs.
145
180
*/
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 ( ) }
147
207
148
208
/**
149
209
* Holds if `i >= 0` and `isParameterDeref(i)` holds for this value, or
150
210
* if `i = -1` and `isQualifierObject()` holds for this value.
151
211
*/
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 )
154
214
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 )
156
224
}
157
225
}
158
226
@@ -308,7 +376,9 @@ class FunctionOutput extends TFunctionOutput {
308
376
* - There is no `FunctionOutput` for which `isParameterDeref(0)` holds, because `n` is neither a
309
377
* pointer nor a reference.
310
378
*/
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 ) }
312
382
313
383
/**
314
384
* 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 {
333
403
* - `isQualifierObject()` holds for the `FunctionOutput` that represents the value of `*this`
334
404
* (with type `C`) on return from the function.
335
405
*/
336
- predicate isQualifierObject ( ) { none ( ) }
406
+ predicate isQualifierObject ( ) { this .isQualifierObject ( 1 ) }
407
+
408
+ predicate isQualifierObject ( int ind ) { ind = 1 and this .isQualifierObject ( ) }
337
409
338
410
/**
339
411
* 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 {
385
457
* - There is no `FunctionOutput` of `getInt()` for which `isReturnValueDeref()` holds because the
386
458
* return type of `getInt()` is neither a pointer nor a reference.
387
459
*/
388
- predicate isReturnValueDeref ( ) { none ( ) }
460
+ predicate isReturnValueDeref ( ) { this .isReturnValueDeref ( _) }
461
+
462
+ predicate isReturnValueDeref ( int ind ) { ind = 1 and this .isReturnValueDeref ( ) }
389
463
390
464
/**
391
465
* 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 {
399
473
* Holds if `i >= 0` and `isParameterDeref(i)` holds for this is the value, or
400
474
* if `i = -1` and `isQualifierObject()` holds for this value.
401
475
*/
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 )
404
478
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 )
406
484
}
407
485
}
408
486
@@ -431,6 +509,10 @@ class OutParameterDeref extends FunctionOutput, TOutParameterDeref {
431
509
ParameterIndex getIndex ( ) { result = index }
432
510
433
511
override predicate isParameterDeref ( ParameterIndex i ) { i = index }
512
+
513
+ override predicate isParameterDeref ( ParameterIndex i , int ind ) {
514
+ this .isParameterDeref ( i ) and ind = 1
515
+ }
434
516
}
435
517
436
518
/**
0 commit comments