diff --git a/scripts/mea/et/internal_witness.py b/scripts/mea/et/internal_witness.py index 34fe03e..3f44114 100644 --- a/scripts/mea/et/internal_witness.py +++ b/scripts/mea/et/internal_witness.py @@ -31,6 +31,9 @@ TAG_LEVEL = "level" TAG_VALUE = "value" +WITNESS_TYPE_VIOLATION = "violation" +WITNESS_TYPE_CORRECTNESS = "correctness" + # Capitalize first letters of attribute names. def capitalize_attr_names(attrs): @@ -152,7 +155,7 @@ def add_edge(self, target, template_edge=None): else: # Here we just create a new edge self._edges.append(edge) - if self.witness_type == 'correctness': + if self.witness_type == WITNESS_TYPE_CORRECTNESS: if target in self.invariants: edge['invariants'] = self.invariants[target] if template_edge: @@ -300,7 +303,7 @@ def process_verifier_notes(self): edge['note'] = self.process_comment(note) break - if not warn_edges and self.witness_type == 'violation': + if not warn_edges and self.witness_type == WITNESS_TYPE_VIOLATION: if self._edges: last_edge = self._edges[-1] if 'note' in last_edge: @@ -431,7 +434,7 @@ def add_thread(self, thread_id: str): def final_checks(self, entry_point="main"): # Check for warnings - if self.witness_type == 'violation': + if self.witness_type == WITNESS_TYPE_VIOLATION: if not self.is_call_stack: self._warnings.append('No call stack (please add tags "enterFunction" and ' '"returnFrom" to improve visualization)') diff --git a/scripts/mea/et/parser.py b/scripts/mea/et/parser.py index 5046be1..9d6585f 100644 --- a/scripts/mea/et/parser.py +++ b/scripts/mea/et/parser.py @@ -26,7 +26,7 @@ import re from xml.etree import ElementTree -from mea.et.internal_witness import InternalWitness +from mea.et.internal_witness import InternalWitness, WITNESS_TYPE_VIOLATION, WITNESS_TYPE_CORRECTNESS class WitnessParser: @@ -147,9 +147,9 @@ def _parse_witness(self, witness): elif key == 'witness-type': witness_type = data.text if witness_type == 'correctness_witness': - self.internal_witness.witness_type = 'correctness' + self.internal_witness.witness_type = WITNESS_TYPE_CORRECTNESS elif witness_type == 'violation_witness': - self.internal_witness.witness_type = 'violation' + self.internal_witness.witness_type = WITNESS_TYPE_VIOLATION else: self._logger.warning(f"Unsupported witness type: {witness_type}") elif key == 'specification': @@ -274,7 +274,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map): if self.entry_point: if self.entry_point == function_name: self.internal_witness.is_main_function = True - if self.internal_witness.witness_type == 'violation': + if self.internal_witness.witness_type == WITNESS_TYPE_VIOLATION: _edge['entry_point'] = "entry point" is_entry_point = True else: @@ -284,7 +284,7 @@ def __parse_witness_edges(self, graph, sink_nodes_map): func_id = self.internal_witness.resolve_function_id(function_name) _edge['enter'] = func_id if not is_entry_point and \ - self.internal_witness.witness_type == 'violation': + self.internal_witness.witness_type == WITNESS_TYPE_VIOLATION: _edge['entry_point'] = "entry point" self.internal_witness.add_thread("decl") is_entry_point = True