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

Previously it would refuse and allow constant propagation respectively.

Author: smowton

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 \