@@ -213,7 +213,29 @@ class ClassAggregateLiteral extends AggregateLiteral {
213213 Expr getFieldExpr ( Field field , int position ) {
214214 field = classType .getAField ( ) and
215215 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+ * @param field The field being initialized.
235+ */
236+ predicate isDesignatorInit ( Field field , int position ) {
237+ field = classType .getAField ( ) and
238+ aggregate_field_init ( underlyingElement ( this ) , _, unresolveElement ( field ) , position , true )
217239 }
218240
219241 /**
@@ -304,7 +326,26 @@ class ArrayOrVectorAggregateLiteral extends AggregateLiteral {
304326 * - `a.getElementExpr(0, 2)` gives `789`.
305327 */
306328 Expr getElementExpr ( int elementIndex , int position ) {
307- aggregate_array_init ( underlyingElement ( this ) , unresolveElement ( result ) , elementIndex , position )
329+ aggregate_array_init ( underlyingElement ( this ) , unresolveElement ( result ) , elementIndex , position ,
330+ _)
331+ }
332+
333+ /**
334+ * Holds if the `position`-th initialization of the array element at `elementIndex`
335+ * in this aggregate initializer uses a designator (e.g., `[0] = ...`) rather than
336+ * an implicit positional initializer.
337+ *
338+ * For example, in:
339+ * ```c
340+ * int x[] = { [0] = 1, 2 };
341+ * ```
342+ * - `[0] = 1` is a designator init, therefore `isDesignatorInit(0, 0)` holds.
343+ * - `2` is a positional init for `x[1]`, therefore `isDesignatorInit(1, 1)` does **not** hold.
344+ *
345+ * @param elementIndex The index of the array element.
346+ */
347+ predicate isDesignatorInit ( int elementIndex , int position ) {
348+ aggregate_array_init ( underlyingElement ( this ) , _, elementIndex , position , true )
308349 }
309350
310351 /**
0 commit comments