@@ -197,7 +197,7 @@ private newtype HC_Fields =
197197private newtype HC_Array =
198198 HC_EmptyArray ( Type t ) {
199199 exists ( ArrayAggregateLiteral aal |
200- aal .getType ( ) = t
200+ aal .getType ( ) . getUnspecifiedType ( ) = t
201201 )
202202 }
203203 or
@@ -602,28 +602,21 @@ private predicate mk_HasInit(HashCons hc, NewOrNewArrayExpr new) {
602602}
603603
604604private predicate mk_HasAlign ( HashCons hc , NewOrNewArrayExpr new ) {
605- hc = hashCons ( new .getAlignmentArgument ( ) )
605+ hc = hashCons ( new .getAlignmentArgument ( ) . getFullyConverted ( ) )
606606}
607607
608608private predicate analyzableNewExpr ( NewExpr new ) {
609609 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
619612}
620613
621614private predicate mk_NewExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align , boolean aligned ,
622615 NewExpr new ) {
623616 analyzableNewExpr ( new ) and
624617 t = new .getAllocatedType ( ) and
625618 (
626- align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) ) ) and
619+ align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) . getFullyConverted ( ) ) ) and
627620 aligned = true
628621 or
629622 not new .hasAlignedAllocation ( ) and
@@ -664,24 +657,16 @@ private predicate mk_NewExpr(Type t, HC_Alloc alloc, HC_Init init, HC_Align alig
664657
665658private predicate analyzableNewArrayExpr ( NewArrayExpr new ) {
666659 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
677662}
678663
679664private predicate mk_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align ,
680665 boolean aligned , NewArrayExpr new ) {
681666 analyzableNewArrayExpr ( new ) and
682667 t = new .getAllocatedType ( ) and
683668 (
684- align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) ) ) and
669+ align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) . getFullyConverted ( ) ) ) and
685670 aligned = true
686671 or
687672 not new .hasAlignedAllocation ( ) and
0 commit comments