From 3141c490a1de19612b6e5b13ec5a003c96987f53 Mon Sep 17 00:00:00 2001 From: Mordan Vitalii Date: Thu, 14 Mar 2024 00:57:53 +0800 Subject: [PATCH] Add support for several notes for the same edge Issue #61 --- scripts/mea/et/internal_witness.py | 6 +++++- scripts/mea/et/parser.py | 4 +++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/scripts/mea/et/internal_witness.py b/scripts/mea/et/internal_witness.py index 80cb416..3c155a3 100644 --- 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 index 826005b..c235dbb 100644 --- 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)