@@ -197,7 +197,7 @@ private newtype HC_Fields =
197
197
private newtype HC_Array =
198
198
HC_EmptyArray ( Type t ) {
199
199
exists ( ArrayAggregateLiteral aal |
200
- aal .getType ( ) = t
200
+ aal .getType ( ) . getUnspecifiedType ( ) = t
201
201
)
202
202
}
203
203
or
@@ -602,28 +602,21 @@ private predicate mk_HasInit(HashCons hc, NewOrNewArrayExpr new) {
602
602
}
603
603
604
604
private predicate mk_HasAlign ( HashCons hc , NewOrNewArrayExpr new ) {
605
- hc = hashCons ( new .getAlignmentArgument ( ) )
605
+ hc = hashCons ( new .getAlignmentArgument ( ) . getFullyConverted ( ) )
606
606
}
607
607
608
608
private predicate analyzableNewExpr ( NewExpr new ) {
609
609
strictcount ( new .getAllocatedType ( ) ) = 1 and
610
- (
611
- not exists ( new .getAllocatorCall ( ) )
612
- or
613
- strictcount ( new .getAllocatorCall ( ) ) = 1
614
- ) and (
615
- not exists ( new .getInitializer ( ) )
616
- or
617
- strictcount ( new .getInitializer ( ) ) = 1
618
- )
610
+ count ( new .getAllocatorCall ( ) .getFullyConverted ( ) ) <= 1 and
611
+ count ( new .getInitializer ( ) .getFullyConverted ( ) ) <= 1
619
612
}
620
613
621
614
private predicate mk_NewExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align , boolean aligned ,
622
615
NewExpr new ) {
623
616
analyzableNewExpr ( new ) and
624
617
t = new .getAllocatedType ( ) and
625
618
(
626
- align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) ) ) and
619
+ align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) . getFullyConverted ( ) ) ) and
627
620
aligned = true
628
621
or
629
622
not new .hasAlignedAllocation ( ) and
@@ -664,24 +657,16 @@ private predicate mk_NewExpr(Type t, HC_Alloc alloc, HC_Init init, HC_Align alig
664
657
665
658
private predicate analyzableNewArrayExpr ( NewArrayExpr new ) {
666
659
strictcount ( new .getAllocatedType ( ) .getUnspecifiedType ( ) ) = 1 and
667
- strictcount ( new .getAllocatedType ( ) .getUnspecifiedType ( ) ) = 1 and
668
- (
669
- not exists ( new .getAllocatorCall ( ) )
670
- or
671
- strictcount ( new .getAllocatorCall ( ) .getFullyConverted ( ) ) = 1
672
- ) and (
673
- not exists ( new .getInitializer ( ) )
674
- or
675
- strictcount ( new .getInitializer ( ) .getFullyConverted ( ) ) = 1
676
- )
660
+ count ( new .getAllocatorCall ( ) .getFullyConverted ( ) ) <= 1 and
661
+ count ( new .getInitializer ( ) .getFullyConverted ( ) ) <= 1
677
662
}
678
663
679
664
private predicate mk_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align ,
680
665
boolean aligned , NewArrayExpr new ) {
681
666
analyzableNewArrayExpr ( new ) and
682
667
t = new .getAllocatedType ( ) and
683
668
(
684
- align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) ) ) and
669
+ align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) . getFullyConverted ( ) ) ) and
685
670
aligned = true
686
671
or
687
672
not new .hasAlignedAllocation ( ) and
0 commit comments