remove check files and add new entry in chengelog.md file

bmw-software-engineering · Apr 18, 2024 · b97c618 · b97c618
1 parent 251a430
commit b97c618
Show file tree

Hide file tree

Showing 16 changed files with 8 additions and 6 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -27,6 +27,12 @@ generated in the following situations:
 
 ### 1.2.3-dev
 
+* [LRM, TRLC] Remove checks block in the `.check` files. This
+  means you don't need to have a separate check file, allowing you to
+  implement your checks in `.rsl` file.
+
+* [TRLC] Remove deprecated feature in check files.
+
 * [TRLC] The deprecated builtin function syntax `trlc:foo` has been
   removed. You should now use `foo` instead.
 
@@ -67,6 +73,7 @@ generated in the following situations:
 * [TRLC] Fix a bug in the verifier mistranslating existential
   quantifiers. This could both lead to false alarms and missed bugs.
 
+
 ### 1.2.2
 
 * [API] Add callbacks to the

diff --git a/...bt-cannot-declare-in-check-file/foo.check → ...em/cannot-declare-in-check-file/foo.check b/...bt-cannot-declare-in-check-file/foo.check → ...em/cannot-declare-in-check-file/foo.check
diff --git a/...m/rbt-cannot-declare-in-check-file/output → ...ystem/cannot-declare-in-check-file/output b/...m/rbt-cannot-declare-in-check-file/output → ...ystem/cannot-declare-in-check-file/output
diff --git a/...cannot-declare-in-check-file/output.brief → ...cannot-declare-in-check-file/output.brief b/...cannot-declare-in-check-file/output.brief → ...cannot-declare-in-check-file/output.brief
diff --git a/...-cannot-declare-in-check-file/output.json → .../cannot-declare-in-check-file/output.json b/...-cannot-declare-in-check-file/output.json → .../cannot-declare-in-check-file/output.json
diff --git a/...annot-declare-in-check-file/output.smtlib → ...annot-declare-in-check-file/output.smtlib b/...annot-declare-in-check-file/output.smtlib → ...annot-declare-in-check-file/output.smtlib
diff --git a/tests-system/rbt-import-in-check/bar.rsl → tests-system/import-in-check/bar.rsl b/tests-system/rbt-import-in-check/bar.rsl → tests-system/import-in-check/bar.rsl
diff --git a/tests-system/rbt-import-in-check/foo.check → tests-system/import-in-check/foo.check b/tests-system/rbt-import-in-check/foo.check → tests-system/import-in-check/foo.check
diff --git a/tests-system/rbt-import-in-check/foo.rsl → tests-system/import-in-check/foo.rsl b/tests-system/rbt-import-in-check/foo.rsl → tests-system/import-in-check/foo.rsl
diff --git a/tests-system/rbt-import-in-check/output → tests-system/import-in-check/output b/tests-system/rbt-import-in-check/output → tests-system/import-in-check/output
diff --git a/...s-system/rbt-import-in-check/output.brief → tests-system/import-in-check/output.brief b/...s-system/rbt-import-in-check/output.brief → tests-system/import-in-check/output.brief
diff --git a/tests-system/rbt-import-in-check/output.json → tests-system/import-in-check/output.json b/tests-system/rbt-import-in-check/output.json → tests-system/import-in-check/output.json
diff --git a/...-system/rbt-import-in-check/output.smtlib → tests-system/import-in-check/output.smtlib b/...-system/rbt-import-in-check/output.smtlib → tests-system/import-in-check/output.smtlib
diff --git a/tests-system/simple/tracing b/tests-system/simple/tracing
@@ -2,7 +2,4 @@ LRM.Layout
 LRM.File_Parsing_Order
 LRM.Preamble
 LRM.RSL_File
-LRM.Check_File
-LRM.Deprecated_Check_Files
-LRM.Check_Block
 LRM.TRLC_File
diff --git a/trlc/ast.py b/trlc/ast.py
@@ -280,7 +280,6 @@ def is_visible(self, n_pkg):
 
     def add_item(self, node):
         # lobster-trace: LRM.RSL_File
-        # lobster-trace: LRM.Check_File
         # lobster-trace: LRM.TRLC_File
         assert isinstance(node, (Concrete_Type,
                                  Check_Block,

diff --git a/trlc/parser.py b/trlc/parser.py
@@ -1807,10 +1807,9 @@ def parse_trlc_entry(self):
             self.cu.add_item(self.parse_record_object_declaration())
 
     def parse_preamble(self, kind):
-        assert kind in ("rsl", "check", "trlc")
+        assert kind in ("rsl", "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