From 149a7910cf3e175c087fcd97eac7f35117e10afc Mon Sep 17 00:00:00 2001 From: MugdhaDhole Date: Tue, 19 Mar 2024 16:27:41 +0530 Subject: [PATCH] Remove warnings regarding duplicate late declaration of packages (#72) ISSUE: #72 --- CHANGELOG.md | 3 +++ language-reference-manual/lrm.trlc | 5 ----- tests-system/late-packages-1/output | 4 +--- tests-system/late-packages-1/output.brief | 1 - tests-system/late-packages-1/output.json | 4 +--- tests-system/late-packages-1/output.smtlib | 4 +--- tests-system/rbt-late-package-declarations/output | 4 +--- .../rbt-late-package-declarations/output.brief | 1 - tests-system/rbt-late-package-declarations/output.json | 4 +--- .../rbt-late-package-declarations/output.smtlib | 4 +--- tests-system/rbt-late-package-declarations/tracing | 1 - trlc/parser.py | 10 ---------- 12 files changed, 9 insertions(+), 36 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 63124042..c4e86ec6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -27,6 +27,9 @@ generated in the following situations: ### 1.2.3-dev +* [TRLC] A warning is not issued by the tools when encountering + duplicate late package declarations. + * [TRLC] The deprecated builtin function syntax `trlc:foo` has been removed. You should now use `foo` instead. diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index 8057f3bc..12141ab6 100644 --- a/language-reference-manual/lrm.trlc +++ b/language-reference-manual/lrm.trlc @@ -1670,11 +1670,6 @@ section "TRLC Files" { declares it.''' } - Recommendation Duplicate_Late_Packages { - text = '''It is recommended to issue a warning if two `.trlc` files - declare the same package.''' - } - 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 diff --git a/tests-system/late-packages-1/output b/tests-system/late-packages-1/output index c57933b7..1140f7f3 100644 --- a/tests-system/late-packages-1/output +++ b/tests-system/late-packages-1/output @@ -1,3 +1 @@ -package a - ^ late-packages-1/b.trlc:1: warning: duplicate late declaration of package a, previous declaration in a.trlc:1; consider adding an rsl file declaring the package -Processed 1 model, 0 checks and 2 requirement files and found 1 warning +Processed 1 model, 0 checks and 2 requirement files and found no issues diff --git a/tests-system/late-packages-1/output.brief b/tests-system/late-packages-1/output.brief index e32a1a47..e69de29b 100644 --- a/tests-system/late-packages-1/output.brief +++ b/tests-system/late-packages-1/output.brief @@ -1 +0,0 @@ -late-packages-1/b.trlc:1:9: trlc warning: duplicate late declaration of package a, previous declaration in a.trlc:1; consider adding an rsl file declaring the package diff --git a/tests-system/late-packages-1/output.json b/tests-system/late-packages-1/output.json index 4f6235c3..24164c87 100644 --- a/tests-system/late-packages-1/output.json +++ b/tests-system/late-packages-1/output.json @@ -1,4 +1,2 @@ -package a - ^ late-packages-1/b.trlc:1: warning: duplicate late declaration of package a, previous declaration in a.trlc:1; consider adding an rsl file declaring the package {} -Processed 1 model, 0 checks and 2 requirement files and found 1 warning +Processed 1 model, 0 checks and 2 requirement files and found no issues diff --git a/tests-system/late-packages-1/output.smtlib b/tests-system/late-packages-1/output.smtlib index c57933b7..1140f7f3 100644 --- a/tests-system/late-packages-1/output.smtlib +++ b/tests-system/late-packages-1/output.smtlib @@ -1,3 +1 @@ -package a - ^ late-packages-1/b.trlc:1: warning: duplicate late declaration of package a, previous declaration in a.trlc:1; consider adding an rsl file declaring the package -Processed 1 model, 0 checks and 2 requirement files and found 1 warning +Processed 1 model, 0 checks and 2 requirement files and found no issues diff --git a/tests-system/rbt-late-package-declarations/output b/tests-system/rbt-late-package-declarations/output index ce3b7e78..673c358c 100644 --- a/tests-system/rbt-late-package-declarations/output +++ b/tests-system/rbt-late-package-declarations/output @@ -1,3 +1 @@ -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 models, 0 checks and 3 requirement files and found 1 warning +Processed 0 models, 0 checks and 3 requirement files and found no issues diff --git a/tests-system/rbt-late-package-declarations/output.brief b/tests-system/rbt-late-package-declarations/output.brief index 75783aa8..e69de29b 100644 --- a/tests-system/rbt-late-package-declarations/output.brief +++ b/tests-system/rbt-late-package-declarations/output.brief @@ -1 +0,0 @@ -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 index b9bede70..d9456610 100644 --- a/tests-system/rbt-late-package-declarations/output.json +++ b/tests-system/rbt-late-package-declarations/output.json @@ -1,4 +1,2 @@ -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 models, 0 checks and 3 requirement files and found 1 warning +Processed 0 models, 0 checks and 3 requirement files and found no issues diff --git a/tests-system/rbt-late-package-declarations/output.smtlib b/tests-system/rbt-late-package-declarations/output.smtlib index ce3b7e78..673c358c 100644 --- a/tests-system/rbt-late-package-declarations/output.smtlib +++ b/tests-system/rbt-late-package-declarations/output.smtlib @@ -1,3 +1 @@ -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 models, 0 checks and 3 requirement files and found 1 warning +Processed 0 models, 0 checks and 3 requirement files and found no issues diff --git a/tests-system/rbt-late-package-declarations/tracing b/tests-system/rbt-late-package-declarations/tracing index f123dc65..e69de29b 100644 --- a/tests-system/rbt-late-package-declarations/tracing +++ b/tests-system/rbt-late-package-declarations/tracing @@ -1 +0,0 @@ -LRM.Duplicate_Late_Packages diff --git a/trlc/parser.py b/trlc/parser.py index 9befa5c8..09550fdc 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -1835,16 +1835,6 @@ def parse_preamble(self, kind): self.stab.register(self.mh, pkg) 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," - " previous declaration in %s;" - " consider adding an rsl file declaring the" - " package" % - (pkg.name, - self.mh.cross_file_reference(pkg.location))) pkg.set_ast_link(t_pkg) pkg.set_ast_link(self.ct)