Merge pull request #4574 from smowton/smowton/fix/brittle-goto-symex-is-constant
goto-symex-is-constant: treat `x * sizeof(t)` and `sizeof(t) * x` alike
This commit is contained in:
commit
0128bb26ec
|
@ -22,16 +22,18 @@ protected:
|
||||||
{
|
{
|
||||||
if(expr.id() == ID_mult)
|
if(expr.id() == ID_mult)
|
||||||
{
|
{
|
||||||
|
bool found_non_constant = false;
|
||||||
|
|
||||||
// propagate stuff with sizeof in it
|
// propagate stuff with sizeof in it
|
||||||
forall_operands(it, expr)
|
forall_operands(it, expr)
|
||||||
{
|
{
|
||||||
if(it->find(ID_C_c_sizeof_type).is_not_nil())
|
if(it->find(ID_C_c_sizeof_type).is_not_nil())
|
||||||
return true;
|
return true;
|
||||||
else if(!is_constant(*it))
|
else if(!is_constant(*it))
|
||||||
return false;
|
found_non_constant = true;
|
||||||
}
|
}
|
||||||
|
|
||||||
return true;
|
return !found_non_constant;
|
||||||
}
|
}
|
||||||
else if(expr.id() == ID_with)
|
else if(expr.id() == ID_with)
|
||||||
{
|
{
|
||||||
|
|
|
@ -29,6 +29,7 @@ SRC += analyses/ai/ai.cpp \
|
||||||
goto-programs/goto_trace_output.cpp \
|
goto-programs/goto_trace_output.cpp \
|
||||||
goto-programs/xml_expr.cpp \
|
goto-programs/xml_expr.cpp \
|
||||||
goto-symex/ssa_equation.cpp \
|
goto-symex/ssa_equation.cpp \
|
||||||
|
goto-symex/is_constant.cpp \
|
||||||
interpreter/interpreter.cpp \
|
interpreter/interpreter.cpp \
|
||||||
json/json_parser.cpp \
|
json/json_parser.cpp \
|
||||||
json_symbol_table.cpp \
|
json_symbol_table.cpp \
|
||||||
|
|
|
@ -0,0 +1,55 @@
|
||||||
|
/*******************************************************************\
|
||||||
|
|
||||||
|
Module: Unit tests for goto_symex_is_constantt
|
||||||
|
|
||||||
|
Author: Diffblue Ltd.
|
||||||
|
|
||||||
|
\*******************************************************************/
|
||||||
|
|
||||||
|
#include <testing-utils/message.h>
|
||||||
|
#include <testing-utils/use_catch.h>
|
||||||
|
|
||||||
|
#include <goto-symex/goto_symex_is_constant.h>
|
||||||
|
#include <util/std_expr.h>
|
||||||
|
#include <util/std_types.h>
|
||||||
|
|
||||||
|
SCENARIO("goto-symex-is-constant", "[core][goto-symex][is_constant]")
|
||||||
|
{
|
||||||
|
signedbv_typet int_type(32);
|
||||||
|
constant_exprt sizeof_constant("4", int_type);
|
||||||
|
sizeof_constant.set(ID_C_c_sizeof_type, int_type);
|
||||||
|
symbol_exprt non_constant("x", int_type);
|
||||||
|
|
||||||
|
goto_symex_is_constantt is_constant;
|
||||||
|
|
||||||
|
GIVEN("Sizeof expression multiplied by a non-constant")
|
||||||
|
{
|
||||||
|
mult_exprt non_const_by_sizeof(non_constant, sizeof_constant);
|
||||||
|
mult_exprt sizeof_by_non_const(sizeof_constant, non_constant);
|
||||||
|
WHEN("We check whether goto-symex regards the expression as constant")
|
||||||
|
{
|
||||||
|
bool result1 = is_constant(non_const_by_sizeof);
|
||||||
|
bool result2 = is_constant(sizeof_by_non_const);
|
||||||
|
|
||||||
|
THEN("Should be constant")
|
||||||
|
{
|
||||||
|
REQUIRE(result1);
|
||||||
|
REQUIRE(result2);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
GIVEN("Non-multiply expression involving a sizeof expression")
|
||||||
|
{
|
||||||
|
plus_exprt non_const_plus_sizeof(non_constant, sizeof_constant);
|
||||||
|
WHEN("We check whether goto-symex regards the expression as constant")
|
||||||
|
{
|
||||||
|
bool result = is_constant(non_const_plus_sizeof);
|
||||||
|
|
||||||
|
THEN("Should not be constant")
|
||||||
|
{
|
||||||
|
REQUIRE(!result);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
Loading…
Reference in New Issue