goto-symex-is-constant: treat `x * sizeof(t)` and `sizeof(t) * x` alike
Previously it would refuse and allow constant propagation respectively.
This commit is contained in:
parent
b77b5b09d4
commit
eb7fc4bb7f
|
@ -22,16 +22,18 @@ protected:
|
|||
{
|
||||
if(expr.id() == ID_mult)
|
||||
{
|
||||
bool found_non_constant = false;
|
||||
|
||||
// propagate stuff with sizeof in it
|
||||
forall_operands(it, expr)
|
||||
{
|
||||
if(it->find(ID_C_c_sizeof_type).is_not_nil())
|
||||
return true;
|
||||
else if(!is_constant(*it))
|
||||
return false;
|
||||
found_non_constant = true;
|
||||
}
|
||||
|
||||
return true;
|
||||
return !found_non_constant;
|
||||
}
|
||||
else if(expr.id() == ID_with)
|
||||
{
|
||||
|
|
|
@ -29,6 +29,7 @@ SRC += analyses/ai/ai.cpp \
|
|||
goto-programs/goto_trace_output.cpp \
|
||||
goto-programs/xml_expr.cpp \
|
||||
goto-symex/ssa_equation.cpp \
|
||||
goto-symex/is_constant.cpp \
|
||||
interpreter/interpreter.cpp \
|
||||
json/json_parser.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