Skip to content

Commit

Permalink
adds tracing for TRLC files
Browse files Browse the repository at this point in the history
  • Loading branch information
christophkloeffel committed Oct 24, 2023
1 parent 405db53 commit 9ace4f5
Show file tree
Hide file tree
Showing 16 changed files with 20 additions and 12 deletions.
2 changes: 1 addition & 1 deletion language-reference-manual/lrm.trlc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 0 additions & 3 deletions tests-system/duplicate-late-packages/output

This file was deleted.

1 change: 0 additions & 1 deletion tests-system/duplicate-late-packages/output.brief

This file was deleted.

4 changes: 0 additions & 4 deletions tests-system/duplicate-late-packages/output.json

This file was deleted.

3 changes: 0 additions & 3 deletions tests-system/duplicate-late-packages/output.smtlib

This file was deleted.

3 changes: 3 additions & 0 deletions tests-system/rbt-late-package-declarations/output
Original file line number Diff line number Diff line change
@@ -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)
1 change: 1 addition & 0 deletions tests-system/rbt-late-package-declarations/output.brief
Original file line number Diff line number Diff line change
@@ -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
4 changes: 4 additions & 0 deletions tests-system/rbt-late-package-declarations/output.json
Original file line number Diff line number Diff line change
@@ -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)
3 changes: 3 additions & 0 deletions tests-system/rbt-late-package-declarations/output.smtlib
Original file line number Diff line number Diff line change
@@ -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)
1 change: 1 addition & 0 deletions tests-system/rbt-late-package-declarations/tracing
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
LRM.Duplicate_Late_Packages
1 change: 1 addition & 0 deletions tests-system/simple/tracing
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,4 @@ LRM.RSL_File
LRM.Check_File
LRM.Deprecated_Check_Files
LRM.Check_Block
LRM.TRLC_File
4 changes: 4 additions & 0 deletions trlc/parser.py
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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:
Expand All @@ -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,"
Expand Down Expand Up @@ -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)

Expand Down
2 changes: 2 additions & 0 deletions trlc/trlc.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 9ace4f5

Please sign in to comment.