@@ -60,35 +60,55 @@ int getMaxDepth(ArrayAggregateLiteral al) {
6060 else result = 1 + max ( Expr child | child = al .getAnElementExpr ( _) | getMaxDepth ( child ) )
6161}
6262
63- // internal recursive predicate for `hasMultipleInitializerExprsForSameIndex`
6463predicate hasMultipleInitializerExprsForSameIndexInternal (
65- ArrayAggregateLiteral al1 , ArrayAggregateLiteral al2 , Expr out_al1_expr , Expr out_al2_expr
64+ ArrayAggregateLiteral root , Expr e1 , Expr e2
6665) {
67- exists ( int shared_index , Expr al1_expr , Expr al2_expr |
68- // an `Expr` initializing an element of the same index in both `al1` and `al2`
69- shared_index = [ 0 .. al1 .getArraySize ( ) - 1 ] and
70- al1_expr = al1 .getAnElementExpr ( shared_index ) and
71- al2_expr = al2 .getAnElementExpr ( shared_index ) and
72- // but not the same `Expr`
73- not al1_expr = al2_expr and
74- (
75- // case A - the children are not aggregate literals
76- // holds if `al1` and `al2` both hold for .getElement[sharedIndex]
77- not al1_expr instanceof ArrayAggregateLiteral and
78- out_al1_expr = al1_expr and
79- out_al2_expr = al2_expr
80- or
81- // case B - `al1` and `al2` both have an aggregate literal child at the same index, so recurse
82- hasMultipleInitializerExprsForSameIndexInternal ( al1_expr , al2_expr , out_al1_expr , out_al2_expr )
83- )
66+ root = e1 and root = e2
67+ or
68+ exists ( ArrayAggregateLiteral parent1 , ArrayAggregateLiteral parent2 , int shared_index |
69+ hasMultipleInitializerExprsForSameIndexInternal ( root , parent1 , parent2 ) and
70+ shared_index = [ 0 .. parent1 .getArraySize ( ) - 1 ] and
71+ e1 = parent1 .getAnElementExpr ( shared_index ) and
72+ e2 = parent2 .getAnElementExpr ( shared_index )
8473 )
8574}
8675
76+ // // internal recursive predicate for `hasMultipleInitializerExprsForSameIndex`
77+ // predicate hasMultipleInitializerExprsForSameIndexInternal(
78+ // ArrayAggregateLiteral al1, ArrayAggregateLiteral al2, Expr out_al1_expr, Expr out_al2_expr
79+ // ) {
80+ // exists(int shared_index, Expr al1_expr, Expr al2_expr |
81+ // // an `Expr` initializing an element of the same index in both `al1` and `al2`
82+ // shared_index = [0 .. al1.getArraySize() - 1] and
83+ // al1_expr = al1.getAnElementExpr(shared_index) and
84+ // al2_expr = al2.getAnElementExpr(shared_index) and
85+ // // but not the same `Expr`
86+ // not al1_expr = al2_expr and
87+ // (
88+ // // case A - the children are not aggregate literals
89+ // // holds if `al1` and `al2` both hold for .getElement[sharedIndex]
90+ // not al1_expr instanceof ArrayAggregateLiteral and
91+ // out_al1_expr = al1_expr and
92+ // out_al2_expr = al2_expr
93+ // or
94+ // // case B - `al1` and `al2` both have an aggregate literal child at the same index, so recurse
95+ // hasMultipleInitializerExprsForSameIndexInternal(al1_expr, al2_expr, out_al1_expr, out_al2_expr)
96+ // )
97+ // )
98+ // }
8799/**
88100 * Holds if `expr1` and `expr2` both initialize the same array element of `root`.
89101 */
90102predicate hasMultipleInitializerExprsForSameIndex ( ArrayAggregateLiteral root , Expr expr1 , Expr expr2 ) {
91- hasMultipleInitializerExprsForSameIndexInternal ( root , root , expr1 , expr2 )
103+ hasMultipleInitializerExprsForSameIndexInternal ( root , expr1 , expr2 ) and
104+ not root = expr1 and
105+ not root = expr2 and
106+ not expr1 = expr2 and
107+ (
108+ not expr1 instanceof ArrayAggregateLiteral
109+ or
110+ not expr2 instanceof ArrayAggregateLiteral
111+ )
92112}
93113
94114/**
0 commit comments