diff --git a/regression/cbmc/Pointer_Arithmetic16/main.c b/regression/cbmc/Pointer_Arithmetic16/main.c new file mode 100644 index 00000000000..a642ce4d7c4 --- /dev/null +++ b/regression/cbmc/Pointer_Arithmetic16/main.c @@ -0,0 +1,10 @@ +#include + +int main() +{ + int *ptr = malloc(sizeof(int) * 2); + int *other_ptr; + if(ptr + 1 == other_ptr) + return 0; + __CPROVER_assert(0, ""); +} diff --git a/regression/cbmc/Pointer_Arithmetic16/test.desc b/regression/cbmc/Pointer_Arithmetic16/test.desc new file mode 100644 index 00000000000..34e9937c5ed --- /dev/null +++ b/regression/cbmc/Pointer_Arithmetic16/test.desc @@ -0,0 +1,11 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +Value-set filtering did not take into account arithemetic over pointers and thus +spuriously failed an invariant. diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 350e75f14f8..e08ef1d8af5 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -70,10 +70,9 @@ void goto_symext::apply_goto_condition( /// Try to evaluate a simple pointer comparison. /// \param operation: ID_equal or ID_not_equal /// \param symbol_expr: The symbol expression in the condition -/// \param other_operand: The other expression in the condition - must pass -/// goto_symex_is_constant, and since it is pointer-typed it must therefore -/// be an address of expression, a typecast of an address of expression or a -/// null pointer +/// \param other_operand: The other expression in the condition; we only support +/// an address of expression, a typecast of an address of expression or a +/// null pointer, and return an empty optionalt in all other cases /// \param value_set: The value-set for looking up what the symbol can point to /// \param language_mode: The language mode /// \param ns: A namespace @@ -90,12 +89,12 @@ static optionalt> try_evaluate_pointer_comparison( const constant_exprt *constant_expr = expr_try_dynamic_cast(other_operand); - INVARIANT( - skip_typecast(other_operand).id() == ID_address_of || - (constant_expr && constant_expr->get_value() == ID_NULL), - "An expression that passes goto_symex_is_constant and has " - "pointer-type must be an address of expression (possibly with some " - "typecasts) or a null pointer"); + if( + skip_typecast(other_operand).id() != ID_address_of && + (!constant_expr || constant_expr->get_value() != ID_NULL)) + { + return {}; + } const ssa_exprt *ssa_symbol_expr = expr_try_dynamic_cast(symbol_expr);