@@ -94,18 +94,21 @@ predicate constantUpperBounded(PointerArithmeticInstruction pai, int delta) {
94
94
}
95
95
96
96
bindingset [ 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
+ )
103
105
}
104
106
107
+ pragma [ nomagic]
105
108
predicate pointerArithOverflow0 ( PointerArithmeticInstruction pai , int delta ) {
106
- exists ( int size , int bound |
109
+ exists ( int size |
107
110
arrayTypeHasSizes ( _, pai .getElementSize ( ) , size ) and
108
- pointerArithOverflow0Impl ( pai , size , bound , delta )
111
+ pointerArithOverflow0Impl ( pai , size , delta )
109
112
)
110
113
}
111
114
@@ -130,7 +133,7 @@ bindingset[v]
130
133
predicate finalPointerArithOverflow ( Variable v , PointerArithmeticInstruction pai , int delta ) {
131
134
exists ( int size |
132
135
arrayTypeHasSizes ( pragma [ only_bind_out ] ( v .getUnspecifiedType ( ) ) , pai .getElementSize ( ) , size ) and
133
- pointerArithOverflow0Impl ( pai , size , _ , delta )
136
+ pointerArithOverflow0Impl ( pai , size , delta )
134
137
)
135
138
}
136
139
0 commit comments