@@ -62,33 +62,31 @@ int getMaxDepth(ArrayAggregateLiteral al) {
6262
6363// internal recursive predicate for `hasMultipleInitializerExprsForSameIndex`
6464predicate hasMultipleInitializerExprsForSameIndexInternal (
65- ArrayAggregateLiteral al1 , ArrayAggregateLiteral al2 , Expr out_al1_expr , Expr out_al2_expr
65+ ArrayAggregateLiteral root , Expr e1 , Expr e2
6666) {
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- )
67+ root = e1 and root = e2
68+ or
69+ exists ( ArrayAggregateLiteral parent1 , ArrayAggregateLiteral parent2 , int shared_index |
70+ hasMultipleInitializerExprsForSameIndexInternal ( root , parent1 , parent2 ) and
71+ shared_index = [ 0 .. parent1 .getArraySize ( ) - 1 ] and
72+ e1 = parent1 .getAnElementExpr ( shared_index ) and
73+ e2 = parent2 .getAnElementExpr ( shared_index )
8474 )
8575}
8676
8777/**
8878 * Holds if `expr1` and `expr2` both initialize the same array element of `root`.
8979 */
9080predicate hasMultipleInitializerExprsForSameIndex ( ArrayAggregateLiteral root , Expr expr1 , Expr expr2 ) {
91- hasMultipleInitializerExprsForSameIndexInternal ( root , root , expr1 , expr2 )
81+ hasMultipleInitializerExprsForSameIndexInternal ( root , expr1 , expr2 ) and
82+ not root = expr1 and
83+ not root = expr2 and
84+ not expr1 = expr2 and
85+ (
86+ not expr1 instanceof ArrayAggregateLiteral
87+ or
88+ not expr2 instanceof ArrayAggregateLiteral
89+ )
9290}
9391
9492/**
0 commit comments