From 25412e55e982ab71bea5b66f82fadc1a48930a70 Mon Sep 17 00:00:00 2001 From: Mordan Vitalii Date: Thu, 14 Mar 2024 12:18:35 +0800 Subject: [PATCH] Duplicate notes edge after they have been fully created --- scripts/mea/et/parser.py | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py index 47fe020..678620e 100644 --- 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)