@@ -213,7 +213,27 @@ 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+ predicate isDesignatorInit ( Field field , int position ) {
235+ field = classType .getAField ( ) and
236+ aggregate_field_init ( underlyingElement ( this ) , _, unresolveElement ( field ) , position , true )
217237 }
218238
219239 /**
@@ -304,7 +324,24 @@ class ArrayOrVectorAggregateLiteral extends AggregateLiteral {
304324 * - `a.getElementExpr(0, 2)` gives `789`.
305325 */
306326 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 )
308345 }
309346
310347 /**
0 commit comments