@@ -32,18 +32,39 @@ predicate hasReferenceInitializer(EnumConstant c) {
3232 )
3333}
3434
35+ /**
36+ * Gets the `rnk`'th (1-based) enumeration constant in `e` that does not have a
37+ * reference initializer (i.e., an initializer that refers to an enumeration
38+ * constant from the same enumeration).
39+ */
40+ EnumConstant getNonReferenceInitializedEnumConstantByRank ( Enum e , int rnk ) {
41+ result =
42+ rank [ rnk ] ( EnumConstant cand , int pos |
43+ e .getEnumConstant ( pos ) = cand and not hasReferenceInitializer ( cand )
44+ |
45+ cand order by pos
46+ )
47+ }
48+
49+ /**
50+ * Holds if `ec` is not the last enumeration constant in `e` that has a non-
51+ * reference initializer.
52+ */
53+ predicate hasNextWithoutReferenceInitializer ( Enum e , EnumConstant ec ) {
54+ exists ( int rnk |
55+ ec = getNonReferenceInitializedEnumConstantByRank ( e , rnk ) and
56+ exists ( getNonReferenceInitializedEnumConstantByRank ( e , rnk + 1 ) )
57+ )
58+ }
59+
3560// There exists another constant whose value is implicit, but it's
3661// not the last one: the last value is okay to use to get the highest
3762// enum value automatically. It can be followed by aliases though.
3863predicate enumThatHasConstantWithImplicitValue ( Enum e ) {
39- exists ( EnumConstant ec , int pos |
40- ec = e .getEnumConstant ( pos ) and
64+ exists ( EnumConstant ec |
65+ ec = e .getAnEnumConstant ( ) and
4166 not hasInitializer ( ec ) and
42- exists ( EnumConstant ec2 , int pos2 |
43- ec2 = e .getEnumConstant ( pos2 ) and
44- pos2 > pos and
45- not hasReferenceInitializer ( ec2 )
46- )
67+ hasNextWithoutReferenceInitializer ( e , ec )
4768 )
4869}
4970
0 commit comments