Add tracing for enumerations

bmw-software-engineering · Oct 4, 2023 · e2518b9 · e2518b9
1 parent 8beee5c
commit e2518b9
Show file tree

Hide file tree

Showing 10 changed files with 38 additions and 1 deletion.
diff --git a/tests-system/enum-ok/tracing b/tests-system/enum-ok/tracing
@@ -0,0 +1 @@
+LRM.Enumeration_Declaration
diff --git a/tests-system/enum/tracing 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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")
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		rbt-unique-enumeration-literals/foo.rsl:6:3: trlc error: duplicate definition, previous definition at foo.rsl:4