diff --git a/src/goto-symex/goto_symex_is_constant.h b/src/goto-symex/goto_symex_is_constant.h index f218ff53b32..d76e3e19c69 100644 --- a/src/goto-symex/goto_symex_is_constant.h +++ b/src/goto-symex/goto_symex_is_constant.h @@ -22,16 +22,18 @@ class goto_symex_is_constantt : public is_constantt { 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) { diff --git a/unit/Makefile b/unit/Makefile index ab374e5378f..f49a0d0be09 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -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 \ diff --git a/unit/goto-symex/is_constant.cpp b/unit/goto-symex/is_constant.cpp new file mode 100644 index 00000000000..a5af38d6843 --- /dev/null +++ b/unit/goto-symex/is_constant.cpp @@ -0,0 +1,55 @@ +/*******************************************************************\ + +Module: Unit tests for goto_symex_is_constantt + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include + +#include +#include +#include + +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); + } + } + } +}