From e2518b9f1fe4e6d2cb018aab668d2d552fca39d2 Mon Sep 17 00:00:00 2001 From: Florian Schanda Date: Wed, 4 Oct 2023 19:40:12 +0200 Subject: [PATCH] Add tracing for enumerations --- tests-system/enum-ok/tracing | 1 + tests-system/enum/tracing | 1 + .../rbt-unique-enumeration-literals/bar.rsl | 15 +++++++++++++++ .../rbt-unique-enumeration-literals/foo.rsl | 10 ++++++++++ .../rbt-unique-enumeration-literals/output | 3 +++ .../rbt-unique-enumeration-literals/output.brief | 1 + .../rbt-unique-enumeration-literals/output.json | 3 +++ .../rbt-unique-enumeration-literals/output.smtlib | 3 +++ trlc/ast.py | 1 + trlc/parser.py | 1 - 10 files changed, 38 insertions(+), 1 deletion(-) create mode 100644 tests-system/enum-ok/tracing create mode 100644 tests-system/enum/tracing create mode 100644 tests-system/rbt-unique-enumeration-literals/bar.rsl create mode 100644 tests-system/rbt-unique-enumeration-literals/foo.rsl create mode 100644 tests-system/rbt-unique-enumeration-literals/output create mode 100644 tests-system/rbt-unique-enumeration-literals/output.brief create mode 100644 tests-system/rbt-unique-enumeration-literals/output.json create mode 100644 tests-system/rbt-unique-enumeration-literals/output.smtlib diff --git a/tests-system/enum-ok/tracing b/tests-system/enum-ok/tracing new file mode 100644 index 00000000..59a66532 --- /dev/null +++ b/tests-system/enum-ok/tracing @@ -0,0 +1 @@ +LRM.Enumeration_Declaration diff --git a/tests-system/enum/tracing b/tests-system/enum/tracing new file mode 100644 index 00000000..59a66532 --- /dev/null +++ b/tests-system/enum/tracing @@ -0,0 +1 @@ +LRM.Enumeration_Declaration diff --git a/tests-system/rbt-unique-enumeration-literals/bar.rsl b/tests-system/rbt-unique-enumeration-literals/bar.rsl new file mode 100644 index 00000000..346d4459 --- /dev/null +++ b/tests-system/rbt-unique-enumeration-literals/bar.rsl @@ -0,0 +1,15 @@ +package Bar + +enum ASIL { + QM + A + B + C + D +} + +enum Language { + Ada + C // Not an issue since it's a different enum + Python +} diff --git a/tests-system/rbt-unique-enumeration-literals/foo.rsl b/tests-system/rbt-unique-enumeration-literals/foo.rsl new file mode 100644 index 00000000..20aeeb87 --- /dev/null +++ b/tests-system/rbt-unique-enumeration-literals/foo.rsl @@ -0,0 +1,10 @@ +package Foo + +enum E { + Foo + Bar + Foo + Baz + Bork + Baz +} diff --git a/tests-system/rbt-unique-enumeration-literals/output b/tests-system/rbt-unique-enumeration-literals/output new file mode 100644 index 00000000..3bdd2956 --- /dev/null +++ b/tests-system/rbt-unique-enumeration-literals/output @@ -0,0 +1,3 @@ +Foo +^^^ rbt-unique-enumeration-literals/foo.rsl:6: error: duplicate definition, previous definition at foo.rsl:4 +Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/rbt-unique-enumeration-literals/output.brief b/tests-system/rbt-unique-enumeration-literals/output.brief new file mode 100644 index 00000000..81e0e640 --- /dev/null +++ b/tests-system/rbt-unique-enumeration-literals/output.brief @@ -0,0 +1 @@ +rbt-unique-enumeration-literals/foo.rsl:6:3: trlc error: duplicate definition, previous definition at foo.rsl:4 diff --git a/tests-system/rbt-unique-enumeration-literals/output.json b/tests-system/rbt-unique-enumeration-literals/output.json new file mode 100644 index 00000000..3bdd2956 --- /dev/null +++ b/tests-system/rbt-unique-enumeration-literals/output.json @@ -0,0 +1,3 @@ +Foo +^^^ rbt-unique-enumeration-literals/foo.rsl:6: error: duplicate definition, previous definition at foo.rsl:4 +Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/rbt-unique-enumeration-literals/output.smtlib b/tests-system/rbt-unique-enumeration-literals/output.smtlib new file mode 100644 index 00000000..3bdd2956 --- /dev/null +++ b/tests-system/rbt-unique-enumeration-literals/output.smtlib @@ -0,0 +1,3 @@ +Foo +^^^ rbt-unique-enumeration-literals/foo.rsl:6: error: duplicate definition, previous definition at foo.rsl:4 +Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/trlc/ast.py b/trlc/ast.py index 6ed29860..080c1cd7 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -2973,6 +2973,7 @@ def make_visible(self, stab): def register(self, mh, entity): # lobster-trace: LRM.Duplicate_Types + # lobster-trace: LRM.Unique_Enumeration_Literals assert isinstance(mh, Message_Handler) assert isinstance(entity, Entity) diff --git a/trlc/parser.py b/trlc/parser.py index 94407cbb..3db7c648 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -382,7 +382,6 @@ def parse_enum_declaration(self): location = name.location, enum = enum) empty = False - # lobster-trace: LRM.Unique_Enumeration_Literals enum.literals.register(self.mh, lit) self.match("C_KET")