debugging

Author: tautschnig

src/goto-symex/build_goto_trace.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening
 
 #include "build_goto_trace.h"
 
+#include <iostream>
 #include <cassert>
 
 #include <util/arith_tools.h>

src/goto-symex/goto_symex_state.cpp

@@ -240,6 +240,8 @@ void goto_symex_statet::assignment(
   value_set.output(ns, std::cout);
   std::cout << "**********************\n";
   #endif
+  std::cerr << "LHS: " << lhs.pretty() << std::endl;
+  std::cerr << "RHS: " << rhs.pretty() << std::endl;
 }
 
 void goto_symex_statet::set_l0_indices(

src/goto-symex/symex_assign.cpp

@@ -9,6 +9,9 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Symbolic Execution
 
+#include <iostream>
+#include <util/format_expr.h>
+
 #include "goto_symex.h"
 
 #include <util/byte_operators.h>
@@ -235,8 +238,11 @@ void goto_symext::symex_assign_symbol(
   // TODO: done via rename
   // field_sensitivityt::apply(ns, ssa_rhs, false);
 
+  std::cerr << "ssa_rhs before rename: " << format(ssa_rhs) << std::endl;
   state.rename(ssa_rhs, ns);
+  std::cerr << "ssa_rhs after rename: " << format(ssa_rhs) << std::endl;
 
+  std::cerr << "lhs before mods: " << format(lhs) << std::endl;
   ssa_exprt lhs_mod = lhs;
 
   if(
@@ -331,7 +337,10 @@ void goto_symext::symex_assign_symbol(
   }
 #endif
 
+  std::cerr << "lhs after mods: " << format(lhs) << std::endl;
+  std::cerr << "lhs_mod after mods: " << format(lhs_mod) << std::endl;
   do_simplify(ssa_rhs);
+  std::cerr << "ssa_rhs after simp: " << format(ssa_rhs) << std::endl;
 
   ssa_exprt ssa_lhs = lhs_mod;
   state.assignment(

src/solvers/flattening/boolbv_index.cpp

@@ -9,6 +9,9 @@ Author: Daniel Kroening, [email protected]
 #include "boolbv.h"
 
 #include <algorithm>
+#include <iostream>
+#include <util/format_expr.h>
+#include <util/format_type.h>
 
 #include <util/arith_tools.h>
 #include <util/cprover_prefix.h>
@@ -129,6 +132,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     if((array.id()==ID_constant || array.id()==ID_array) &&
        prop.has_set_to())
     {
+      std::cerr << "HACK: " << array.id() << std::endl;
       #ifdef CONSTANT_ARRAY_HACK
       // TODO : Compile the whole array into a single relation
       #endif
@@ -139,6 +143,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       const std::string identifier = CPROVER_PREFIX "internal_actual_array_" +
                                      std::to_string(actual_array_counter++);
 
+      std::cerr << "expr.type() = " << format(expr.type()) << std::endl;
       symbol_exprt result(identifier, expr.type());
       bv = convert_bv(result);
 
@@ -170,6 +175,8 @@ bvt boolbvt::convert_index(const index_exprt &expr)
         value_equality.rhs()=*it++;
 
         // Cache comparisons and equalities
+        std::cerr << "imp: " << format(implies_exprt(index_equality,
+                                                 value_equality)) << std::endl;
         prop.l_set_to_true(convert(implies_exprt(index_equality,
                                                  value_equality)));
       }