@@ -94,18 +94,21 @@ predicate constantUpperBounded(PointerArithmeticInstruction pai, int delta) {
9494}
9595
9696bindingset [ pai, size]
97- predicate pointerArithOverflow0Impl ( PointerArithmeticInstruction pai , int size , int bound , int delta ) {
98- constantUpperBounded ( pai , bound ) and
99- delta = bound - size and
100- delta >= 0 and
101- size != 0 and
102- size != 1
97+ predicate pointerArithOverflow0Impl ( PointerArithmeticInstruction pai , int size , int delta ) {
98+ exists ( int bound |
99+ constantUpperBounded ( pai , bound ) and
100+ delta = bound - size and
101+ delta >= 0 and
102+ size != 0 and
103+ size != 1
104+ )
103105}
104106
107+ pragma [ nomagic]
105108predicate pointerArithOverflow0 ( PointerArithmeticInstruction pai , int delta ) {
106- exists ( int size , int bound |
109+ exists ( int size |
107110 arrayTypeHasSizes ( _, pai .getElementSize ( ) , size ) and
108- pointerArithOverflow0Impl ( pai , size , bound , delta )
111+ pointerArithOverflow0Impl ( pai , size , delta )
109112 )
110113}
111114
@@ -130,7 +133,7 @@ bindingset[v]
130133predicate finalPointerArithOverflow ( Variable v , PointerArithmeticInstruction pai , int delta ) {
131134 exists ( int size |
132135 arrayTypeHasSizes ( pragma [ only_bind_out ] ( v .getUnspecifiedType ( ) ) , pai .getElementSize ( ) , size ) and
133- pointerArithOverflow0Impl ( pai , size , _ , delta )
136+ pointerArithOverflow0Impl ( pai , size , delta )
134137 )
135138}
136139
0 commit comments