diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index 29a8c83e..b536ebbf 100644 --- a/language-reference-manual/lrm.trlc +++ b/language-reference-manual/lrm.trlc @@ -1685,7 +1685,7 @@ section "TRLC Files" { declare the same package.''' } - Recommendation TRLC_Parse_Issue { + Note TRLC_Parse_Issue { text = '''For TRLC files it is impossible fully parse a file in isolation, since we must process at least the package indication of every other trlc file to know which import diff --git a/tests-system/duplicate-late-packages/output b/tests-system/duplicate-late-packages/output deleted file mode 100644 index c839b5bb..00000000 --- a/tests-system/duplicate-late-packages/output +++ /dev/null @@ -1,3 +0,0 @@ -package Foo - ^^^ duplicate-late-packages/foo.trlc:1: warning: duplicate late declaration of package Foo, previous declaration in bar.trlc:1; consider adding an rsl file declaring the package -Processed 0 model(s), 0 check(s) and 3 requirement file(s) and found 1 warning(s) diff --git a/tests-system/duplicate-late-packages/output.brief b/tests-system/duplicate-late-packages/output.brief deleted file mode 100644 index 9190bc98..00000000 --- a/tests-system/duplicate-late-packages/output.brief +++ /dev/null @@ -1 +0,0 @@ -duplicate-late-packages/foo.trlc:1:9: trlc warning: duplicate late declaration of package Foo, previous declaration in bar.trlc:1; consider adding an rsl file declaring the package diff --git a/tests-system/duplicate-late-packages/output.json b/tests-system/duplicate-late-packages/output.json deleted file mode 100644 index b423bfdf..00000000 --- a/tests-system/duplicate-late-packages/output.json +++ /dev/null @@ -1,4 +0,0 @@ -package Foo - ^^^ duplicate-late-packages/foo.trlc:1: warning: duplicate late declaration of package Foo, previous declaration in bar.trlc:1; consider adding an rsl file declaring the package -{} -Processed 0 model(s), 0 check(s) and 3 requirement file(s) and found 1 warning(s) diff --git a/tests-system/duplicate-late-packages/output.smtlib b/tests-system/duplicate-late-packages/output.smtlib deleted file mode 100644 index c839b5bb..00000000 --- a/tests-system/duplicate-late-packages/output.smtlib +++ /dev/null @@ -1,3 +0,0 @@ -package Foo - ^^^ duplicate-late-packages/foo.trlc:1: warning: duplicate late declaration of package Foo, previous declaration in bar.trlc:1; consider adding an rsl file declaring the package -Processed 0 model(s), 0 check(s) and 3 requirement file(s) and found 1 warning(s) diff --git a/tests-system/duplicate-late-packages/bar.trlc b/tests-system/rbt-late-package-declarations/bar.trlc similarity index 100% rename from tests-system/duplicate-late-packages/bar.trlc rename to tests-system/rbt-late-package-declarations/bar.trlc diff --git a/tests-system/duplicate-late-packages/baz.trlc b/tests-system/rbt-late-package-declarations/baz.trlc similarity index 100% rename from tests-system/duplicate-late-packages/baz.trlc rename to tests-system/rbt-late-package-declarations/baz.trlc diff --git a/tests-system/duplicate-late-packages/foo.trlc b/tests-system/rbt-late-package-declarations/foo.trlc similarity index 100% rename from tests-system/duplicate-late-packages/foo.trlc rename to tests-system/rbt-late-package-declarations/foo.trlc diff --git a/tests-system/rbt-late-package-declarations/output b/tests-system/rbt-late-package-declarations/output new file mode 100644 index 00000000..8e196436 --- /dev/null +++ b/tests-system/rbt-late-package-declarations/output @@ -0,0 +1,3 @@ +package Foo + ^^^ rbt-late-package-declarations/foo.trlc:1: warning: duplicate late declaration of package Foo, previous declaration in bar.trlc:1; consider adding an rsl file declaring the package +Processed 0 model(s), 0 check(s) and 3 requirement file(s) and found 1 warning(s) diff --git a/tests-system/rbt-late-package-declarations/output.brief b/tests-system/rbt-late-package-declarations/output.brief new file mode 100644 index 00000000..75783aa8 --- /dev/null +++ b/tests-system/rbt-late-package-declarations/output.brief @@ -0,0 +1 @@ +rbt-late-package-declarations/foo.trlc:1:9: trlc warning: duplicate late declaration of package Foo, previous declaration in bar.trlc:1; consider adding an rsl file declaring the package diff --git a/tests-system/rbt-late-package-declarations/output.json b/tests-system/rbt-late-package-declarations/output.json new file mode 100644 index 00000000..61f2766d --- /dev/null +++ b/tests-system/rbt-late-package-declarations/output.json @@ -0,0 +1,4 @@ +package Foo + ^^^ rbt-late-package-declarations/foo.trlc:1: warning: duplicate late declaration of package Foo, previous declaration in bar.trlc:1; consider adding an rsl file declaring the package +{} +Processed 0 model(s), 0 check(s) and 3 requirement file(s) and found 1 warning(s) diff --git a/tests-system/rbt-late-package-declarations/output.smtlib b/tests-system/rbt-late-package-declarations/output.smtlib new file mode 100644 index 00000000..8e196436 --- /dev/null +++ b/tests-system/rbt-late-package-declarations/output.smtlib @@ -0,0 +1,3 @@ +package Foo + ^^^ rbt-late-package-declarations/foo.trlc:1: warning: duplicate late declaration of package Foo, previous declaration in bar.trlc:1; consider adding an rsl file declaring the package +Processed 0 model(s), 0 check(s) and 3 requirement file(s) and found 1 warning(s) diff --git a/tests-system/rbt-late-package-declarations/tracing b/tests-system/rbt-late-package-declarations/tracing new file mode 100644 index 00000000..f123dc65 --- /dev/null +++ b/tests-system/rbt-late-package-declarations/tracing @@ -0,0 +1 @@ +LRM.Duplicate_Late_Packages diff --git a/tests-system/simple/tracing b/tests-system/simple/tracing index 002c42f3..643244ff 100644 --- a/tests-system/simple/tracing +++ b/tests-system/simple/tracing @@ -5,3 +5,4 @@ LRM.RSL_File LRM.Check_File LRM.Deprecated_Check_Files LRM.Check_Block +LRM.TRLC_File diff --git a/trlc/parser.py b/trlc/parser.py index 9316db50..0b67d2be 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -1581,6 +1581,7 @@ def parse_record_object_declaration(self): return obj def parse_trlc_entry(self): + # lobster-trace: LRM.TRLC_File if self.peek_kw("section"): self.parse_section_declaration() else: @@ -1602,6 +1603,7 @@ def parse_preamble(self, kind): elif kind == "check": declare_package = False else: + # lobster-trace: LRM.Late_Package_Declarations declare_package = not self.stab.contains(self.ct.value) if declare_package: @@ -1614,6 +1616,7 @@ def parse_preamble(self, kind): else: pkg = self.stab.lookup(self.mh, self.ct, ast.Package) if pkg.declared_late and kind == "trlc": + # lobster-trace: LRM.Duplicate_Late_Packages self.mh.warning( self.ct.location, "duplicate late declaration of package %s," @@ -1709,6 +1712,7 @@ def parse_check_file(self): return ok def parse_trlc_file(self): + # lobster-trace: LRM.TRLC_File assert self.cu.package is not None self.cu.resolve_imports(self.mh, self.stab) diff --git a/trlc/trlc.py b/trlc/trlc.py index 7cc2c37f..f5d28232 100644 --- a/trlc/trlc.py +++ b/trlc/trlc.py @@ -280,6 +280,7 @@ def register_check_file(self, file_name, file_content=None): file_content) def register_trlc_file(self, file_name, file_content=None): + # lobster-trace: LRM.TRLC_File assert os.path.isfile(file_name) assert file_name not in self.trlc_files assert isinstance(file_content, str) or file_content is None @@ -362,6 +363,7 @@ def parse_check_files(self): return ok def parse_trlc_files(self): + # lobster-trace: LRM.TRLC_File # lobster-trace: LRM.Preamble ok = True