diff --git a/regression/cbmc/pointer-overflow2/test.desc b/regression/cbmc/pointer-overflow2/test.desc index 0cd1d164728..090e350f3cd 100644 --- a/regression/cbmc/pointer-overflow2/test.desc +++ b/regression/cbmc/pointer-overflow2/test.desc @@ -1,11 +1,11 @@ -KNOWNBUG +CORE main.c --pointer-overflow-check ^EXIT=0$ ^SIGNAL=0$ -\[main.overflow.1\] line \d+ pointer arithmetic overflow on - in p - \(signed long int\)1: SUCCESS -\[main.overflow.2\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long int\)1: SUCCESS -\[main.overflow.3\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long int\)-1: SUCCESS -\[main.overflow.4\] line \d+ pointer arithmetic overflow on - in p - \(signed long int\)-1: SUCCESS +\[main.overflow.1\] line \d+ pointer arithmetic overflow on - in p - \(signed long (long )?int\)1: SUCCESS +\[main.overflow.2\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long (long )?int\)1: SUCCESS +\[main.overflow.3\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long (long )?int\)-1: SUCCESS +\[main.overflow.4\] line \d+ pointer arithmetic overflow on - in p - \(signed long (long )?int\)-1: SUCCESS -- ^warning: ignoring diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 007413e882d..594fab39fc6 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1157,8 +1157,13 @@ void goto_checkt::pointer_overflow_check( expr.operands().size() == 2, "pointer arithmetic expected to have exactly 2 operands"); + // check for address space overflow by checking for overflow on integers exprt overflow("overflow-" + expr.id_string(), bool_typet()); - overflow.operands() = expr.operands(); + for(const auto &op : expr.operands()) + { + overflow.add_to_operands( + typecast_exprt::conditional_cast(op, pointer_diff_type())); + } add_guarded_property( not_exprt(overflow),