Print (at debug level) the size of assignments during symex

src/goto-symex/symex_assign.cpp

@@ -12,9 +12,9 @@ Author: Daniel Kroening, [email protected]
 #include "goto_symex.h"
 
 #include <util/byte_operators.h>
-#include <util/cprover_prefix.h>
-
 #include <util/c_types.h>
+#include <util/cprover_prefix.h>
+#include <util/pointer_offset_size.h>
 
 #include "goto_symex_state.h"
 
@@ -251,6 +251,14 @@ void goto_symext::symex_assign_symbol(
   if(symbol.is_auxiliary)
     assignment_type=symex_targett::assignment_typet::HIDDEN;
 
+  log.conditional_output(
+    log.debug(),
+    [this, &ssa_lhs](messaget::mstreamt &mstream) {
+      mstream << "Assignment to " << ssa_lhs.get_identifier()
+              << " [" << pointer_offset_bits(ssa_lhs.type(), ns) << " bits]"
+              << messaget::eom;
+    });
+
   target.assignment(
     tmp_guard.as_expr(),
     ssa_lhs,

src/goto-symex/symex_goto.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/invariant.h>
+#include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
 
 #include <analyses/dirty.h>
@@ -249,6 +250,14 @@ void goto_symext::symex_goto(statet &state)
 
       guardt guard;
 
+      log.conditional_output(
+        log.debug(),
+        [this, &new_lhs](messaget::mstreamt &mstream) {
+          mstream << "Assignment to " << new_lhs.get_identifier()
+                  << " [" << pointer_offset_bits(new_lhs.type(), ns) << " bits]"
+                  << messaget::eom;
+        });
+
       target.assignment(
         guard.as_expr(),
         new_lhs, new_lhs, guard_symbol_expr,
@@ -473,6 +482,14 @@ void goto_symext::phi_function(
     dest_state.assignment(new_lhs, rhs, ns, true, true);
     dest_state.record_events=record_events;
 
+    log.conditional_output(
+      log.debug(),
+      [this, &new_lhs](messaget::mstreamt &mstream) {
+        mstream << "Assignment to " << new_lhs.get_identifier()
+                << " [" << pointer_offset_bits(new_lhs.type(), ns) << " bits]"
+                << messaget::eom;
+      });
+
     target.assignment(
       true_exprt(),
       new_lhs, new_lhs, new_lhs.get_original_expr(),