From a20fb34156ab1993f462c7bfe59003b4868aa88b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 18 Apr 2018 11:20:16 +0100 Subject: [PATCH] Pointer arithmetic overflow is overflow on integer representation At a bare minimum, we should report an overflow when performing pointer arithmetic that would result in an overflow on the underlying integer representation. As future work, we may want to expand on those checks by reporting overflows when exceeding object bounds, as discussed in #5426. Fixes: #5284 --- regression/cbmc/pointer-overflow2/test.desc | 10 +++++----- src/analyses/goto_check.cpp | 7 ++++++- 2 files changed, 11 insertions(+), 6 deletions(-) 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),