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):