@@ -213,7 +213,27 @@ class ClassAggregateLiteral extends AggregateLiteral {
213
213
Expr getFieldExpr ( Field field , int position ) {
214
214
field = classType .getAField ( ) and
215
215
aggregate_field_init ( underlyingElement ( this ) , unresolveElement ( result ) , unresolveElement ( field ) ,
216
- position )
216
+ position , _)
217
+ }
218
+
219
+ /**
220
+ * Holds if the `position`-th initialization of `field` in this aggregate initializer
221
+ * uses a designator (e.g., `.x =`, `[42] =`) rather than a positional initializer.
222
+ *
223
+ * This can be used to distinguish explicitly designated initializations from
224
+ * implicit positional ones.
225
+ *
226
+ * For example, in the initializer:
227
+ * ```c
228
+ * struct S { int x, y; };
229
+ * struct S s = { .x = 1, 2 };
230
+ * ```
231
+ * - `.x = 1` is a designator init, therefore `isDesignatorInit(x, 0)` holds.
232
+ * - `2` is a positional init for `.y`, therefore `isDesignatorInit(y, 1)` does **not** hold.
233
+ */
234
+ predicate isDesignatorInit ( Field field , int position ) {
235
+ field = classType .getAField ( ) and
236
+ aggregate_field_init ( underlyingElement ( this ) , _, unresolveElement ( field ) , position , true )
217
237
}
218
238
219
239
/**
@@ -304,7 +324,24 @@ class ArrayOrVectorAggregateLiteral extends AggregateLiteral {
304
324
* - `a.getElementExpr(0, 2)` gives `789`.
305
325
*/
306
326
Expr getElementExpr ( int elementIndex , int position ) {
307
- aggregate_array_init ( underlyingElement ( this ) , unresolveElement ( result ) , elementIndex , position )
327
+ aggregate_array_init ( underlyingElement ( this ) , unresolveElement ( result ) , elementIndex , position ,
328
+ _)
329
+ }
330
+
331
+ /**
332
+ * Holds if the `position`-th initialization of the array element at `elementIndex`
333
+ * in this aggregate initializer uses a designator (e.g., `[0] = ...`) rather than
334
+ * an implicit positional initializer.
335
+ *
336
+ * For example, in:
337
+ * ```c
338
+ * int x[] = { [0] = 1, 2 };
339
+ * ```
340
+ * - `[0] = 1` is a designator init, therefore `isDesignatorInit(0, 0)` holds.
341
+ * - `2` is a positional init for `x[1]`, therefore `isDesignatorInit(1, 1)` does **not** hold.
342
+ */
343
+ predicate isDesignatorInit ( int elementIndex , int position ) {
344
+ aggregate_array_init ( underlyingElement ( this ) , _, elementIndex , position , true )
308
345
}
309
346
310
347
/**
0 commit comments