goto-symex-is-constant: treat x * sizeof(t) and sizeof(t) * x alike

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)
     {

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 \

unit/goto-symex/is_constant.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);
+      }
+    }
+  }
+}