From b22befce76db4c992292bc91a82d8af4dd551e98 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Christoph=20Kl=C3=B6ffel?= <145490354+christophkloeffel@users.noreply.github.com> Date: Tue, 15 Oct 2024 13:38:36 +0200 Subject: [PATCH] adds tracing for names (#66) adds tracing for chapter 12 --- language-reference-manual/lrm.trlc | 4 --- tests-system/rbt-endswith-semantics/foo.rsl | 9 ++++++ tests-system/rbt-endswith-semantics/foo.trlc | 5 ++++ tests-system/rbt-endswith-semantics/output | 1 + .../rbt-endswith-semantics/output.brief | 0 .../rbt-endswith-semantics/output.json | 6 ++++ .../rbt-endswith-semantics/output.smtlib | 1 + tests-system/rbt-len-semantics/foo.rsl | 12 ++++++++ tests-system/rbt-len-semantics/foo.trlc | 7 +++++ tests-system/rbt-len-semantics/output | 1 + tests-system/rbt-len-semantics/output.brief | 0 tests-system/rbt-len-semantics/output.json | 11 ++++++++ tests-system/rbt-len-semantics/output.smtlib | 1 + tests-system/rbt-matches-semantics/foo.rsl | 11 ++++++++ tests-system/rbt-matches-semantics/foo.trlc | 7 +++++ tests-system/rbt-matches-semantics/output | 1 + .../rbt-matches-semantics/output.brief | 0 .../rbt-matches-semantics/output.json | 8 ++++++ .../rbt-matches-semantics/output.smtlib | 1 + tests-system/rbt-names/foo.rsl | 25 +++++++++++++++++ tests-system/rbt-names/foo.trlc | 7 +++++ tests-system/rbt-names/output | 3 ++ tests-system/rbt-names/output.brief | 1 + tests-system/rbt-names/output.json | 20 +++++++++++++ tests-system/rbt-names/output.smtlib | 3 ++ tests-system/rbt-signature-len-1/foo.rsl | 12 ++++++++ tests-system/rbt-signature-len-1/output | 3 ++ tests-system/rbt-signature-len-1/output.brief | 1 + tests-system/rbt-signature-len-1/output.json | 3 ++ .../rbt-signature-len-1/output.smtlib | 3 ++ tests-system/rbt-signature-len-2/foo.rsl | 13 +++++++++ tests-system/rbt-signature-len-2/foo.trlc | 7 +++++ tests-system/rbt-signature-len-2/output | 3 ++ tests-system/rbt-signature-len-2/output.brief | 1 + tests-system/rbt-signature-len-2/output.json | 3 ++ .../rbt-signature-len-2/output.smtlib | 3 ++ tests-system/rbt-signature-matches-1/foo.rsl | 11 ++++++++ tests-system/rbt-signature-matches-1/output | 3 ++ .../rbt-signature-matches-1/output.brief | 1 + .../rbt-signature-matches-1/output.json | 3 ++ .../rbt-signature-matches-1/output.smtlib | 3 ++ tests-system/rbt-signature-matches-2/foo.rsl | 11 ++++++++ tests-system/rbt-signature-matches-2/foo.trlc | 7 +++++ tests-system/rbt-signature-matches-2/output | 3 ++ .../rbt-signature-matches-2/output.brief | 1 + .../rbt-signature-matches-2/output.json | 3 ++ .../rbt-signature-matches-2/output.smtlib | 3 ++ tests-system/rbt-signature-matches-3/foo.rsl | 11 ++++++++ tests-system/rbt-signature-matches-3/foo.trlc | 7 +++++ tests-system/rbt-signature-matches-3/output | 3 ++ .../rbt-signature-matches-3/output.brief | 1 + .../rbt-signature-matches-3/output.json | 3 ++ .../rbt-signature-matches-3/output.smtlib | 3 ++ .../foo.rsl | 14 ++++++++++ .../output | 3 ++ .../output.brief | 1 + .../output.json | 3 ++ .../output.smtlib | 3 ++ .../foo.rsl | 14 ++++++++++ .../foo.trlc | 7 +++++ .../output | 3 ++ .../output.brief | 1 + .../output.json | 3 ++ .../output.smtlib | 3 ++ .../rbt-signature-type-conversion/foo.rsl | 11 ++++++++ .../rbt-signature-type-conversion/foo.trlc | 6 ++++ .../rbt-signature-type-conversion/output | 5 ++++ .../output.brief | 2 ++ .../rbt-signature-type-conversion/output.json | 11 ++++++++ .../output.smtlib | 5 ++++ .../rbt-signature-type-conversion/tracing | 2 ++ tests-system/rbt-startswith-semantics/foo.rsl | 9 ++++++ .../rbt-startswith-semantics/foo.trlc | 5 ++++ tests-system/rbt-startswith-semantics/output | 1 + .../rbt-startswith-semantics/output.brief | 0 .../rbt-startswith-semantics/output.json | 6 ++++ .../rbt-startswith-semantics/output.smtlib | 1 + .../rbt-static-regular-expression/foo.rsl | 10 +++++++ .../rbt-static-regular-expression/foo.trlc | 6 ++++ .../rbt-static-regular-expression/output | 3 ++ .../output.brief | 1 + .../rbt-static-regular-expression/output.json | 3 ++ .../output.smtlib | 3 ++ .../rbt-valid-access-prefixes/foo.rsl | 22 +++++++++++++++ .../rbt-valid-access-prefixes/foo.trlc | 6 ++++ tests-system/rbt-valid-access-prefixes/output | 5 ++++ .../rbt-valid-access-prefixes/output.brief | 2 ++ .../rbt-valid-access-prefixes/output.json | 5 ++++ .../rbt-valid-access-prefixes/output.smtlib | 5 ++++ tests-system/rbt-valid-base-names/bar.rsl | 5 ++++ tests-system/rbt-valid-base-names/foo.rsl | 5 ++++ tests-system/rbt-valid-base-names/foo.trlc | 10 +++++++ tests-system/rbt-valid-base-names/output | 3 ++ .../rbt-valid-base-names/output.brief | 1 + tests-system/rbt-valid-base-names/output.json | 3 ++ .../rbt-valid-base-names/output.smtlib | 3 ++ .../rbt-valid-function-prefixes/foo.rsl | 11 ++++++++ .../rbt-valid-function-prefixes/output | 3 ++ .../rbt-valid-function-prefixes/output.brief | 1 + .../rbt-valid-function-prefixes/output.json | 3 ++ .../rbt-valid-function-prefixes/output.smtlib | 3 ++ tests-system/rbt-valid-index-prefixes/foo.rsl | 10 +++++++ tests-system/rbt-valid-index-prefixes/output | 3 ++ .../rbt-valid-index-prefixes/output.brief | 1 + .../rbt-valid-index-prefixes/output.json | 3 ++ .../rbt-valid-index-prefixes/output.smtlib | 3 ++ trlc/ast.py | 28 +++++++++++++++++++ trlc/parser.py | 5 ++++ 108 files changed, 564 insertions(+), 4 deletions(-) create mode 100644 tests-system/rbt-endswith-semantics/foo.rsl create mode 100644 tests-system/rbt-endswith-semantics/foo.trlc create mode 100644 tests-system/rbt-endswith-semantics/output create mode 100644 tests-system/rbt-endswith-semantics/output.brief create mode 100644 tests-system/rbt-endswith-semantics/output.json create mode 100644 tests-system/rbt-endswith-semantics/output.smtlib create mode 100644 tests-system/rbt-len-semantics/foo.rsl create mode 100644 tests-system/rbt-len-semantics/foo.trlc create mode 100644 tests-system/rbt-len-semantics/output create mode 100644 tests-system/rbt-len-semantics/output.brief create mode 100644 tests-system/rbt-len-semantics/output.json create mode 100644 tests-system/rbt-len-semantics/output.smtlib create mode 100644 tests-system/rbt-matches-semantics/foo.rsl create mode 100644 tests-system/rbt-matches-semantics/foo.trlc create mode 100644 tests-system/rbt-matches-semantics/output create mode 100644 tests-system/rbt-matches-semantics/output.brief create mode 100644 tests-system/rbt-matches-semantics/output.json create mode 100644 tests-system/rbt-matches-semantics/output.smtlib create mode 100644 tests-system/rbt-names/foo.rsl create mode 100644 tests-system/rbt-names/foo.trlc create mode 100644 tests-system/rbt-names/output create mode 100644 tests-system/rbt-names/output.brief create mode 100644 tests-system/rbt-names/output.json create mode 100644 tests-system/rbt-names/output.smtlib create mode 100644 tests-system/rbt-signature-len-1/foo.rsl create mode 100644 tests-system/rbt-signature-len-1/output create mode 100644 tests-system/rbt-signature-len-1/output.brief create mode 100644 tests-system/rbt-signature-len-1/output.json create mode 100644 tests-system/rbt-signature-len-1/output.smtlib create mode 100644 tests-system/rbt-signature-len-2/foo.rsl create mode 100644 tests-system/rbt-signature-len-2/foo.trlc create mode 100644 tests-system/rbt-signature-len-2/output create mode 100644 tests-system/rbt-signature-len-2/output.brief create mode 100644 tests-system/rbt-signature-len-2/output.json create mode 100644 tests-system/rbt-signature-len-2/output.smtlib create mode 100644 tests-system/rbt-signature-matches-1/foo.rsl create mode 100644 tests-system/rbt-signature-matches-1/output create mode 100644 tests-system/rbt-signature-matches-1/output.brief create mode 100644 tests-system/rbt-signature-matches-1/output.json create mode 100644 tests-system/rbt-signature-matches-1/output.smtlib create mode 100644 tests-system/rbt-signature-matches-2/foo.rsl create mode 100644 tests-system/rbt-signature-matches-2/foo.trlc create mode 100644 tests-system/rbt-signature-matches-2/output create mode 100644 tests-system/rbt-signature-matches-2/output.brief create mode 100644 tests-system/rbt-signature-matches-2/output.json create mode 100644 tests-system/rbt-signature-matches-2/output.smtlib create mode 100644 tests-system/rbt-signature-matches-3/foo.rsl create mode 100644 tests-system/rbt-signature-matches-3/foo.trlc create mode 100644 tests-system/rbt-signature-matches-3/output create mode 100644 tests-system/rbt-signature-matches-3/output.brief create mode 100644 tests-system/rbt-signature-matches-3/output.json create mode 100644 tests-system/rbt-signature-matches-3/output.smtlib create mode 100644 tests-system/rbt-signature-string-end-functions-1/foo.rsl create mode 100644 tests-system/rbt-signature-string-end-functions-1/output create mode 100644 tests-system/rbt-signature-string-end-functions-1/output.brief create mode 100644 tests-system/rbt-signature-string-end-functions-1/output.json create mode 100644 tests-system/rbt-signature-string-end-functions-1/output.smtlib create mode 100644 tests-system/rbt-signature-string-end-functions-2/foo.rsl create mode 100644 tests-system/rbt-signature-string-end-functions-2/foo.trlc create mode 100644 tests-system/rbt-signature-string-end-functions-2/output create mode 100644 tests-system/rbt-signature-string-end-functions-2/output.brief create mode 100644 tests-system/rbt-signature-string-end-functions-2/output.json create mode 100644 tests-system/rbt-signature-string-end-functions-2/output.smtlib create mode 100644 tests-system/rbt-signature-type-conversion/foo.rsl create mode 100644 tests-system/rbt-signature-type-conversion/foo.trlc create mode 100644 tests-system/rbt-signature-type-conversion/output create mode 100644 tests-system/rbt-signature-type-conversion/output.brief create mode 100644 tests-system/rbt-signature-type-conversion/output.json create mode 100644 tests-system/rbt-signature-type-conversion/output.smtlib create mode 100644 tests-system/rbt-signature-type-conversion/tracing create mode 100644 tests-system/rbt-startswith-semantics/foo.rsl create mode 100644 tests-system/rbt-startswith-semantics/foo.trlc create mode 100644 tests-system/rbt-startswith-semantics/output create mode 100644 tests-system/rbt-startswith-semantics/output.brief create mode 100644 tests-system/rbt-startswith-semantics/output.json create mode 100644 tests-system/rbt-startswith-semantics/output.smtlib create mode 100644 tests-system/rbt-static-regular-expression/foo.rsl create mode 100644 tests-system/rbt-static-regular-expression/foo.trlc create mode 100644 tests-system/rbt-static-regular-expression/output create mode 100644 tests-system/rbt-static-regular-expression/output.brief create mode 100644 tests-system/rbt-static-regular-expression/output.json create mode 100644 tests-system/rbt-static-regular-expression/output.smtlib create mode 100644 tests-system/rbt-valid-access-prefixes/foo.rsl create mode 100644 tests-system/rbt-valid-access-prefixes/foo.trlc create mode 100644 tests-system/rbt-valid-access-prefixes/output create mode 100644 tests-system/rbt-valid-access-prefixes/output.brief create mode 100644 tests-system/rbt-valid-access-prefixes/output.json create mode 100644 tests-system/rbt-valid-access-prefixes/output.smtlib create mode 100644 tests-system/rbt-valid-base-names/bar.rsl create mode 100644 tests-system/rbt-valid-base-names/foo.rsl create mode 100644 tests-system/rbt-valid-base-names/foo.trlc create mode 100644 tests-system/rbt-valid-base-names/output create mode 100644 tests-system/rbt-valid-base-names/output.brief create mode 100644 tests-system/rbt-valid-base-names/output.json create mode 100644 tests-system/rbt-valid-base-names/output.smtlib create mode 100644 tests-system/rbt-valid-function-prefixes/foo.rsl create mode 100644 tests-system/rbt-valid-function-prefixes/output create mode 100644 tests-system/rbt-valid-function-prefixes/output.brief create mode 100644 tests-system/rbt-valid-function-prefixes/output.json create mode 100644 tests-system/rbt-valid-function-prefixes/output.smtlib create mode 100644 tests-system/rbt-valid-index-prefixes/foo.rsl create mode 100644 tests-system/rbt-valid-index-prefixes/output create mode 100644 tests-system/rbt-valid-index-prefixes/output.brief create mode 100644 tests-system/rbt-valid-index-prefixes/output.json create mode 100644 tests-system/rbt-valid-index-prefixes/output.smtlib diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index 3b8cb68d..9cc18123 100644 --- a/language-reference-manual/lrm.trlc +++ b/language-reference-manual/lrm.trlc @@ -1188,10 +1188,6 @@ section "Names" { the given integer to the exact same rational.''' } - Name_Resolution Case_Sensitive { - text = '''Name resolution is case sensitive.''' - } - Example Name_Examples { hidden_rsl = ''' package Example diff --git a/tests-system/rbt-endswith-semantics/foo.rsl b/tests-system/rbt-endswith-semantics/foo.rsl new file mode 100644 index 00000000..7a21f1f8 --- /dev/null +++ b/tests-system/rbt-endswith-semantics/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type T { + b String +} + +checks T { + endswith(b, "en"), warning "b should end with en", b +} diff --git a/tests-system/rbt-endswith-semantics/foo.trlc b/tests-system/rbt-endswith-semantics/foo.trlc new file mode 100644 index 00000000..5013e982 --- /dev/null +++ b/tests-system/rbt-endswith-semantics/foo.trlc @@ -0,0 +1,5 @@ +package Foo + +T Bar { + b = "kitten" +} diff --git a/tests-system/rbt-endswith-semantics/output b/tests-system/rbt-endswith-semantics/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-endswith-semantics/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-endswith-semantics/output.brief b/tests-system/rbt-endswith-semantics/output.brief new file mode 100644 index 00000000..e69de29b diff --git a/tests-system/rbt-endswith-semantics/output.json b/tests-system/rbt-endswith-semantics/output.json new file mode 100644 index 00000000..37f5ecfc --- /dev/null +++ b/tests-system/rbt-endswith-semantics/output.json @@ -0,0 +1,6 @@ +{ + "Bar": { + "b": "kitten" + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-endswith-semantics/output.smtlib b/tests-system/rbt-endswith-semantics/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-endswith-semantics/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-len-semantics/foo.rsl b/tests-system/rbt-len-semantics/foo.rsl new file mode 100644 index 00000000..ea052081 --- /dev/null +++ b/tests-system/rbt-len-semantics/foo.rsl @@ -0,0 +1,12 @@ +package Foo + +type T { + a String + b Integer + c Integer[1..*] +} + +checks T { + len(a) == 6, "not true" + len(c) == 2, "not true" +} diff --git a/tests-system/rbt-len-semantics/foo.trlc b/tests-system/rbt-len-semantics/foo.trlc new file mode 100644 index 00000000..f3bd6ce1 --- /dev/null +++ b/tests-system/rbt-len-semantics/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Bar { + a = "potato" + b = 1 + c = [2,1] +} diff --git a/tests-system/rbt-len-semantics/output b/tests-system/rbt-len-semantics/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-len-semantics/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-len-semantics/output.brief b/tests-system/rbt-len-semantics/output.brief new file mode 100644 index 00000000..e69de29b diff --git a/tests-system/rbt-len-semantics/output.json b/tests-system/rbt-len-semantics/output.json new file mode 100644 index 00000000..fa391476 --- /dev/null +++ b/tests-system/rbt-len-semantics/output.json @@ -0,0 +1,11 @@ +{ + "Bar": { + "a": "potato", + "b": 1, + "c": [ + 2, + 1 + ] + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-len-semantics/output.smtlib b/tests-system/rbt-len-semantics/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-len-semantics/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-matches-semantics/foo.rsl b/tests-system/rbt-matches-semantics/foo.rsl new file mode 100644 index 00000000..aac4b3bc --- /dev/null +++ b/tests-system/rbt-matches-semantics/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + a String + b String + c Integer +} + +checks T { + matches(a, "potato"), warning "a should match with potato", a +} diff --git a/tests-system/rbt-matches-semantics/foo.trlc b/tests-system/rbt-matches-semantics/foo.trlc new file mode 100644 index 00000000..71700516 --- /dev/null +++ b/tests-system/rbt-matches-semantics/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Bar { + a = "potato" + b = "kitten" + c = 1 +} diff --git a/tests-system/rbt-matches-semantics/output b/tests-system/rbt-matches-semantics/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-matches-semantics/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-matches-semantics/output.brief b/tests-system/rbt-matches-semantics/output.brief new file mode 100644 index 00000000..e69de29b diff --git a/tests-system/rbt-matches-semantics/output.json b/tests-system/rbt-matches-semantics/output.json new file mode 100644 index 00000000..4d25cf13 --- /dev/null +++ b/tests-system/rbt-matches-semantics/output.json @@ -0,0 +1,8 @@ +{ + "Bar": { + "a": "potato", + "b": "kitten", + "c": 1 + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-matches-semantics/output.smtlib b/tests-system/rbt-matches-semantics/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-matches-semantics/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-names/foo.rsl b/tests-system/rbt-names/foo.rsl new file mode 100644 index 00000000..068f861d --- /dev/null +++ b/tests-system/rbt-names/foo.rsl @@ -0,0 +1,25 @@ +package Foo + +enum E { + A + B + C +} + +tuple T { + first Integer + separator @ + second Integer +} + +type Bar { + e E + b Integer[2..*] + t T +} + +checks Bar { + len(b) < 5, warning "try to minimize the length", b + b[0]+b[1] != 0, error "sum of first two elements must not be zero", b + t.first + t.second != 0, error "the sum of the versions must not be zero", t +} diff --git a/tests-system/rbt-names/foo.trlc b/tests-system/rbt-names/foo.trlc new file mode 100644 index 00000000..7ccc1a1d --- /dev/null +++ b/tests-system/rbt-names/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +Bar potato { + e = E.A + t = 1@2 + b = [1,2,3,4,5,6] +} diff --git a/tests-system/rbt-names/output b/tests-system/rbt-names/output new file mode 100644 index 00000000..ffb91253 --- /dev/null +++ b/tests-system/rbt-names/output @@ -0,0 +1,3 @@ +b = [1,2,3,4,5,6] + ^ rbt-names/foo.trlc:6: check warning: try to minimize the length +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-names/output.brief b/tests-system/rbt-names/output.brief new file mode 100644 index 00000000..43151939 --- /dev/null +++ b/tests-system/rbt-names/output.brief @@ -0,0 +1 @@ +rbt-names/foo.trlc:6:9: trlc check warning: try to minimize the length diff --git a/tests-system/rbt-names/output.json b/tests-system/rbt-names/output.json new file mode 100644 index 00000000..71268297 --- /dev/null +++ b/tests-system/rbt-names/output.json @@ -0,0 +1,20 @@ +b = [1,2,3,4,5,6] + ^ rbt-names/foo.trlc:6: check warning: try to minimize the length +{ + "potato": { + "b": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "e": "A", + "t": { + "first": 1, + "second": 2 + } + } +} +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-names/output.smtlib b/tests-system/rbt-names/output.smtlib new file mode 100644 index 00000000..ffb91253 --- /dev/null +++ b/tests-system/rbt-names/output.smtlib @@ -0,0 +1,3 @@ +b = [1,2,3,4,5,6] + ^ rbt-names/foo.trlc:6: check warning: try to minimize the length +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-signature-len-1/foo.rsl b/tests-system/rbt-signature-len-1/foo.rsl new file mode 100644 index 00000000..353b0a6d --- /dev/null +++ b/tests-system/rbt-signature-len-1/foo.rsl @@ -0,0 +1,12 @@ +package Foo + +type T { + a String + b Integer + c Integer[1..*] +} + +checks T { + len(a) > 7, "a must be longer than 7" + len(b) > 7, "b must be longer than 7" +} diff --git a/tests-system/rbt-signature-len-1/output b/tests-system/rbt-signature-len-1/output new file mode 100644 index 00000000..c752dc91 --- /dev/null +++ b/tests-system/rbt-signature-len-1/output @@ -0,0 +1,3 @@ +len(b) > 7, "b must be longer than 7" + ^ rbt-signature-len-1/foo.rsl:11: error: expected expression of type Array_Type, got Builtin_Integer instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-signature-len-1/output.brief b/tests-system/rbt-signature-len-1/output.brief new file mode 100644 index 00000000..ec522560 --- /dev/null +++ b/tests-system/rbt-signature-len-1/output.brief @@ -0,0 +1 @@ +rbt-signature-len-1/foo.rsl:11:9: trlc error: expected expression of type Array_Type, got Builtin_Integer instead diff --git a/tests-system/rbt-signature-len-1/output.json b/tests-system/rbt-signature-len-1/output.json new file mode 100644 index 00000000..c752dc91 --- /dev/null +++ b/tests-system/rbt-signature-len-1/output.json @@ -0,0 +1,3 @@ +len(b) > 7, "b must be longer than 7" + ^ rbt-signature-len-1/foo.rsl:11: error: expected expression of type Array_Type, got Builtin_Integer instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-signature-len-1/output.smtlib b/tests-system/rbt-signature-len-1/output.smtlib new file mode 100644 index 00000000..c752dc91 --- /dev/null +++ b/tests-system/rbt-signature-len-1/output.smtlib @@ -0,0 +1,3 @@ +len(b) > 7, "b must be longer than 7" + ^ rbt-signature-len-1/foo.rsl:11: error: expected expression of type Array_Type, got Builtin_Integer instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-signature-len-2/foo.rsl b/tests-system/rbt-signature-len-2/foo.rsl new file mode 100644 index 00000000..af918e07 --- /dev/null +++ b/tests-system/rbt-signature-len-2/foo.rsl @@ -0,0 +1,13 @@ +package Foo + +type T { + a String + b Integer + c Integer[1..*] +} + +checks T { + len(a) > 7, "a must be longer than 7" + len(c) > 7, "b must be longer than 7" + len(a, c) > 7, "a and c must be longer than 7" +} diff --git a/tests-system/rbt-signature-len-2/foo.trlc b/tests-system/rbt-signature-len-2/foo.trlc new file mode 100644 index 00000000..f3bd6ce1 --- /dev/null +++ b/tests-system/rbt-signature-len-2/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Bar { + a = "potato" + b = 1 + c = [2,1] +} diff --git a/tests-system/rbt-signature-len-2/output b/tests-system/rbt-signature-len-2/output new file mode 100644 index 00000000..5a01f12e --- /dev/null +++ b/tests-system/rbt-signature-len-2/output @@ -0,0 +1,3 @@ +len(a, c) > 7, "a and c must be longer than 7" +^^^ rbt-signature-len-2/foo.rsl:12: error: function requires 1 parameters +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-len-2/output.brief b/tests-system/rbt-signature-len-2/output.brief new file mode 100644 index 00000000..58e08a15 --- /dev/null +++ b/tests-system/rbt-signature-len-2/output.brief @@ -0,0 +1 @@ +rbt-signature-len-2/foo.rsl:12:5: trlc error: function requires 1 parameters diff --git a/tests-system/rbt-signature-len-2/output.json b/tests-system/rbt-signature-len-2/output.json new file mode 100644 index 00000000..5a01f12e --- /dev/null +++ b/tests-system/rbt-signature-len-2/output.json @@ -0,0 +1,3 @@ +len(a, c) > 7, "a and c must be longer than 7" +^^^ rbt-signature-len-2/foo.rsl:12: error: function requires 1 parameters +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-len-2/output.smtlib b/tests-system/rbt-signature-len-2/output.smtlib new file mode 100644 index 00000000..5a01f12e --- /dev/null +++ b/tests-system/rbt-signature-len-2/output.smtlib @@ -0,0 +1,3 @@ +len(a, c) > 7, "a and c must be longer than 7" +^^^ rbt-signature-len-2/foo.rsl:12: error: function requires 1 parameters +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-matches-1/foo.rsl b/tests-system/rbt-signature-matches-1/foo.rsl new file mode 100644 index 00000000..abd2d622 --- /dev/null +++ b/tests-system/rbt-signature-matches-1/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + a String + b String + c Integer +} + +checks T { + matches(c, "potato"), warning "a should match with potato", a +} diff --git a/tests-system/rbt-signature-matches-1/output b/tests-system/rbt-signature-matches-1/output new file mode 100644 index 00000000..399804df --- /dev/null +++ b/tests-system/rbt-signature-matches-1/output @@ -0,0 +1,3 @@ +matches(c, "potato"), warning "a should match with potato", a + ^ rbt-signature-matches-1/foo.rsl:10: error: expected expression of type Builtin_String, got Builtin_Integer instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-signature-matches-1/output.brief b/tests-system/rbt-signature-matches-1/output.brief new file mode 100644 index 00000000..97880a4d --- /dev/null +++ b/tests-system/rbt-signature-matches-1/output.brief @@ -0,0 +1 @@ +rbt-signature-matches-1/foo.rsl:10:13: trlc error: expected expression of type Builtin_String, got Builtin_Integer instead diff --git a/tests-system/rbt-signature-matches-1/output.json b/tests-system/rbt-signature-matches-1/output.json new file mode 100644 index 00000000..399804df --- /dev/null +++ b/tests-system/rbt-signature-matches-1/output.json @@ -0,0 +1,3 @@ +matches(c, "potato"), warning "a should match with potato", a + ^ rbt-signature-matches-1/foo.rsl:10: error: expected expression of type Builtin_String, got Builtin_Integer instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-signature-matches-1/output.smtlib b/tests-system/rbt-signature-matches-1/output.smtlib new file mode 100644 index 00000000..399804df --- /dev/null +++ b/tests-system/rbt-signature-matches-1/output.smtlib @@ -0,0 +1,3 @@ +matches(c, "potato"), warning "a should match with potato", a + ^ rbt-signature-matches-1/foo.rsl:10: error: expected expression of type Builtin_String, got Builtin_Integer instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-signature-matches-2/foo.rsl b/tests-system/rbt-signature-matches-2/foo.rsl new file mode 100644 index 00000000..ed1a976f --- /dev/null +++ b/tests-system/rbt-signature-matches-2/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + a String + b String + c Integer +} + +checks T { + matches(a, b, "potato"), warning "a should match with potato", a +} diff --git a/tests-system/rbt-signature-matches-2/foo.trlc b/tests-system/rbt-signature-matches-2/foo.trlc new file mode 100644 index 00000000..71700516 --- /dev/null +++ b/tests-system/rbt-signature-matches-2/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Bar { + a = "potato" + b = "kitten" + c = 1 +} diff --git a/tests-system/rbt-signature-matches-2/output b/tests-system/rbt-signature-matches-2/output new file mode 100644 index 00000000..a31ebfd3 --- /dev/null +++ b/tests-system/rbt-signature-matches-2/output @@ -0,0 +1,3 @@ +matches(a, b, "potato"), warning "a should match with potato", a +^^^^^^^ rbt-signature-matches-2/foo.rsl:10: error: function requires 2 parameters +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-matches-2/output.brief b/tests-system/rbt-signature-matches-2/output.brief new file mode 100644 index 00000000..3d364487 --- /dev/null +++ b/tests-system/rbt-signature-matches-2/output.brief @@ -0,0 +1 @@ +rbt-signature-matches-2/foo.rsl:10:5: trlc error: function requires 2 parameters diff --git a/tests-system/rbt-signature-matches-2/output.json b/tests-system/rbt-signature-matches-2/output.json new file mode 100644 index 00000000..a31ebfd3 --- /dev/null +++ b/tests-system/rbt-signature-matches-2/output.json @@ -0,0 +1,3 @@ +matches(a, b, "potato"), warning "a should match with potato", a +^^^^^^^ rbt-signature-matches-2/foo.rsl:10: error: function requires 2 parameters +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-matches-2/output.smtlib b/tests-system/rbt-signature-matches-2/output.smtlib new file mode 100644 index 00000000..a31ebfd3 --- /dev/null +++ b/tests-system/rbt-signature-matches-2/output.smtlib @@ -0,0 +1,3 @@ +matches(a, b, "potato"), warning "a should match with potato", a +^^^^^^^ rbt-signature-matches-2/foo.rsl:10: error: function requires 2 parameters +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-matches-3/foo.rsl b/tests-system/rbt-signature-matches-3/foo.rsl new file mode 100644 index 00000000..e30fd895 --- /dev/null +++ b/tests-system/rbt-signature-matches-3/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + a String + b String + c Integer +} + +checks T { + matches(a, "(abc(def)"), warning "a should match with potato", a +} diff --git a/tests-system/rbt-signature-matches-3/foo.trlc b/tests-system/rbt-signature-matches-3/foo.trlc new file mode 100644 index 00000000..97cbccf6 --- /dev/null +++ b/tests-system/rbt-signature-matches-3/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Bar { + a = "(abc(def)" + b = "kitten" + c = 1 +} diff --git a/tests-system/rbt-signature-matches-3/output b/tests-system/rbt-signature-matches-3/output new file mode 100644 index 00000000..16cec378 --- /dev/null +++ b/tests-system/rbt-signature-matches-3/output @@ -0,0 +1,3 @@ +matches(a, "(abc(def)"), warning "a should match with potato", a + ^^^^^^^^^^^ rbt-signature-matches-3/foo.rsl:10: error: missing ), unterminated subpattern at position 0 +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-matches-3/output.brief b/tests-system/rbt-signature-matches-3/output.brief new file mode 100644 index 00000000..5b4c0dd8 --- /dev/null +++ b/tests-system/rbt-signature-matches-3/output.brief @@ -0,0 +1 @@ +rbt-signature-matches-3/foo.rsl:10:16: trlc error: missing ), unterminated subpattern at position 0 diff --git a/tests-system/rbt-signature-matches-3/output.json b/tests-system/rbt-signature-matches-3/output.json new file mode 100644 index 00000000..16cec378 --- /dev/null +++ b/tests-system/rbt-signature-matches-3/output.json @@ -0,0 +1,3 @@ +matches(a, "(abc(def)"), warning "a should match with potato", a + ^^^^^^^^^^^ rbt-signature-matches-3/foo.rsl:10: error: missing ), unterminated subpattern at position 0 +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-matches-3/output.smtlib b/tests-system/rbt-signature-matches-3/output.smtlib new file mode 100644 index 00000000..16cec378 --- /dev/null +++ b/tests-system/rbt-signature-matches-3/output.smtlib @@ -0,0 +1,3 @@ +matches(a, "(abc(def)"), warning "a should match with potato", a + ^^^^^^^^^^^ rbt-signature-matches-3/foo.rsl:10: error: missing ), unterminated subpattern at position 0 +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-string-end-functions-1/foo.rsl b/tests-system/rbt-signature-string-end-functions-1/foo.rsl new file mode 100644 index 00000000..48e28213 --- /dev/null +++ b/tests-system/rbt-signature-string-end-functions-1/foo.rsl @@ -0,0 +1,14 @@ +package Foo + +type T { + a String + b String + c Integer +} + +checks T { + startswith(a, "po"), warning "a should start with po", a + startswith(b, "po"), warning "b should start with po", b + endswith(c, "en"), warning "a should end with en", c + endswith(b, "en"), warning "b should end with en", b +} diff --git a/tests-system/rbt-signature-string-end-functions-1/output b/tests-system/rbt-signature-string-end-functions-1/output new file mode 100644 index 00000000..3914fdbb --- /dev/null +++ b/tests-system/rbt-signature-string-end-functions-1/output @@ -0,0 +1,3 @@ +endswith(c, "en"), warning "a should end with en", c + ^ rbt-signature-string-end-functions-1/foo.rsl:12: error: expected expression of type Builtin_String, got Builtin_Integer instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-signature-string-end-functions-1/output.brief b/tests-system/rbt-signature-string-end-functions-1/output.brief new file mode 100644 index 00000000..b4c1b3b0 --- /dev/null +++ b/tests-system/rbt-signature-string-end-functions-1/output.brief @@ -0,0 +1 @@ +rbt-signature-string-end-functions-1/foo.rsl:12:14: trlc error: expected expression of type Builtin_String, got Builtin_Integer instead diff --git a/tests-system/rbt-signature-string-end-functions-1/output.json b/tests-system/rbt-signature-string-end-functions-1/output.json new file mode 100644 index 00000000..3914fdbb --- /dev/null +++ b/tests-system/rbt-signature-string-end-functions-1/output.json @@ -0,0 +1,3 @@ +endswith(c, "en"), warning "a should end with en", c + ^ rbt-signature-string-end-functions-1/foo.rsl:12: error: expected expression of type Builtin_String, got Builtin_Integer instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-signature-string-end-functions-1/output.smtlib b/tests-system/rbt-signature-string-end-functions-1/output.smtlib new file mode 100644 index 00000000..3914fdbb --- /dev/null +++ b/tests-system/rbt-signature-string-end-functions-1/output.smtlib @@ -0,0 +1,3 @@ +endswith(c, "en"), warning "a should end with en", c + ^ rbt-signature-string-end-functions-1/foo.rsl:12: error: expected expression of type Builtin_String, got Builtin_Integer instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-signature-string-end-functions-2/foo.rsl b/tests-system/rbt-signature-string-end-functions-2/foo.rsl new file mode 100644 index 00000000..19c6e27d --- /dev/null +++ b/tests-system/rbt-signature-string-end-functions-2/foo.rsl @@ -0,0 +1,14 @@ +package Foo + +type T { + a String + b String + c Integer +} + +checks T { + startswith(a, "po"), warning "a should start with po", a + startswith(b, "po"), warning "b should start with po", b + endswith(a, "en"), warning "a should end with en", a + endswith(a, b, "en"), warning "b should end with en", b +} diff --git a/tests-system/rbt-signature-string-end-functions-2/foo.trlc b/tests-system/rbt-signature-string-end-functions-2/foo.trlc new file mode 100644 index 00000000..71700516 --- /dev/null +++ b/tests-system/rbt-signature-string-end-functions-2/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Bar { + a = "potato" + b = "kitten" + c = 1 +} diff --git a/tests-system/rbt-signature-string-end-functions-2/output b/tests-system/rbt-signature-string-end-functions-2/output new file mode 100644 index 00000000..595f67df --- /dev/null +++ b/tests-system/rbt-signature-string-end-functions-2/output @@ -0,0 +1,3 @@ +endswith(a, b, "en"), warning "b should end with en", b +^^^^^^^^ rbt-signature-string-end-functions-2/foo.rsl:13: error: function requires 2 parameters +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-string-end-functions-2/output.brief b/tests-system/rbt-signature-string-end-functions-2/output.brief new file mode 100644 index 00000000..57483f2e --- /dev/null +++ b/tests-system/rbt-signature-string-end-functions-2/output.brief @@ -0,0 +1 @@ +rbt-signature-string-end-functions-2/foo.rsl:13:5: trlc error: function requires 2 parameters diff --git a/tests-system/rbt-signature-string-end-functions-2/output.json b/tests-system/rbt-signature-string-end-functions-2/output.json new file mode 100644 index 00000000..595f67df --- /dev/null +++ b/tests-system/rbt-signature-string-end-functions-2/output.json @@ -0,0 +1,3 @@ +endswith(a, b, "en"), warning "b should end with en", b +^^^^^^^^ rbt-signature-string-end-functions-2/foo.rsl:13: error: function requires 2 parameters +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-string-end-functions-2/output.smtlib b/tests-system/rbt-signature-string-end-functions-2/output.smtlib new file mode 100644 index 00000000..595f67df --- /dev/null +++ b/tests-system/rbt-signature-string-end-functions-2/output.smtlib @@ -0,0 +1,3 @@ +endswith(a, b, "en"), warning "b should end with en", b +^^^^^^^^ rbt-signature-string-end-functions-2/foo.rsl:13: error: function requires 2 parameters +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-signature-type-conversion/foo.rsl b/tests-system/rbt-signature-type-conversion/foo.rsl new file mode 100644 index 00000000..bf5ee208 --- /dev/null +++ b/tests-system/rbt-signature-type-conversion/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + a Integer + b Decimal +} + +checks T { + a >= Integer(b), warning "a is less than b" + b <= Decimal(a), warning "b is greater than a" +} diff --git a/tests-system/rbt-signature-type-conversion/foo.trlc b/tests-system/rbt-signature-type-conversion/foo.trlc new file mode 100644 index 00000000..327a17fe --- /dev/null +++ b/tests-system/rbt-signature-type-conversion/foo.trlc @@ -0,0 +1,6 @@ +package Foo + +T Bar { + a = 1 + b = 1.5 +} diff --git a/tests-system/rbt-signature-type-conversion/output b/tests-system/rbt-signature-type-conversion/output new file mode 100644 index 00000000..0e4788c9 --- /dev/null +++ b/tests-system/rbt-signature-type-conversion/output @@ -0,0 +1,5 @@ +T Bar { + ^^^ rbt-signature-type-conversion/foo.trlc:3: check warning: a is less than b +T Bar { + ^^^ rbt-signature-type-conversion/foo.trlc:3: check warning: b is greater than a +Processed 1 model and 1 requirement file and found 2 warnings diff --git a/tests-system/rbt-signature-type-conversion/output.brief b/tests-system/rbt-signature-type-conversion/output.brief new file mode 100644 index 00000000..98a43d2d --- /dev/null +++ b/tests-system/rbt-signature-type-conversion/output.brief @@ -0,0 +1,2 @@ +rbt-signature-type-conversion/foo.trlc:3:3: trlc check warning: a is less than b +rbt-signature-type-conversion/foo.trlc:3:3: trlc check warning: b is greater than a diff --git a/tests-system/rbt-signature-type-conversion/output.json b/tests-system/rbt-signature-type-conversion/output.json new file mode 100644 index 00000000..74df0025 --- /dev/null +++ b/tests-system/rbt-signature-type-conversion/output.json @@ -0,0 +1,11 @@ +T Bar { + ^^^ rbt-signature-type-conversion/foo.trlc:3: check warning: a is less than b +T Bar { + ^^^ rbt-signature-type-conversion/foo.trlc:3: check warning: b is greater than a +{ + "Bar": { + "a": 1, + "b": 1.5 + } +} +Processed 1 model and 1 requirement file and found 2 warnings diff --git a/tests-system/rbt-signature-type-conversion/output.smtlib b/tests-system/rbt-signature-type-conversion/output.smtlib new file mode 100644 index 00000000..0e4788c9 --- /dev/null +++ b/tests-system/rbt-signature-type-conversion/output.smtlib @@ -0,0 +1,5 @@ +T Bar { + ^^^ rbt-signature-type-conversion/foo.trlc:3: check warning: a is less than b +T Bar { + ^^^ rbt-signature-type-conversion/foo.trlc:3: check warning: b is greater than a +Processed 1 model and 1 requirement file and found 2 warnings diff --git a/tests-system/rbt-signature-type-conversion/tracing b/tests-system/rbt-signature-type-conversion/tracing new file mode 100644 index 00000000..a26fbff5 --- /dev/null +++ b/tests-system/rbt-signature-type-conversion/tracing @@ -0,0 +1,2 @@ +LRM.Integer_Conversion_Semantics +LRM.Decimal_Conversion_Semantics diff --git a/tests-system/rbt-startswith-semantics/foo.rsl b/tests-system/rbt-startswith-semantics/foo.rsl new file mode 100644 index 00000000..77014bad --- /dev/null +++ b/tests-system/rbt-startswith-semantics/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type T { + a String +} + +checks T { + startswith(a, "p"), warning "a should start with p", a +} diff --git a/tests-system/rbt-startswith-semantics/foo.trlc b/tests-system/rbt-startswith-semantics/foo.trlc new file mode 100644 index 00000000..a5493199 --- /dev/null +++ b/tests-system/rbt-startswith-semantics/foo.trlc @@ -0,0 +1,5 @@ +package Foo + +T Bar { + a = "potato" +} diff --git a/tests-system/rbt-startswith-semantics/output b/tests-system/rbt-startswith-semantics/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-startswith-semantics/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-startswith-semantics/output.brief b/tests-system/rbt-startswith-semantics/output.brief new file mode 100644 index 00000000..e69de29b diff --git a/tests-system/rbt-startswith-semantics/output.json b/tests-system/rbt-startswith-semantics/output.json new file mode 100644 index 00000000..0817587a --- /dev/null +++ b/tests-system/rbt-startswith-semantics/output.json @@ -0,0 +1,6 @@ +{ + "Bar": { + "a": "potato" + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-startswith-semantics/output.smtlib b/tests-system/rbt-startswith-semantics/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-startswith-semantics/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-static-regular-expression/foo.rsl b/tests-system/rbt-static-regular-expression/foo.rsl new file mode 100644 index 00000000..ddb2e9b4 --- /dev/null +++ b/tests-system/rbt-static-regular-expression/foo.rsl @@ -0,0 +1,10 @@ +package Foo + +type T { + a String + b String +} + +checks T { + matches(a, b), warning "a and b are not the same" +} diff --git a/tests-system/rbt-static-regular-expression/foo.trlc b/tests-system/rbt-static-regular-expression/foo.trlc new file mode 100644 index 00000000..aad56745 --- /dev/null +++ b/tests-system/rbt-static-regular-expression/foo.trlc @@ -0,0 +1,6 @@ +package Foo + +T Bar { + a = "potato" + b = "potato" +} diff --git a/tests-system/rbt-static-regular-expression/output b/tests-system/rbt-static-regular-expression/output new file mode 100644 index 00000000..fbfa63d1 --- /dev/null +++ b/tests-system/rbt-static-regular-expression/output @@ -0,0 +1,3 @@ +matches(a, b), warning "a and b are not the same" + ^ rbt-static-regular-expression/foo.rsl:9: error: cannot be used in a static context +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-static-regular-expression/output.brief b/tests-system/rbt-static-regular-expression/output.brief new file mode 100644 index 00000000..bba924ef --- /dev/null +++ b/tests-system/rbt-static-regular-expression/output.brief @@ -0,0 +1 @@ +rbt-static-regular-expression/foo.rsl:9:16: trlc error: cannot be used in a static context diff --git a/tests-system/rbt-static-regular-expression/output.json b/tests-system/rbt-static-regular-expression/output.json new file mode 100644 index 00000000..fbfa63d1 --- /dev/null +++ b/tests-system/rbt-static-regular-expression/output.json @@ -0,0 +1,3 @@ +matches(a, b), warning "a and b are not the same" + ^ rbt-static-regular-expression/foo.rsl:9: error: cannot be used in a static context +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-static-regular-expression/output.smtlib b/tests-system/rbt-static-regular-expression/output.smtlib new file mode 100644 index 00000000..fbfa63d1 --- /dev/null +++ b/tests-system/rbt-static-regular-expression/output.smtlib @@ -0,0 +1,3 @@ +matches(a, b), warning "a and b are not the same" + ^ rbt-static-regular-expression/foo.rsl:9: error: cannot be used in a static context +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-valid-access-prefixes/foo.rsl b/tests-system/rbt-valid-access-prefixes/foo.rsl new file mode 100644 index 00000000..e576670f --- /dev/null +++ b/tests-system/rbt-valid-access-prefixes/foo.rsl @@ -0,0 +1,22 @@ +package Foo + +enum E { + A + B + C +} + +tuple T { + first Integer + separator @ + second Integer +} + +type Bar { + e E + t T +} + +checks Bar { + t.first + t.second + t.third !=0, error "sum of tuple elements must not be 0", t +} diff --git a/tests-system/rbt-valid-access-prefixes/foo.trlc b/tests-system/rbt-valid-access-prefixes/foo.trlc new file mode 100644 index 00000000..47edafda --- /dev/null +++ b/tests-system/rbt-valid-access-prefixes/foo.trlc @@ -0,0 +1,6 @@ +package Foo + +Bar potato { + e = E.D + t = 1@2 +} diff --git a/tests-system/rbt-valid-access-prefixes/output b/tests-system/rbt-valid-access-prefixes/output new file mode 100644 index 00000000..c5d29933 --- /dev/null +++ b/tests-system/rbt-valid-access-prefixes/output @@ -0,0 +1,5 @@ +t.first + t.second + t.third !=0, error "sum of tuple elements must not be 0", t + ^^^^^ rbt-valid-access-prefixes/foo.rsl:21: error: unknown symbol third +e = E.D + ^ rbt-valid-access-prefixes/foo.trlc:4: error: unknown symbol D +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-valid-access-prefixes/output.brief b/tests-system/rbt-valid-access-prefixes/output.brief new file mode 100644 index 00000000..6a3e3ebe --- /dev/null +++ b/tests-system/rbt-valid-access-prefixes/output.brief @@ -0,0 +1,2 @@ +rbt-valid-access-prefixes/foo.rsl:21:28: trlc error: unknown symbol third +rbt-valid-access-prefixes/foo.trlc:4:11: trlc error: unknown symbol D diff --git a/tests-system/rbt-valid-access-prefixes/output.json b/tests-system/rbt-valid-access-prefixes/output.json new file mode 100644 index 00000000..c5d29933 --- /dev/null +++ b/tests-system/rbt-valid-access-prefixes/output.json @@ -0,0 +1,5 @@ +t.first + t.second + t.third !=0, error "sum of tuple elements must not be 0", t + ^^^^^ rbt-valid-access-prefixes/foo.rsl:21: error: unknown symbol third +e = E.D + ^ rbt-valid-access-prefixes/foo.trlc:4: error: unknown symbol D +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-valid-access-prefixes/output.smtlib b/tests-system/rbt-valid-access-prefixes/output.smtlib new file mode 100644 index 00000000..c5d29933 --- /dev/null +++ b/tests-system/rbt-valid-access-prefixes/output.smtlib @@ -0,0 +1,5 @@ +t.first + t.second + t.third !=0, error "sum of tuple elements must not be 0", t + ^^^^^ rbt-valid-access-prefixes/foo.rsl:21: error: unknown symbol third +e = E.D + ^ rbt-valid-access-prefixes/foo.trlc:4: error: unknown symbol D +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-valid-base-names/bar.rsl b/tests-system/rbt-valid-base-names/bar.rsl new file mode 100644 index 00000000..cd9dd38b --- /dev/null +++ b/tests-system/rbt-valid-base-names/bar.rsl @@ -0,0 +1,5 @@ +package Bar + +type D { + a Integer +} diff --git a/tests-system/rbt-valid-base-names/foo.rsl b/tests-system/rbt-valid-base-names/foo.rsl new file mode 100644 index 00000000..7ce0c330 --- /dev/null +++ b/tests-system/rbt-valid-base-names/foo.rsl @@ -0,0 +1,5 @@ +package Foo + +type T { + a Integer +} diff --git a/tests-system/rbt-valid-base-names/foo.trlc b/tests-system/rbt-valid-base-names/foo.trlc new file mode 100644 index 00000000..626c1f5b --- /dev/null +++ b/tests-system/rbt-valid-base-names/foo.trlc @@ -0,0 +1,10 @@ +package Foo +import Bar + +T potato { + a = 1 +} + +Bar.T kitten { + a = 1 +} diff --git a/tests-system/rbt-valid-base-names/output b/tests-system/rbt-valid-base-names/output new file mode 100644 index 00000000..ea513397 --- /dev/null +++ b/tests-system/rbt-valid-base-names/output @@ -0,0 +1,3 @@ +Bar.T kitten { + ^ rbt-valid-base-names/foo.trlc:8: error: unknown symbol T +Processed 2 models and 1 requirement file and found 1 error diff --git a/tests-system/rbt-valid-base-names/output.brief b/tests-system/rbt-valid-base-names/output.brief new file mode 100644 index 00000000..4851ef87 --- /dev/null +++ b/tests-system/rbt-valid-base-names/output.brief @@ -0,0 +1 @@ +rbt-valid-base-names/foo.trlc:8:5: trlc error: unknown symbol T diff --git a/tests-system/rbt-valid-base-names/output.json b/tests-system/rbt-valid-base-names/output.json new file mode 100644 index 00000000..ea513397 --- /dev/null +++ b/tests-system/rbt-valid-base-names/output.json @@ -0,0 +1,3 @@ +Bar.T kitten { + ^ rbt-valid-base-names/foo.trlc:8: error: unknown symbol T +Processed 2 models and 1 requirement file and found 1 error diff --git a/tests-system/rbt-valid-base-names/output.smtlib b/tests-system/rbt-valid-base-names/output.smtlib new file mode 100644 index 00000000..ea513397 --- /dev/null +++ b/tests-system/rbt-valid-base-names/output.smtlib @@ -0,0 +1,3 @@ +Bar.T kitten { + ^ rbt-valid-base-names/foo.trlc:8: error: unknown symbol T +Processed 2 models and 1 requirement file and found 1 error diff --git a/tests-system/rbt-valid-function-prefixes/foo.rsl b/tests-system/rbt-valid-function-prefixes/foo.rsl new file mode 100644 index 00000000..1bc420c1 --- /dev/null +++ b/tests-system/rbt-valid-function-prefixes/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + a String + b Integer +} + +checks T { + len(a) > b, error "potato error" + size(a) > b, error "potato error" +} diff --git a/tests-system/rbt-valid-function-prefixes/output b/tests-system/rbt-valid-function-prefixes/output new file mode 100644 index 00000000..2cdbed98 --- /dev/null +++ b/tests-system/rbt-valid-function-prefixes/output @@ -0,0 +1,3 @@ +size(a) > b, error "potato error" +^^^^ rbt-valid-function-prefixes/foo.rsl:10: error: unknown symbol size +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-valid-function-prefixes/output.brief b/tests-system/rbt-valid-function-prefixes/output.brief new file mode 100644 index 00000000..ddfaa20d --- /dev/null +++ b/tests-system/rbt-valid-function-prefixes/output.brief @@ -0,0 +1 @@ +rbt-valid-function-prefixes/foo.rsl:10:5: trlc error: unknown symbol size diff --git a/tests-system/rbt-valid-function-prefixes/output.json b/tests-system/rbt-valid-function-prefixes/output.json new file mode 100644 index 00000000..2cdbed98 --- /dev/null +++ b/tests-system/rbt-valid-function-prefixes/output.json @@ -0,0 +1,3 @@ +size(a) > b, error "potato error" +^^^^ rbt-valid-function-prefixes/foo.rsl:10: error: unknown symbol size +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-valid-function-prefixes/output.smtlib b/tests-system/rbt-valid-function-prefixes/output.smtlib new file mode 100644 index 00000000..2cdbed98 --- /dev/null +++ b/tests-system/rbt-valid-function-prefixes/output.smtlib @@ -0,0 +1,3 @@ +size(a) > b, error "potato error" +^^^^ rbt-valid-function-prefixes/foo.rsl:10: error: unknown symbol size +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-valid-index-prefixes/foo.rsl b/tests-system/rbt-valid-index-prefixes/foo.rsl new file mode 100644 index 00000000..9043b879 --- /dev/null +++ b/tests-system/rbt-valid-index-prefixes/foo.rsl @@ -0,0 +1,10 @@ +package Foo + +type T { + a Integer[1..*] + b Integer +} + +checks T { + a[0] + b[0] != 0, error "potato error" +} diff --git a/tests-system/rbt-valid-index-prefixes/output b/tests-system/rbt-valid-index-prefixes/output new file mode 100644 index 00000000..35185706 --- /dev/null +++ b/tests-system/rbt-valid-index-prefixes/output @@ -0,0 +1,3 @@ +a[0] + b[0] != 0, error "potato error" + ^ rbt-valid-index-prefixes/foo.rsl:9: error: expression 'b' has type Integer, which is not an array +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-valid-index-prefixes/output.brief b/tests-system/rbt-valid-index-prefixes/output.brief new file mode 100644 index 00000000..17e82961 --- /dev/null +++ b/tests-system/rbt-valid-index-prefixes/output.brief @@ -0,0 +1 @@ +rbt-valid-index-prefixes/foo.rsl:9:12: trlc error: expression 'b' has type Integer, which is not an array diff --git a/tests-system/rbt-valid-index-prefixes/output.json b/tests-system/rbt-valid-index-prefixes/output.json new file mode 100644 index 00000000..35185706 --- /dev/null +++ b/tests-system/rbt-valid-index-prefixes/output.json @@ -0,0 +1,3 @@ +a[0] + b[0] != 0, error "potato error" + ^ rbt-valid-index-prefixes/foo.rsl:9: error: expression 'b' has type Integer, which is not an array +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-valid-index-prefixes/output.smtlib b/tests-system/rbt-valid-index-prefixes/output.smtlib new file mode 100644 index 00000000..35185706 --- /dev/null +++ b/tests-system/rbt-valid-index-prefixes/output.smtlib @@ -0,0 +1,3 @@ +a[0] + b[0] != 0, error "potato error" + ^ rbt-valid-index-prefixes/foo.rsl:9: error: expression 'b' has type Integer, which is not an array +Processed 1 model and 0 requirement files and found 1 error diff --git a/trlc/ast.py b/trlc/ast.py index 5777e107..d36900cf 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -492,6 +492,7 @@ def to_string(self): # pragma: no cover def ensure_type(self, mh, typ): # lobster-trace: LRM.Restricted_Null # lobster-trace: LRM.Null_Is_Invalid + assert isinstance(typ, (type, Type)) if self.typ is None: mh.error(self.location, @@ -1106,6 +1107,8 @@ def can_be_null(self): class Name_Reference(Expression): # lobster-trace: LRM.Qualified_Name + # lobster-trace: LRM.Static_Regular_Expression + """Reference to a name Name reference to either a :class:`Composite_Component` or a @@ -1184,6 +1187,9 @@ def __init__(self, mh, location, typ, operator, n_operand): # lobster-trace: LRM.Simple_Expression # lobster-trace: LRM.Relation # lobster-trace: LRM.Factor + # lobster-trace: LRM.Signature_Len + # lobster-trace: LRM.Signature_Type_Conversion + super().__init__(location, typ) assert isinstance(mh, Message_Handler) assert isinstance(operator, Unary_Operator) @@ -1242,6 +1248,12 @@ def dump(self, indent=0): # pragma: no cover def evaluate(self, mh, context): # lobster-trace: LRM.Null_Is_Invalid + # lobster-trace: LRM.Signature_Len + # lobster-trace: LRM.Signature_Type_Conversion + # lobster-trace: LRM.Len_Semantics + # lobster-trace: LRM.Integer_Conversion_Semantics + # lobster-trace: LRM.Decimal_Conversion_Semantics + assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) @@ -1353,6 +1365,9 @@ def __init__(self, mh, location, typ, operator, n_lhs, n_rhs): # lobster-trace: LRM.Simple_Expression # lobster-trace: LRM.Term # lobster-trace: LRM.Factor + # lobster-trace: LRM.Signature_String_End_Functions + # lobster-trace: LRM.Signature_Matches + super().__init__(location, typ) assert isinstance(mh, Message_Handler) assert isinstance(operator, Binary_Operator) @@ -1483,6 +1498,12 @@ def to_string(self): def evaluate(self, mh, context): # lobster-trace: LRM.Null_Equivalence # lobster-trace: LRM.Null_Is_Invalid + # lobster-trace: LRM.Signature_String_End_Functions + # lobster-trace: LRM.Signature_Matches + # lobster-trace: LRM.Startswith_Semantics + # lobster-trace: LRM.Endswith_Semantics + # lobster-trace: LRM.Matches_Semantics + assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) @@ -3273,6 +3294,9 @@ def lookup_direct(self, simplified=False): # lobster-trace: LRM.Described_Name_Equality # lobster-trace: LRM.Sufficiently_Distinct + # lobster-trace: LRM.Valid_Base_Names + # lobster-trace: LRM.Valid_Access_Prefixes + # lobster-trace: LRM.Valid_Function_Prefixes """Retrieve an object from the table For example:: @@ -3401,6 +3425,10 @@ def create_global_table(cls, mh): # lobster-trace: LRM.Builtin_Types # lobster-trace: LRM.Builtin_Functions # lobster-trace: LRM.Builtin_Type_Conversion_Functions + # lobster-trace: LRM.Signature_Len + # lobster-trace: LRM.Signature_String_End_Functions + # lobster-trace: LRM.Signature_Matches + stab = Symbol_Table() stab.register(mh, Builtin_Integer()) stab.register(mh, Builtin_Decimal()) diff --git a/trlc/parser.py b/trlc/parser.py index 925100d9..b0843e7e 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -1243,6 +1243,7 @@ def parse_builtin(self, scope, n_name, t_name): elif n_name.name == "matches": parameters[1].ensure_type(self.mh, ast.Builtin_String) try: + # lobster-trace: LRM.Static_Regular_Expression # scope is None on purpose to enforce static context value = parameters[1].evaluate(self.mh, None) assert isinstance(value.typ, ast.Builtin_String) @@ -1290,6 +1291,9 @@ def parse_builtin(self, scope, n_name, t_name): "unexpected builtin") def parse_name(self, scope): + # lobster-trace: LRM.Names + # lobster-trace: LRM.Case_Sensitive + # This is a bit more complex. The grammar is: # # qualified_name ::= [ IDENTIFIER_package_name '.' ] IDENTIFIER_name @@ -1373,6 +1377,7 @@ def parse_name(self, scope): while self.peek("DOT") or self.peek("S_BRA"): if self.peek("DOT"): if not isinstance(n_name.typ, ast.Tuple_Type): + # lobster-trace: LRM.Valid_Index_Prefixes self.mh.error(n_name.location, "expression '%s' has type %s, " "which is not a tuple" %