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 0000000..960d84c --- /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 0000000..335f683 --- /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 820e86c..25e9fd1 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 3139113..0f9484d 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 820e86c..25e9fd1 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 0000000..2d163bf --- /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 0000000..db0ae8b --- /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 0000000..d39afae --- /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 0000000..d19bc5b --- /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 0000000..d39afae --- /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 0000000..d39afae --- /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 0000000..2d163bf --- /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 0000000..7e226ea --- /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 0000000..a36e3ba --- /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 0000000..e69de29 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 0000000..202758f --- /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 0000000..a36e3ba --- /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 0000000..2d163bf --- /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 0000000..68a41a9 --- /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 0000000..a36e3ba --- /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 0000000..e69de29 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 0000000..b2a1efe --- /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 0000000..a36e3ba --- /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 0000000..2d163bf --- /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 0000000..7fc6c1d --- /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 0000000..e329d66 --- /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 0000000..2b95e5d --- /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 0000000..e329d66 --- /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 0000000..e329d66 --- /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 0000000..564790e --- /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 0000000..e8f7fa1 --- /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 0000000..2d163bf --- /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 0000000..af03a28 --- /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 0000000..258ca7e --- /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 0000000..090da49 --- /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 0000000..258ca7e --- /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 0000000..258ca7e --- /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 b0843e7..4dbb005 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 6c0db92..ca954a4 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):