Insert notes comments before target edge

ispras · Mar 14, 2024 · c3fd90d · c3fd90d
1 parent 3141c49
commit c3fd90d
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 9 deletions.
diff --git a/scripts/mea/et/internal_witness.py b/scripts/mea/et/internal_witness.py
@@ -144,14 +144,17 @@ def add_attr(self, name, value, associate, compare):
     def add_entry_node_id(self, node_id):
         self._entry_node_id = node_id
 
-    # noinspection PyUnusedLocal
-    def add_edge(self, source, target, template_edge=None):
-        # pylint: disable=unused-argument
-        # TODO: check coherence of source and target.
+    def add_edge(self, target, template_edge=None):
         edge = {}
-        self._edges.append(edge)
-        if target in self.invariants:
-            edge['invariants'] = self.invariants[target]
+        if template_edge:
+            # If there is a template edge, then we create a new edge with comment (note, warn, env).
+            self._edges.insert(len(self._edges) - 1, edge)
+        else:
+            # Here we just create a new edge
+            self._edges.append(edge)
+        if self.witness_type == 'correctness':
+            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'):

diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py
@@ -242,7 +242,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
                 continue
 
             # Update lists of input and output edges for source and target nodes.
-            _edge = self.internal_witness.add_edge(source_node_id, target_node_id)
+            _edge = self.internal_witness.add_edge(target_node_id)
 
             start_offset = 0
             end_offset = 0
@@ -316,7 +316,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map):
                 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(source_node_id, target_node_id, _edge)
+                    new_edge = self.internal_witness.add_edge(target_node_id, _edge)
                     new_edge[tag] = note_desc
                     self.internal_witness.is_notes = True
                 elif data_key == 'env':