Add support for several notes for the same edge

Issue #61
ispras · Mar 13, 2024 · 3141c49 · 3141c49
1 parent 3d65ed0
commit 3141c49
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/scripts/mea/et/internal_witness.py b/scripts/mea/et/internal_witness.py
@@ -145,13 +145,17 @@ def add_entry_node_id(self, node_id):
         self._entry_node_id = node_id
 
     # noinspection PyUnusedLocal
-    def add_edge(self, source, target):
+    def add_edge(self, source, target, template_edge=None):
         # pylint: disable=unused-argument
         # TODO: check coherence of source and target.
         edge = {}
         self._edges.append(edge)
         if target in self.invariants:
             edge['invariants'] = self.invariants[target]
+        if template_edge:
+            for key, val in template_edge.items():
+                if key not in ('warn', 'note', 'env', 'enter', 'return'):
+                    edge[key] = val
         return edge
 
     def add_file(self, file_name):

diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py
@@ -315,7 +315,9 @@ 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)
-                    _edge[tag] = note_desc
+                    self._logger.debug(f"Add verifier {tag}: '{note_desc}' for edge {_edge}")
+                    new_edge = self.internal_witness.add_edge(source_node_id, target_node_id, _edge)
+                    new_edge[tag] = note_desc
                     self.internal_witness.is_notes = True
                 elif data_key == 'env':
                     _edge['env'] = self.internal_witness.process_comment(data.text)