@@ -737,14 +737,15 @@ private predicate mk_FieldCons(
737
737
exists ( Expr e |
738
738
e = cal .getFieldExpr ( f ) .getFullyConverted ( ) and
739
739
f .getInitializationOrder ( ) = i and
740
- hc = hashCons ( e ) and
741
740
(
742
741
exists ( HashCons head , Field f2 , HC_Fields tail |
742
+ hc = hashCons ( e ) and
743
743
hcf = HC_FieldCons ( c , i - 1 , f2 , head , tail ) and
744
744
f2 .getInitializationOrder ( ) = i - 1 and
745
745
mk_FieldCons ( c , i - 1 , f2 , head , tail , cal )
746
746
)
747
747
or
748
+ hc = hashCons ( e ) and
748
749
i = 0 and
749
750
hcf = HC_EmptyFields ( c )
750
751
)
@@ -765,11 +766,13 @@ private predicate mk_ClassAggregateLiteral(Class c, HC_Fields hcf, ClassAggregat
765
766
analyzableClassAggregateLiteral ( cal ) and
766
767
c = cal .getUnspecifiedType ( ) and
767
768
(
768
- exists ( HC_Fields tail , Expr e , Field f |
769
+ exists ( HC_Fields tail , Expr e , Field f , int numChildren , HashCons eCons |
769
770
f .getInitializationOrder ( ) = cal .getNumChild ( ) - 1 and
770
771
e = cal .getFieldExpr ( f ) .getFullyConverted ( ) and
771
- hcf = HC_FieldCons ( c , cal .getNumChild ( ) - 1 , f , hashCons ( e ) , tail ) and
772
- mk_FieldCons ( c , cal .getNumChild ( ) - 1 , f , hashCons ( e ) , tail , cal )
772
+ eCons = hashCons ( e ) and
773
+ numChildren = cal .getNumChild ( ) and
774
+ hcf = HC_FieldCons ( c , numChildren - 1 , f , eCons , tail ) and
775
+ mk_FieldCons ( c , numChildren - 1 , f , eCons , tail , cal )
773
776
)
774
777
or
775
778
cal .getNumChild ( ) = 0 and
@@ -800,9 +803,10 @@ private predicate mk_ArrayCons(Type t, int i, HashCons hc, HC_Array hca, ArrayAg
800
803
private predicate mk_ArrayAggregateLiteral ( Type t , HC_Array hca , ArrayAggregateLiteral aal ) {
801
804
t = aal .getUnspecifiedType ( ) and
802
805
(
803
- exists ( HashCons head , HC_Array tail |
804
- hca = HC_ArrayCons ( t , aal .getNumChild ( ) - 1 , head , tail ) and
805
- mk_ArrayCons ( t , aal .getNumChild ( ) - 1 , head , tail , aal )
806
+ exists ( HashCons head , HC_Array tail , int numElements |
807
+ numElements = aal .getNumChild ( ) and
808
+ hca = HC_ArrayCons ( t , numElements - 1 , head , tail ) and
809
+ mk_ArrayCons ( t , numElements - 1 , head , tail , aal )
806
810
)
807
811
or
808
812
aal .getNumChild ( ) = 0 and
0 commit comments