@@ -729,6 +729,18 @@ private predicate mk_AlignofExpr(HashCons child, AlignofExprOperator e) {
729
729
child = hashCons ( e .getAChild ( ) )
730
730
}
731
731
732
+ /**
733
+ * Gets the hash cons of field initializer expressions [0..i), where i > 0, for
734
+ * the class aggregate literal `cal` of type `c`, where `head` is the hash cons
735
+ * of the i'th initializer expression.
736
+ */
737
+ HC_Fields aggInitExprsUpTo ( ClassAggregateLiteral cal , Class c , int i ) {
738
+ exists ( Field f , HashCons head , HC_Fields tail |
739
+ result = HC_FieldCons ( c , i - 1 , f , head , tail ) and
740
+ mk_FieldCons ( c , i - 1 , f , head , tail , cal )
741
+ )
742
+ }
743
+
732
744
private predicate mk_FieldCons (
733
745
Class c , int i , Field f , HashCons hc , HC_Fields hcf , ClassAggregateLiteral cal
734
746
) {
@@ -738,12 +750,8 @@ private predicate mk_FieldCons(
738
750
e = cal .getFieldExpr ( f ) .getFullyConverted ( ) and
739
751
f .getInitializationOrder ( ) = i and
740
752
(
741
- exists ( HashCons head , Field f2 , HC_Fields tail |
742
- hc = hashCons ( e ) and
743
- hcf = HC_FieldCons ( c , i - 1 , f2 , head , tail ) and
744
- f2 .getInitializationOrder ( ) = i - 1 and
745
- mk_FieldCons ( c , i - 1 , f2 , head , tail , cal )
746
- )
753
+ hc = hashCons ( e ) and
754
+ hcf = aggInitExprsUpTo ( cal , c , i )
747
755
or
748
756
hc = hashCons ( e ) and
749
757
i = 0 and
@@ -766,14 +774,7 @@ private predicate mk_ClassAggregateLiteral(Class c, HC_Fields hcf, ClassAggregat
766
774
analyzableClassAggregateLiteral ( cal ) and
767
775
c = cal .getUnspecifiedType ( ) and
768
776
(
769
- exists ( HC_Fields tail , Expr e , Field f , int numChildren , HashCons eCons |
770
- f .getInitializationOrder ( ) = cal .getNumChild ( ) - 1 and
771
- e = cal .getFieldExpr ( f ) .getFullyConverted ( ) and
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 )
776
- )
777
+ hcf = aggInitExprsUpTo ( cal , c , cal .getNumChild ( ) )
777
778
or
778
779
cal .getNumChild ( ) = 0 and
779
780
hcf = HC_EmptyFields ( c )
@@ -785,15 +786,23 @@ private predicate analyzableArrayAggregateLiteral(ArrayAggregateLiteral aal) {
785
786
strictcount ( aal .getUnspecifiedType ( ) ) = 1
786
787
}
787
788
789
+ /**
790
+ * Gets the hash cons of array elements in [0..i), where i > 0, for
791
+ * the array aggregate literal `aal` of type `t`.
792
+ */
793
+ private HC_Array arrayElemsUpTo ( ArrayAggregateLiteral aal , Type t , int i ) {
794
+ exists ( HC_Array tail , HashCons head |
795
+ result = HC_ArrayCons ( t , i - 1 , head , tail ) and
796
+ mk_ArrayCons ( t , i - 1 , head , tail , aal )
797
+ )
798
+ }
799
+
788
800
private predicate mk_ArrayCons ( Type t , int i , HashCons hc , HC_Array hca , ArrayAggregateLiteral aal ) {
789
801
analyzableArrayAggregateLiteral ( aal ) and
790
802
t = aal .getUnspecifiedType ( ) and
791
803
hc = hashCons ( aal .getChild ( i ) ) and
792
804
(
793
- exists ( HC_Array tail , HashCons head |
794
- hca = HC_ArrayCons ( t , i - 1 , head , tail ) and
795
- mk_ArrayCons ( t , i - 1 , head , tail , aal )
796
- )
805
+ hca = arrayElemsUpTo ( aal , t , i )
797
806
or
798
807
i = 0 and
799
808
hca = HC_EmptyArray ( t )
0 commit comments