@@ -62,33 +62,31 @@ int getMaxDepth(ArrayAggregateLiteral al) {
62
62
63
63
// internal recursive predicate for `hasMultipleInitializerExprsForSameIndex`
64
64
predicate hasMultipleInitializerExprsForSameIndexInternal (
65
- ArrayAggregateLiteral al1 , ArrayAggregateLiteral al2 , Expr out_al1_expr , Expr out_al2_expr
65
+ ArrayAggregateLiteral root , Expr e1 , Expr e2
66
66
) {
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 )
84
74
)
85
75
}
86
76
87
77
/**
88
78
* Holds if `expr1` and `expr2` both initialize the same array element of `root`.
89
79
*/
90
80
predicate 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
+ )
92
90
}
93
91
94
92
/**
0 commit comments