From 9656026ac991f8c62c535209d7879caf61d09101 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Christoph=20Kl=C3=B6ffel?= <145490354+christophkloeffel@users.noreply.github.com> Date: Thu, 24 Oct 2024 14:54:05 +0200 Subject: [PATCH] adds tracing for markup strings (#67) adds tracing for chapter 19 --- tests-system/lint-ug-examples/div_by_zero.rsl | 13 ++++++++++++ tests-system/lint-ug-examples/options | 1 + tests-system/lint-ug-examples/output | 21 +++---------------- tests-system/lint-ug-examples/output.json | 2 +- tests-system/lint-ug-examples/output.smtlib | 21 +++---------------- tests-system/rbt-markup-string-errors/foo.rsl | 5 +++++ .../rbt-markup-string-errors/foo.trlc | 13 ++++++++++++ tests-system/rbt-markup-string-errors/output | 7 +++++++ .../rbt-markup-string-errors/output.brief | 3 +++ .../rbt-markup-string-errors/output.json | 7 +++++++ .../rbt-markup-string-errors/output.smtlib | 7 +++++++ tests-system/rbt-markup-string-format/foo.rsl | 5 +++++ .../rbt-markup-string-format/foo.trlc | 9 ++++++++ tests-system/rbt-markup-string-format/output | 1 + .../rbt-markup-string-format/output.brief | 0 .../rbt-markup-string-format/output.json | 9 ++++++++ .../rbt-markup-string-format/output.smtlib | 1 + .../foo.rsl | 5 +++++ .../foo.trlc | 13 ++++++++++++ .../output | 1 + .../output.brief | 0 .../output.json | 12 +++++++++++ .../output.smtlib | 1 + .../rbt-markup-string-resolution/foo.rsl | 5 +++++ .../rbt-markup-string-resolution/foo.trlc | 5 +++++ .../rbt-markup-string-resolution/output | 3 +++ .../rbt-markup-string-resolution/output.brief | 1 + .../rbt-markup-string-resolution/output.json | 3 +++ .../output.smtlib | 3 +++ .../rbt-markup-string-resolution/potato.rsl | 5 +++++ .../rbt-markup-string-resolution/potato.trlc | 5 +++++ tests-system/rbt-markup-string-types/foo.rsl | 5 +++++ tests-system/rbt-markup-string-types/foo.trlc | 9 ++++++++ tests-system/rbt-markup-string-types/output | 3 +++ .../rbt-markup-string-types/output.brief | 1 + .../rbt-markup-string-types/output.json | 3 +++ .../rbt-markup-string-types/output.smtlib | 3 +++ trlc/parser.py | 7 +++++++ trlc/trlc.py | 1 + 39 files changed, 182 insertions(+), 37 deletions(-) create mode 100644 tests-system/lint-ug-examples/div_by_zero.rsl create mode 100644 tests-system/lint-ug-examples/options create mode 100644 tests-system/rbt-markup-string-errors/foo.rsl create mode 100644 tests-system/rbt-markup-string-errors/foo.trlc create mode 100644 tests-system/rbt-markup-string-errors/output create mode 100644 tests-system/rbt-markup-string-errors/output.brief create mode 100644 tests-system/rbt-markup-string-errors/output.json create mode 100644 tests-system/rbt-markup-string-errors/output.smtlib create mode 100644 tests-system/rbt-markup-string-format/foo.rsl create mode 100644 tests-system/rbt-markup-string-format/foo.trlc create mode 100644 tests-system/rbt-markup-string-format/output create mode 100644 tests-system/rbt-markup-string-format/output.brief create mode 100644 tests-system/rbt-markup-string-format/output.json create mode 100644 tests-system/rbt-markup-string-format/output.smtlib create mode 100644 tests-system/rbt-markup-string-late-reference-resolution/foo.rsl create mode 100644 tests-system/rbt-markup-string-late-reference-resolution/foo.trlc create mode 100644 tests-system/rbt-markup-string-late-reference-resolution/output create mode 100644 tests-system/rbt-markup-string-late-reference-resolution/output.brief create mode 100644 tests-system/rbt-markup-string-late-reference-resolution/output.json create mode 100644 tests-system/rbt-markup-string-late-reference-resolution/output.smtlib create mode 100644 tests-system/rbt-markup-string-resolution/foo.rsl create mode 100644 tests-system/rbt-markup-string-resolution/foo.trlc create mode 100644 tests-system/rbt-markup-string-resolution/output create mode 100644 tests-system/rbt-markup-string-resolution/output.brief create mode 100644 tests-system/rbt-markup-string-resolution/output.json create mode 100644 tests-system/rbt-markup-string-resolution/output.smtlib create mode 100644 tests-system/rbt-markup-string-resolution/potato.rsl create mode 100644 tests-system/rbt-markup-string-resolution/potato.trlc create mode 100644 tests-system/rbt-markup-string-types/foo.rsl create mode 100644 tests-system/rbt-markup-string-types/foo.trlc create mode 100644 tests-system/rbt-markup-string-types/output create mode 100644 tests-system/rbt-markup-string-types/output.brief create mode 100644 tests-system/rbt-markup-string-types/output.json create mode 100644 tests-system/rbt-markup-string-types/output.smtlib diff --git a/tests-system/lint-ug-examples/div_by_zero.rsl b/tests-system/lint-ug-examples/div_by_zero.rsl new file mode 100644 index 00000000..960d84c3 --- /dev/null +++ b/tests-system/lint-ug-examples/div_by_zero.rsl @@ -0,0 +1,13 @@ +package Div_By_Zero + +type T { + x Integer + y Integer +} + +checks T { + x > 2, fatal "x too small" + y > 2, fatal "y too small" + + 100 / (111 - x * y) > 0, "example" +} diff --git a/tests-system/lint-ug-examples/options b/tests-system/lint-ug-examples/options new file mode 100644 index 00000000..335f6839 --- /dev/null +++ b/tests-system/lint-ug-examples/options @@ -0,0 +1 @@ +--no-detailed-info diff --git a/tests-system/lint-ug-examples/output b/tests-system/lint-ug-examples/output index 820e86cc..25e9fd16 100644 --- a/tests-system/lint-ug-examples/output +++ b/tests-system/lint-ug-examples/output @@ -1,40 +1,25 @@ type Q extends T { ^ lint-ug-examples/clarify_final.rsl:7: issue: consider clarifying that this record is final [clarify_final] - | Parent record Clarify_Final.T is final, making this record - | also final. Marking it explicitly as final - | clarifies this to casual readers. -x / 3 < 0, "non-obvious meaning" ^ lint-ug-examples/unary_minus_precedence.rsl:8: issue: expression means -(x / 3), place explicit brackets to clarify intent [unary_minus_precedence] description != null, "description cannot be empty" ^^ lint-ug-examples/always_true.rsl:12: issue: expression is always true [vcg-always-true] len(x) >= 3 implies x[3] > 0, "too small" ^ lint-ug-examples/array_index.rsl:8: issue: array index could be larger than len(x) [vcg-array-index] - | example record_type triggering error: - | T bad_potato { - | x = [1, 1, 1] - | } +100 / (111 - x * y) > 0, "example" + ^ lint-ug-examples/div_by_zero.rsl:12: issue: divisor could be 0 [vcg-div-by-zero] len(description) >= 10, "too short" ^^^^^^^^^^^ lint-ug-examples/evaluation_of_null.rsl:8: issue: expression could be null [vcg-evaluation-of-null] - | example record_type triggering error: - | Requirement bad_potato { - | /* description is null */ - | } x Integer [10 .. 3] ^ lint-ug-examples/impossible_array_types.rsl:4: issue: upper bound must be at least 10 [impossible_array_types] y Integer [0 .. 0] ^ lint-ug-examples/impossible_array_types.rsl:5: issue: this array makes no sense [impossible_array_types] separator x ^ lint-ug-examples/separator_based_literal_ambiguity.rsl:5: issue: x separator after integer component creates ambiguities [separator_based_literal_ambiguity] - | For example 0x100 would be a base 16 literal - | instead of the tuple segment 0 x 100. x Integer [1 .. 1] ^ lint-ug-examples/weird_array_types.rsl:4: issue: array of fixed size 1 should not be an array [weird_array_types] - | An array with a fixed size of 1 should not - | be an array at all. y Integer [0 .. 1] ^ lint-ug-examples/weird_array_types.rsl:5: issue: consider making this array an optional Integer [weird_array_types] - | An array with 0 to 1 components should just - | be an optional Integer instead. abstract type T { ^ lint-ug-examples/abstract_leaf_types.rsl:3: issue: abstract type T does not have any extensions [abstract_leaf_types] -Processed 13 models and 0 requirement files and found 11 warnings +Processed 14 models and 0 requirement files and found 12 warnings diff --git a/tests-system/lint-ug-examples/output.json b/tests-system/lint-ug-examples/output.json index 31391131..0f9484da 100644 --- a/tests-system/lint-ug-examples/output.json +++ b/tests-system/lint-ug-examples/output.json @@ -1,2 +1,2 @@ {} -Processed 13 models and 0 requirement files and found no issues +Processed 14 models and 0 requirement files and found no issues diff --git a/tests-system/lint-ug-examples/output.smtlib b/tests-system/lint-ug-examples/output.smtlib index 820e86cc..25e9fd16 100644 --- a/tests-system/lint-ug-examples/output.smtlib +++ b/tests-system/lint-ug-examples/output.smtlib @@ -1,40 +1,25 @@ type Q extends T { ^ lint-ug-examples/clarify_final.rsl:7: issue: consider clarifying that this record is final [clarify_final] - | Parent record Clarify_Final.T is final, making this record - | also final. Marking it explicitly as final - | clarifies this to casual readers. -x / 3 < 0, "non-obvious meaning" ^ lint-ug-examples/unary_minus_precedence.rsl:8: issue: expression means -(x / 3), place explicit brackets to clarify intent [unary_minus_precedence] description != null, "description cannot be empty" ^^ lint-ug-examples/always_true.rsl:12: issue: expression is always true [vcg-always-true] len(x) >= 3 implies x[3] > 0, "too small" ^ lint-ug-examples/array_index.rsl:8: issue: array index could be larger than len(x) [vcg-array-index] - | example record_type triggering error: - | T bad_potato { - | x = [1, 1, 1] - | } +100 / (111 - x * y) > 0, "example" + ^ lint-ug-examples/div_by_zero.rsl:12: issue: divisor could be 0 [vcg-div-by-zero] len(description) >= 10, "too short" ^^^^^^^^^^^ lint-ug-examples/evaluation_of_null.rsl:8: issue: expression could be null [vcg-evaluation-of-null] - | example record_type triggering error: - | Requirement bad_potato { - | /* description is null */ - | } x Integer [10 .. 3] ^ lint-ug-examples/impossible_array_types.rsl:4: issue: upper bound must be at least 10 [impossible_array_types] y Integer [0 .. 0] ^ lint-ug-examples/impossible_array_types.rsl:5: issue: this array makes no sense [impossible_array_types] separator x ^ lint-ug-examples/separator_based_literal_ambiguity.rsl:5: issue: x separator after integer component creates ambiguities [separator_based_literal_ambiguity] - | For example 0x100 would be a base 16 literal - | instead of the tuple segment 0 x 100. x Integer [1 .. 1] ^ lint-ug-examples/weird_array_types.rsl:4: issue: array of fixed size 1 should not be an array [weird_array_types] - | An array with a fixed size of 1 should not - | be an array at all. y Integer [0 .. 1] ^ lint-ug-examples/weird_array_types.rsl:5: issue: consider making this array an optional Integer [weird_array_types] - | An array with 0 to 1 components should just - | be an optional Integer instead. abstract type T { ^ lint-ug-examples/abstract_leaf_types.rsl:3: issue: abstract type T does not have any extensions [abstract_leaf_types] -Processed 13 models and 0 requirement files and found 11 warnings +Processed 14 models and 0 requirement files and found 12 warnings diff --git a/tests-system/rbt-markup-string-errors/foo.rsl b/tests-system/rbt-markup-string-errors/foo.rsl new file mode 100644 index 00000000..2d163bfe --- /dev/null +++ b/tests-system/rbt-markup-string-errors/foo.rsl @@ -0,0 +1,5 @@ +package Foo + +type T { + a Markup_String +} diff --git a/tests-system/rbt-markup-string-errors/foo.trlc b/tests-system/rbt-markup-string-errors/foo.trlc new file mode 100644 index 00000000..db0ae8bf --- /dev/null +++ b/tests-system/rbt-markup-string-errors/foo.trlc @@ -0,0 +1,13 @@ +package Foo + +T Bar { + a = "[[Bar" +} + +T But { + a = "But]]" +} + +T Baz { + a = "[[Baz[[But]]]]" +} diff --git a/tests-system/rbt-markup-string-errors/output b/tests-system/rbt-markup-string-errors/output new file mode 100644 index 00000000..d39afaed --- /dev/null +++ b/tests-system/rbt-markup-string-errors/output @@ -0,0 +1,7 @@ +a = "[[Bar" + ^^^ rbt-markup-string-errors/foo.trlc:4: error: expected ]], encountered end-of-string instead +a = "But]]" + ^^ rbt-markup-string-errors/foo.trlc:8: error: opening [[ for this ]] found +a = "[[Baz[[But]]]]" + ^^ rbt-markup-string-errors/foo.trlc:12: error: cannot nest reference lists +Processed 1 model and 1 requirement file and found 3 errors diff --git a/tests-system/rbt-markup-string-errors/output.brief b/tests-system/rbt-markup-string-errors/output.brief new file mode 100644 index 00000000..d19bc5b4 --- /dev/null +++ b/tests-system/rbt-markup-string-errors/output.brief @@ -0,0 +1,3 @@ +rbt-markup-string-errors/foo.trlc:4:12: trlc error: expected ]], encountered end-of-string instead +rbt-markup-string-errors/foo.trlc:8:13: trlc error: opening [[ for this ]] found +rbt-markup-string-errors/foo.trlc:12:15: trlc error: cannot nest reference lists diff --git a/tests-system/rbt-markup-string-errors/output.json b/tests-system/rbt-markup-string-errors/output.json new file mode 100644 index 00000000..d39afaed --- /dev/null +++ b/tests-system/rbt-markup-string-errors/output.json @@ -0,0 +1,7 @@ +a = "[[Bar" + ^^^ rbt-markup-string-errors/foo.trlc:4: error: expected ]], encountered end-of-string instead +a = "But]]" + ^^ rbt-markup-string-errors/foo.trlc:8: error: opening [[ for this ]] found +a = "[[Baz[[But]]]]" + ^^ rbt-markup-string-errors/foo.trlc:12: error: cannot nest reference lists +Processed 1 model and 1 requirement file and found 3 errors diff --git a/tests-system/rbt-markup-string-errors/output.smtlib b/tests-system/rbt-markup-string-errors/output.smtlib new file mode 100644 index 00000000..d39afaed --- /dev/null +++ b/tests-system/rbt-markup-string-errors/output.smtlib @@ -0,0 +1,7 @@ +a = "[[Bar" + ^^^ rbt-markup-string-errors/foo.trlc:4: error: expected ]], encountered end-of-string instead +a = "But]]" + ^^ rbt-markup-string-errors/foo.trlc:8: error: opening [[ for this ]] found +a = "[[Baz[[But]]]]" + ^^ rbt-markup-string-errors/foo.trlc:12: error: cannot nest reference lists +Processed 1 model and 1 requirement file and found 3 errors diff --git a/tests-system/rbt-markup-string-format/foo.rsl b/tests-system/rbt-markup-string-format/foo.rsl new file mode 100644 index 00000000..2d163bfe --- /dev/null +++ b/tests-system/rbt-markup-string-format/foo.rsl @@ -0,0 +1,5 @@ +package Foo + +type T { + a Markup_String +} diff --git a/tests-system/rbt-markup-string-format/foo.trlc b/tests-system/rbt-markup-string-format/foo.trlc new file mode 100644 index 00000000..7e226ead --- /dev/null +++ b/tests-system/rbt-markup-string-format/foo.trlc @@ -0,0 +1,9 @@ +package Foo + +T Bar { + a = "bar [[Inline]]" +} + +T Inline { + a = "inline" +} diff --git a/tests-system/rbt-markup-string-format/output b/tests-system/rbt-markup-string-format/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-markup-string-format/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-markup-string-format/output.brief b/tests-system/rbt-markup-string-format/output.brief new file mode 100644 index 00000000..e69de29b diff --git a/tests-system/rbt-markup-string-format/output.json b/tests-system/rbt-markup-string-format/output.json new file mode 100644 index 00000000..202758fd --- /dev/null +++ b/tests-system/rbt-markup-string-format/output.json @@ -0,0 +1,9 @@ +{ + "Bar": { + "a": "bar [[Inline]]" + }, + "Inline": { + "a": "inline" + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-markup-string-format/output.smtlib b/tests-system/rbt-markup-string-format/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-markup-string-format/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-markup-string-late-reference-resolution/foo.rsl b/tests-system/rbt-markup-string-late-reference-resolution/foo.rsl new file mode 100644 index 00000000..2d163bfe --- /dev/null +++ b/tests-system/rbt-markup-string-late-reference-resolution/foo.rsl @@ -0,0 +1,5 @@ +package Foo + +type T { + a Markup_String +} diff --git a/tests-system/rbt-markup-string-late-reference-resolution/foo.trlc b/tests-system/rbt-markup-string-late-reference-resolution/foo.trlc new file mode 100644 index 00000000..68a41a99 --- /dev/null +++ b/tests-system/rbt-markup-string-late-reference-resolution/foo.trlc @@ -0,0 +1,13 @@ +package Foo + +T Bar { + a = "[[Bar]]" +} + +T But { + a = "[[Baz]]" +} + +T Baz { + a = "[[Baz]]" +} diff --git a/tests-system/rbt-markup-string-late-reference-resolution/output b/tests-system/rbt-markup-string-late-reference-resolution/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-markup-string-late-reference-resolution/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-markup-string-late-reference-resolution/output.brief b/tests-system/rbt-markup-string-late-reference-resolution/output.brief new file mode 100644 index 00000000..e69de29b diff --git a/tests-system/rbt-markup-string-late-reference-resolution/output.json b/tests-system/rbt-markup-string-late-reference-resolution/output.json new file mode 100644 index 00000000..b2a1efe5 --- /dev/null +++ b/tests-system/rbt-markup-string-late-reference-resolution/output.json @@ -0,0 +1,12 @@ +{ + "Bar": { + "a": "[[Bar]]" + }, + "Baz": { + "a": "[[Baz]]" + }, + "But": { + "a": "[[Baz]]" + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-markup-string-late-reference-resolution/output.smtlib b/tests-system/rbt-markup-string-late-reference-resolution/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-markup-string-late-reference-resolution/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-markup-string-resolution/foo.rsl b/tests-system/rbt-markup-string-resolution/foo.rsl new file mode 100644 index 00000000..2d163bfe --- /dev/null +++ b/tests-system/rbt-markup-string-resolution/foo.rsl @@ -0,0 +1,5 @@ +package Foo + +type T { + a Markup_String +} diff --git a/tests-system/rbt-markup-string-resolution/foo.trlc b/tests-system/rbt-markup-string-resolution/foo.trlc new file mode 100644 index 00000000..7fc6c1de --- /dev/null +++ b/tests-system/rbt-markup-string-resolution/foo.trlc @@ -0,0 +1,5 @@ +package Foo + +T Bar { + a = "[[Bar]]" +} diff --git a/tests-system/rbt-markup-string-resolution/output b/tests-system/rbt-markup-string-resolution/output new file mode 100644 index 00000000..e329d66a --- /dev/null +++ b/tests-system/rbt-markup-string-resolution/output @@ -0,0 +1,3 @@ +a = "[[Foo.Bar]]" + ^^^ rbt-markup-string-resolution/potato.trlc:4: error: package must be imported before use +Processed 2 models and 2 requirement files and found 1 error diff --git a/tests-system/rbt-markup-string-resolution/output.brief b/tests-system/rbt-markup-string-resolution/output.brief new file mode 100644 index 00000000..2b95e5d4 --- /dev/null +++ b/tests-system/rbt-markup-string-resolution/output.brief @@ -0,0 +1 @@ +rbt-markup-string-resolution/potato.trlc:4:12: trlc error: package must be imported before use diff --git a/tests-system/rbt-markup-string-resolution/output.json b/tests-system/rbt-markup-string-resolution/output.json new file mode 100644 index 00000000..e329d66a --- /dev/null +++ b/tests-system/rbt-markup-string-resolution/output.json @@ -0,0 +1,3 @@ +a = "[[Foo.Bar]]" + ^^^ rbt-markup-string-resolution/potato.trlc:4: error: package must be imported before use +Processed 2 models and 2 requirement files and found 1 error diff --git a/tests-system/rbt-markup-string-resolution/output.smtlib b/tests-system/rbt-markup-string-resolution/output.smtlib new file mode 100644 index 00000000..e329d66a --- /dev/null +++ b/tests-system/rbt-markup-string-resolution/output.smtlib @@ -0,0 +1,3 @@ +a = "[[Foo.Bar]]" + ^^^ rbt-markup-string-resolution/potato.trlc:4: error: package must be imported before use +Processed 2 models and 2 requirement files and found 1 error diff --git a/tests-system/rbt-markup-string-resolution/potato.rsl b/tests-system/rbt-markup-string-resolution/potato.rsl new file mode 100644 index 00000000..564790e2 --- /dev/null +++ b/tests-system/rbt-markup-string-resolution/potato.rsl @@ -0,0 +1,5 @@ +package Potato + +type T { + a Markup_String +} diff --git a/tests-system/rbt-markup-string-resolution/potato.trlc b/tests-system/rbt-markup-string-resolution/potato.trlc new file mode 100644 index 00000000..e8f7fa16 --- /dev/null +++ b/tests-system/rbt-markup-string-resolution/potato.trlc @@ -0,0 +1,5 @@ +package Potato + +T Kitten { + a = "[[Foo.Bar]]" +} diff --git a/tests-system/rbt-markup-string-types/foo.rsl b/tests-system/rbt-markup-string-types/foo.rsl new file mode 100644 index 00000000..2d163bfe --- /dev/null +++ b/tests-system/rbt-markup-string-types/foo.rsl @@ -0,0 +1,5 @@ +package Foo + +type T { + a Markup_String +} diff --git a/tests-system/rbt-markup-string-types/foo.trlc b/tests-system/rbt-markup-string-types/foo.trlc new file mode 100644 index 00000000..af03a287 --- /dev/null +++ b/tests-system/rbt-markup-string-types/foo.trlc @@ -0,0 +1,9 @@ +package Foo + +T Bar { + a = "[[T]]" +} + +T But { + a = "[[But]]" +} diff --git a/tests-system/rbt-markup-string-types/output b/tests-system/rbt-markup-string-types/output new file mode 100644 index 00000000..258ca7eb --- /dev/null +++ b/tests-system/rbt-markup-string-types/output @@ -0,0 +1,3 @@ +a = "[[T]]" + ^ rbt-markup-string-types/foo.trlc:4: error: Record_Type T is not a Record_Object +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-markup-string-types/output.brief b/tests-system/rbt-markup-string-types/output.brief new file mode 100644 index 00000000..090da49c --- /dev/null +++ b/tests-system/rbt-markup-string-types/output.brief @@ -0,0 +1 @@ +rbt-markup-string-types/foo.trlc:4:12: trlc error: Record_Type T is not a Record_Object diff --git a/tests-system/rbt-markup-string-types/output.json b/tests-system/rbt-markup-string-types/output.json new file mode 100644 index 00000000..258ca7eb --- /dev/null +++ b/tests-system/rbt-markup-string-types/output.json @@ -0,0 +1,3 @@ +a = "[[T]]" + ^ rbt-markup-string-types/foo.trlc:4: error: Record_Type T is not a Record_Object +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-markup-string-types/output.smtlib b/tests-system/rbt-markup-string-types/output.smtlib new file mode 100644 index 00000000..258ca7eb --- /dev/null +++ b/tests-system/rbt-markup-string-types/output.smtlib @@ -0,0 +1,3 @@ +a = "[[T]]" + ^ rbt-markup-string-types/foo.trlc:4: error: Record_Type T is not a Record_Object +Processed 1 model and 1 requirement file and found 1 error diff --git a/trlc/parser.py b/trlc/parser.py index b0843e7e..4dbb0055 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -27,6 +27,8 @@ class Markup_Token(Token_Base): + # lobster-trace: LRM.Markup_String_Format + KIND = { "CHARACTER" : "character", "REFLIST_BEGIN" : "[[", @@ -51,6 +53,8 @@ def file_location(self): return self.origin_location def token(self): + # lobster-trace: LRM.Markup_String_Errors + if self.in_reflist: self.skip_whitespace() else: @@ -249,6 +253,9 @@ def parse_qualified_name(self): # lobster-trace: LRM.Qualified_Name # lobster-trace: LRM.Valid_Qualifier # lobster-trace: LRM.Valid_Name + # lobster-trace: LRM.Markup_String_Resolution + # lobster-trace: LRM.Markup_String_Types + self.match("REFLIST_IDENTIFIER") if self.peek("REFLIST_DOT"): package = self.parent.stab.lookup_direct( diff --git a/trlc/trlc.py b/trlc/trlc.py index 6c0db925..ca954a43 100644 --- a/trlc/trlc.py +++ b/trlc/trlc.py @@ -456,6 +456,7 @@ def parse_trlc_files(self): return ok def resolve_record_references(self): + # lobster-trace: LRM.Markup_String_Late_Reference_Resolution # lobster-trace: LRM.Late_Reference_Checking ok = True for package in self.stab.values(ast.Package):