@@ -748,14 +748,13 @@ private predicate mk_FieldCons(Class c, int i, Field f, HashCons hc, HC_Fields h
748
748
cal .getType ( ) .getUnspecifiedType ( ) = c and
749
749
exists ( Expr e |
750
750
e = cal .getFieldExpr ( f ) .getFullyConverted ( ) and
751
- e = cal . getChild ( i ) . getFullyConverted ( ) and
751
+ f . getInitializationOrder ( ) = i and
752
752
hc = hashCons ( e ) and
753
753
(
754
754
exists ( HashCons head , Field f2 , HC_Fields tail |
755
755
hcf = HC_FieldCons ( c , i - 1 , f2 , head , tail ) and
756
- cal . getChild ( i - 1 ) . getFullyConverted ( ) = cal . getFieldExpr ( f2 ) . getFullyConverted ( ) and
756
+ f2 . getInitializationOrder ( ) = i - 1 and
757
757
mk_FieldCons ( c , i - 1 , f2 , head , tail , cal )
758
-
759
758
)
760
759
or
761
760
i = 0 and
@@ -777,7 +776,7 @@ private predicate mk_ClassAggregateLiteral(Class c, HC_Fields hcf, ClassAggregat
777
776
c = cal .getType ( ) .getUnspecifiedType ( ) and
778
777
(
779
778
exists ( HC_Fields tail , Expr e , Field f |
780
- e = cal .getChild ( cal . getNumChild ( ) - 1 ) . getFullyConverted ( ) and
779
+ f . getInitializationOrder ( ) = cal .getNumChild ( ) - 1 and
781
780
e = cal .getFieldExpr ( f ) .getFullyConverted ( ) and
782
781
hcf = HC_FieldCons ( c , cal .getNumChild ( ) - 1 , f , hashCons ( e ) , tail ) and
783
782
mk_FieldCons ( c , cal .getNumChild ( ) - 1 , f , hashCons ( e ) , tail , cal )
0 commit comments