Duplicate notes edge after they have been fully created

ispras · Mar 14, 2024 · 25412e5 · 25412e5
1 parent 46a1423
commit 25412e5
Showing 1 changed file with 9 additions and 4 deletions.
diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py
@@ -248,6 +248,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
             condition = None
             invariant = None
             invariant_scope = None
+            cur_notes = {}
             for data in edge.findall('graphml:data', self.WITNESS_NS):
                 data_key = data.attrib.get('key')
                 if data_key == 'originfile':
@@ -314,16 +315,20 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
                     end_offset = int(data.text)
                 elif data_key in ('note', 'warning'):
                     tag, note_desc = self.internal_witness.process_note(data_key, data.text)
-                    self._logger.debug(f"Add verifier {tag}: '{note_desc}' for edge {_edge}")
-                    new_edge = self.internal_witness.add_edge(target_node_id, _edge)
-                    new_edge[tag] = note_desc
-                    self.internal_witness.is_notes = True
+                    cur_notes[tag] = note_desc
                 elif data_key == 'env':
                     _edge['env'] = self.internal_witness.process_comment(data.text)
                 elif data_key not in unsupported_edge_data_keys:
                     self._logger.warning(f'Edge data key {data_key} is not supported')
                     unsupported_edge_data_keys[data_key] = None
 
+            for tag, note_desc in cur_notes.items():
+                # Actually there is only one note available.
+                self._logger.debug(f"Add verifier {tag}: '{note_desc}' for edge {_edge}")
+                new_edge = self.internal_witness.add_edge(target_node_id, _edge)
+                new_edge[tag] = note_desc
+                self.internal_witness.is_notes = True
+
             if invariant and invariant_scope:
                 self.internal_witness.add_invariant(invariant, invariant_scope)