Merge pull request #872 from reuk/assignment-typet-fix-master

Assignment typet fix master

Author: kroening

src/goto-symex/build_goto_trace.cpp

@@ -191,7 +191,9 @@ void build_goto_trace(
           symex_target_equationt::assignment_typet::PHI ||
         SSA_step.assignment_type==
           symex_target_equationt::assignment_typet::GUARD))
+    {
       continue;
+    }
 
     goto_tracet::stepst &steps=time_map[current_time];
     steps.push_back(goto_trace_stept());

src/goto-symex/symex_target.h

@@ -56,7 +56,12 @@ class symex_targett
 
   enum class assignment_typet
   {
-    STATE, HIDDEN, VISIBLE_ACTUAL_PARAMETER, HIDDEN_ACTUAL_PARAMETER, PHI, GUARD
+    STATE,
+    HIDDEN,
+    VISIBLE_ACTUAL_PARAMETER,
+    HIDDEN_ACTUAL_PARAMETER,
+    PHI,
+    GUARD,
   };
 
   // read event

src/goto-symex/symex_target_equation.cpp

@@ -647,17 +647,23 @@ void symex_target_equationt::SSA_stept::output(
     switch(assignment_type)
     {
     case assignment_typet::HIDDEN:
-      out << "HIDDEN"; break;
+      out << "HIDDEN";
+      break;
     case assignment_typet::STATE:
-      out << "STATE"; break;
+      out << "STATE";
+      break;
     case assignment_typet::VISIBLE_ACTUAL_PARAMETER:
-      out << "VISIBLE_ACTUAL_PARAMETER"; break;
+      out << "VISIBLE_ACTUAL_PARAMETER";
+      break;
     case assignment_typet::HIDDEN_ACTUAL_PARAMETER:
-      out << "HIDDEN_ACTUAL_PARAMETER"; break;
+      out << "HIDDEN_ACTUAL_PARAMETER";
+      break;
     case assignment_typet::PHI:
-      out << "PHI"; break;
+      out << "PHI";
+      break;
     case assignment_typet::GUARD:
-      out << "GUARD"; break;
+      out << "GUARD";
+      break;
     default:
       {
       }

src/goto-symex/symex_target_equation.h

@@ -207,7 +207,7 @@ class symex_target_equationt:public symex_targett
     bool is_atomic_end() const      { return type==goto_trace_stept::typet::ATOMIC_END; }
 
     // we may choose to hide
-    bool hidden;
+    bool hidden=false;
 
     exprt guard;
     literalt guard_literal;
@@ -216,7 +216,7 @@ class symex_target_equationt:public symex_targett
     ssa_exprt ssa_lhs;
     exprt ssa_full_lhs, original_full_lhs;
     exprt ssa_rhs;
-    assignment_typet assignment_type;
+    assignment_typet assignment_type=assignment_typet::STATE;
 
     // for ASSUME/ASSERT/GOTO/CONSTRAINT
     exprt cond_expr;
@@ -225,18 +225,18 @@ class symex_target_equationt:public symex_targett
 
     // for INPUT/OUTPUT
     irep_idt format_string, io_id;
-    bool formatted;
+    bool formatted=false;
     std::list<exprt> io_args;
     std::list<exprt> converted_io_args;
 
     // for function call/return
     irep_idt identifier;
 
     // for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
-    unsigned atomic_section_id;
+    unsigned atomic_section_id=0;
 
     // for slicing
-    bool ignore;
+    bool ignore=false;
 
     SSA_stept():
       type(goto_trace_stept::typet::NONE),