Invariants must be added to nodes

src/goto-programs/graphml_witness.cpp

@@ -151,6 +151,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
   graphml[sink].node_name="sink";
   graphml[sink].thread_nr=0;
   graphml[sink].is_violation=false;
+  graphml[sink].has_invariant=false;
 
   // step numbers start at 1
   std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
@@ -196,6 +197,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
     graphml[node].thread_nr=it->thread_nr;
     graphml[node].is_violation=
       it->type==goto_trace_stept::ASSERT && !it->cond_value;
+    graphml[node].has_invariant=false;
 
     step_to_node[it->step_nr]=node;
   }
@@ -341,6 +343,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
   graphml[sink].node_name="sink";
   graphml[sink].thread_nr=0;
   graphml[sink].is_violation=false;
+  graphml[sink].has_invariant=false;
 
   // step numbers start at 1
   std::vector<std::size_t> step_to_node(equation.SSA_steps.size()+1, 0);
@@ -384,6 +387,8 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
     graphml[node].file=source_location.get_file();
     graphml[node].line=source_location.get_line();
     graphml[node].thread_nr=it->source.thread_nr;
+    graphml[node].is_violation=false;
+    graphml[node].has_invariant=false;
 
     step_to_node[step_nr]=node;
   }
@@ -442,14 +447,11 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
         {
           irep_idt identifier=it->ssa_lhs.get_object_name();
 
-          xmlt &val=edge.new_element("data");
-          val.set_attribute("key", "invariant");
+          graphml[to].has_invariant=true;
           code_assignt assign(it->ssa_full_lhs, it->ssa_rhs);
-          val.data=convert_assign_rec(identifier, assign);
-
-          xmlt &val_s=edge.new_element("data");
-          val_s.set_attribute("key", "invariant.scope");
-          val_s.data=id2string(it->source.pc->source_location.get_function());
+          graphml[to].invariant=convert_assign_rec(identifier, assign);
+          graphml[to].invariant_scope=
+            id2string(it->source.pc->source_location.get_function());
         }
         else if(it->is_goto() &&
                 it->source.pc->is_goto())

src/xmllang/graphml.cpp

@@ -75,6 +75,7 @@ static bool build_graph_rec(
     graphmlt::nodet &node=dest[n];
     node.node_name=node_name;
     node.is_violation=false;
+    node.has_invariant=false;
     node.thread_nr=0;
 
     for(xmlt::elementst::const_iterator
@@ -607,6 +608,17 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
       entry.data="true";
     }
 
+    if(n.has_invariant)
+    {
+      xmlt &val=node.new_element("data");
+      val.set_attribute("key", "invariant");
+      val.data=n.invariant;
+
+      xmlt &val_s=node.new_element("data");
+      val_s.set_attribute("key", "invariant.scope");
+      val_s.data=n.invariant_scope;
+    }
+
     for(graphmlt::edgest::const_iterator
         e_it=n.out.begin();
         e_it!=n.out.end();

src/xmllang/graphml.h

@@ -32,6 +32,9 @@ struct xml_graph_nodet:public graph_nodet<xml_edget>
   irep_idt line;
   unsigned thread_nr;
   bool is_violation;
+  bool has_invariant;
+  std::string invariant;
+  std::string invariant_scope;
 };
 
 class graphmlt : public graph<xml_graph_nodet>