@@ -205,10 +205,12 @@ predicate linearAccessImpl(Expr expr, VariableAccess v, float p, float q) {
205205 expr = unaryPlusExpr )
206206 or
207207 // (larger_type)(p*v+q) == p*v + q
208- exists ( Cast cast
208+ exists ( Cast cast , ArithmeticType sourceType , ArithmeticType targetType
209209 | linearAccess ( cast .getExpr ( ) , v , p , q ) and
210- typeLowerBound ( cast .getType ( ) ) <= typeLowerBound ( cast .getExpr ( ) .getType ( ) ) and
211- typeUpperBound ( cast .getType ( ) ) >= typeUpperBound ( cast .getExpr ( ) .getType ( ) ) and
210+ sourceType = cast .getExpr ( ) .getType ( ) .getUnspecifiedType ( ) and
211+ targetType = cast .getType ( ) .getUnspecifiedType ( ) and
212+ typeLowerBound ( targetType ) <= typeLowerBound ( sourceType ) and
213+ typeUpperBound ( targetType ) >= typeUpperBound ( sourceType ) and
212214 expr = cast )
213215 or
214216 // (p*v+q) == p*v + q
@@ -282,14 +284,14 @@ predicate cmpWithLinearBound(
282284}
283285
284286/**
285- * Holds if `lb` and `ub` are the lower and upper bounds of type `t`
286- * respectively .
287+ * Holds if `lb` and `ub` are the lower and upper bounds of the unspecified
288+ * type `t` .
287289 *
288290 * For example, if `t` is a signed 32-bit type then holds if `lb` is
289291 * `-2^31` and `ub` is `2^31 - 1`.
290292 */
291293private
292- predicate typeBounds ( Type t , float lb , float ub ) {
294+ predicate typeBounds ( ArithmeticType t , float lb , float ub ) {
293295 exists ( IntegralType integralType , float limit
294296 | integralType = t and limit = 2 .pow ( 8 * integralType .getSize ( ) )
295297 | if integralType instanceof BoolType
@@ -303,22 +305,22 @@ predicate typeBounds(Type t, float lb, float ub) {
303305}
304306
305307/**
306- * Gets the lower bound for type `t`.
308+ * Gets the lower bound for the unspecified type `t`.
307309 *
308310 * For example, if `t` is a signed 32-bit type then the result is
309311 * `-2^31`.
310312 */
311- float typeLowerBound ( Type t ) {
313+ float typeLowerBound ( ArithmeticType t ) {
312314 typeBounds ( t , result , _)
313315}
314316
315317/**
316- * Gets the upper bound for type `t`.
318+ * Gets the upper bound for the unspecified type `t`.
317319 *
318320 * For example, if `t` is a signed 32-bit type then the result is
319321 * `2^31 - 1`.
320322 */
321- float typeUpperBound ( Type t ) {
323+ float typeUpperBound ( ArithmeticType t ) {
322324 typeBounds ( t , _, result )
323325}
324326
0 commit comments