From da147491194ba9b546117d015757cadae328b70d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Christoph=20Kl=C3=B6ffel?= <145490354+christophkloeffel@users.noreply.github.com> Date: Wed, 11 Oct 2023 14:50:12 +0200 Subject: [PATCH] adds tracing for check files (#35) adds tracing for chapter 9 --- tests-system/rbt-cannot-declare-in-check-file/foo.check | 1 + tests-system/rbt-cannot-declare-in-check-file/output | 3 +++ tests-system/rbt-cannot-declare-in-check-file/output.brief | 1 + tests-system/rbt-cannot-declare-in-check-file/output.json | 3 +++ tests-system/rbt-cannot-declare-in-check-file/output.smtlib | 3 +++ tests-system/rbt-import-in-check/bar.rsl | 1 + tests-system/rbt-import-in-check/foo.check | 3 +++ tests-system/rbt-import-in-check/foo.rsl | 1 + tests-system/rbt-import-in-check/output | 3 +++ tests-system/rbt-import-in-check/output.brief | 1 + tests-system/rbt-import-in-check/output.json | 3 +++ tests-system/rbt-import-in-check/output.smtlib | 3 +++ tests-system/simple/tracing | 2 ++ trlc/parser.py | 4 ++++ trlc/trlc.py | 1 + 15 files changed, 33 insertions(+) create mode 100644 tests-system/rbt-cannot-declare-in-check-file/foo.check create mode 100644 tests-system/rbt-cannot-declare-in-check-file/output create mode 100644 tests-system/rbt-cannot-declare-in-check-file/output.brief create mode 100644 tests-system/rbt-cannot-declare-in-check-file/output.json create mode 100644 tests-system/rbt-cannot-declare-in-check-file/output.smtlib create mode 100644 tests-system/rbt-import-in-check/bar.rsl create mode 100644 tests-system/rbt-import-in-check/foo.check create mode 100644 tests-system/rbt-import-in-check/foo.rsl create mode 100644 tests-system/rbt-import-in-check/output create mode 100644 tests-system/rbt-import-in-check/output.brief create mode 100644 tests-system/rbt-import-in-check/output.json create mode 100644 tests-system/rbt-import-in-check/output.smtlib diff --git a/tests-system/rbt-cannot-declare-in-check-file/foo.check b/tests-system/rbt-cannot-declare-in-check-file/foo.check new file mode 100644 index 00000000..f7b1f4be --- /dev/null +++ b/tests-system/rbt-cannot-declare-in-check-file/foo.check @@ -0,0 +1 @@ +package Foo diff --git a/tests-system/rbt-cannot-declare-in-check-file/output b/tests-system/rbt-cannot-declare-in-check-file/output new file mode 100644 index 00000000..563aa1b2 --- /dev/null +++ b/tests-system/rbt-cannot-declare-in-check-file/output @@ -0,0 +1,3 @@ +package Foo + ^^^ rbt-cannot-declare-in-check-file/foo.check:1: error: unknown symbol Foo +Processed 0 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/rbt-cannot-declare-in-check-file/output.brief b/tests-system/rbt-cannot-declare-in-check-file/output.brief new file mode 100644 index 00000000..f159d699 --- /dev/null +++ b/tests-system/rbt-cannot-declare-in-check-file/output.brief @@ -0,0 +1 @@ +rbt-cannot-declare-in-check-file/foo.check:1:9: trlc error: unknown symbol Foo diff --git a/tests-system/rbt-cannot-declare-in-check-file/output.json b/tests-system/rbt-cannot-declare-in-check-file/output.json new file mode 100644 index 00000000..563aa1b2 --- /dev/null +++ b/tests-system/rbt-cannot-declare-in-check-file/output.json @@ -0,0 +1,3 @@ +package Foo + ^^^ rbt-cannot-declare-in-check-file/foo.check:1: error: unknown symbol Foo +Processed 0 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/rbt-cannot-declare-in-check-file/output.smtlib b/tests-system/rbt-cannot-declare-in-check-file/output.smtlib new file mode 100644 index 00000000..563aa1b2 --- /dev/null +++ b/tests-system/rbt-cannot-declare-in-check-file/output.smtlib @@ -0,0 +1,3 @@ +package Foo + ^^^ rbt-cannot-declare-in-check-file/foo.check:1: error: unknown symbol Foo +Processed 0 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/rbt-import-in-check/bar.rsl b/tests-system/rbt-import-in-check/bar.rsl new file mode 100644 index 00000000..6c9a6655 --- /dev/null +++ b/tests-system/rbt-import-in-check/bar.rsl @@ -0,0 +1 @@ +package Bar diff --git a/tests-system/rbt-import-in-check/foo.check b/tests-system/rbt-import-in-check/foo.check new file mode 100644 index 00000000..17efec44 --- /dev/null +++ b/tests-system/rbt-import-in-check/foo.check @@ -0,0 +1,3 @@ +package Foo + +import Bar diff --git a/tests-system/rbt-import-in-check/foo.rsl b/tests-system/rbt-import-in-check/foo.rsl new file mode 100644 index 00000000..f7b1f4be --- /dev/null +++ b/tests-system/rbt-import-in-check/foo.rsl @@ -0,0 +1 @@ +package Foo diff --git a/tests-system/rbt-import-in-check/output b/tests-system/rbt-import-in-check/output new file mode 100644 index 00000000..de881876 --- /dev/null +++ b/tests-system/rbt-import-in-check/output @@ -0,0 +1,3 @@ +import Bar +^^^^^^ rbt-import-in-check/foo.check:3: error: expected keyword checks, encountered keyword import instead +Processed 2 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/rbt-import-in-check/output.brief b/tests-system/rbt-import-in-check/output.brief new file mode 100644 index 00000000..47e27167 --- /dev/null +++ b/tests-system/rbt-import-in-check/output.brief @@ -0,0 +1 @@ +rbt-import-in-check/foo.check:3:1: trlc error: expected keyword checks, encountered keyword import instead diff --git a/tests-system/rbt-import-in-check/output.json b/tests-system/rbt-import-in-check/output.json new file mode 100644 index 00000000..de881876 --- /dev/null +++ b/tests-system/rbt-import-in-check/output.json @@ -0,0 +1,3 @@ +import Bar +^^^^^^ rbt-import-in-check/foo.check:3: error: expected keyword checks, encountered keyword import instead +Processed 2 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/rbt-import-in-check/output.smtlib b/tests-system/rbt-import-in-check/output.smtlib new file mode 100644 index 00000000..de881876 --- /dev/null +++ b/tests-system/rbt-import-in-check/output.smtlib @@ -0,0 +1,3 @@ +import Bar +^^^^^^ rbt-import-in-check/foo.check:3: error: expected keyword checks, encountered keyword import instead +Processed 2 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/simple/tracing b/tests-system/simple/tracing index b6ac5987..3c4844bf 100644 --- a/tests-system/simple/tracing +++ b/tests-system/simple/tracing @@ -2,3 +2,5 @@ LRM.Layout LRM.File_Parsing_Order LRM.Preamble LRM.RSL_File +LRM.Check_File +LRM.Deprecated_Check_Files diff --git a/trlc/parser.py b/trlc/parser.py index 3db7c648..dfeb1226 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -1583,6 +1583,7 @@ def parse_preamble(self, kind): assert kind in ("rsl", "check", "trlc") # lobster-trace: LRM.Layout # lobster-trace: LRM.Preamble + # lobster-trace: LRM.Cannot_Declare_In_Check_File # First, parse package indication, declaring the package if # needed @@ -1665,6 +1666,7 @@ def parse_rsl_file(self): return ok def parse_check_file(self): + # lobster-trace: LRM.Check_File self.parse_preamble("check") self.cu.resolve_imports(self.mh, self.stab) @@ -1674,6 +1676,7 @@ def parse_check_file(self): try: n_block = self.parse_check_block() self.cu.add_item(n_block) + # lobster-trace: LRM.Deprecated_Check_Files if self.lint_mode: self.mh.check( n_block.location, @@ -1689,6 +1692,7 @@ def parse_check_file(self): # Recovery strategy is to look for the next check # block self.skip_until_newline() + # lobster-trace: LRM.Import_In_Check while not self.peek_eof() and not self.peek_kw("checks"): self.advance() self.skip_until_newline() diff --git a/trlc/trlc.py b/trlc/trlc.py index d1182de2..7cc2c37f 100644 --- a/trlc/trlc.py +++ b/trlc/trlc.py @@ -350,6 +350,7 @@ def parse_rsl_files(self): def parse_check_files(self): # lobster-trace: LRM.Preamble + # lobster-trace: LRM.Check_File ok = True for name in sorted(self.check_files):