From e3802325a56b2f0c62484dfbca5ba13ca9f3b861 Mon Sep 17 00:00:00 2001 From: Daniel Schwartz-Narbonne Date: Wed, 2 Feb 2022 12:13:56 -0500 Subject: [PATCH] PR Comments --- src/kani-compiler/cbmc/src/goto_program/expr.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kani-compiler/cbmc/src/goto_program/expr.rs b/src/kani-compiler/cbmc/src/goto_program/expr.rs index 95e485def95d..0df742918c15 100644 --- a/src/kani-compiler/cbmc/src/goto_program/expr.rs +++ b/src/kani-compiler/cbmc/src/goto_program/expr.rs @@ -855,7 +855,7 @@ impl Expr { // While one can technically use these on pointers, the result is treated as an integer. // This is almost never what you actually want. OverflowMinus | OverflowMult | OverflowPlus => { - lhs.typ.is_integer() && rhs.typ.is_integer() + lhs.typ == rhs.typ && lhs.typ.is_integer() } } } @@ -1206,7 +1206,7 @@ impl Expr { // FIXME: https://github.com/model-checking/kani/issues/786 // Overflow checking on pointers is hard to do at the IREP level. // Instead, we rely on `--pointer-overflow-check` in CBMC. - let overflowed = if self.typ.is_pointer() { + let overflowed = if self.typ.is_pointer() || e.typ.is_pointer() { warn!( "Overflow operations are not properly supported on pointer types {:?} {:?}", self, e