From b12214ade24bdfb30babd05c4ebdabdb3856972a Mon Sep 17 00:00:00 2001 From: christophkloeffel Date: Mon, 9 Oct 2023 07:53:54 +0200 Subject: [PATCH] adds tracing for checks --- language-reference-manual/lrm.trlc | 3 ++- tests-system/checks-10/foo.rsl | 10 ++++++++++ tests-system/checks-10/output | 3 +++ tests-system/checks-10/output.brief | 1 + tests-system/checks-10/output.json | 3 +++ tests-system/checks-10/output.smtlib | 3 +++ tests-system/checks-10/tracing | 1 + tests-system/checks-11/foo.rsl | 12 ++++++++++++ tests-system/checks-11/foo.trlc | 6 ++++++ tests-system/checks-11/output | 7 +++++++ tests-system/checks-11/output.brief | 3 +++ tests-system/checks-11/output.json | 13 +++++++++++++ tests-system/checks-11/output.smtlib | 7 +++++++ tests-system/checks-11/tracing | 1 + tests-system/checks-12/bar.rsl | 11 +++++++++++ tests-system/checks-12/bar.trlc | 6 ++++++ tests-system/checks-12/foo.rsl | 9 +++++++++ tests-system/checks-12/output | 5 +++++ tests-system/checks-12/output.brief | 2 ++ tests-system/checks-12/output.json | 5 +++++ tests-system/checks-12/output.smtlib | 5 +++++ tests-system/checks-12/tracing | 2 ++ tests-system/checks-9/bar.rsl | 5 +++++ tests-system/checks-9/foo.rsl | 10 ++++++++++ tests-system/checks-9/output | 3 +++ tests-system/checks-9/output.brief | 1 + tests-system/checks-9/output.json | 3 +++ tests-system/checks-9/output.smtlib | 3 +++ tests-system/checks-9/tracing | 1 + tests-system/checks-error/foo.rsl | 13 +++++++++++++ tests-system/checks-error/foo.trlc | 7 +++++++ tests-system/checks-error/output | 7 +++++++ tests-system/checks-error/output.brief | 3 +++ tests-system/checks-error/output.json | 7 +++++++ tests-system/checks-error/output.smtlib | 7 +++++++ tests-system/checks-error/tracing | 1 + tests-system/checks-fatal/foo.rsl | 13 +++++++++++++ tests-system/checks-fatal/foo.trlc | 7 +++++++ tests-system/checks-fatal/output | 3 +++ tests-system/checks-fatal/output.brief | 1 + tests-system/checks-fatal/output.json | 3 +++ tests-system/checks-fatal/output.smtlib | 3 +++ tests-system/checks-fatal/tracing | 1 + tests-system/checks-warning/foo.rsl | 13 +++++++++++++ tests-system/checks-warning/foo.trlc | 7 +++++++ tests-system/checks-warning/output | 7 +++++++ tests-system/checks-warning/output.brief | 3 +++ tests-system/checks-warning/output.json | 14 ++++++++++++++ tests-system/checks-warning/output.smtlib | 7 +++++++ tests-system/checks-warning/tracing | 1 + tests-system/simple/foo.rsl | 9 +++++++++ tests-system/simple/instances.trlc | 5 +++++ tests-system/simple/output | 2 +- tests-system/simple/output.json | 5 ++++- tests-system/simple/output.smtlib | 2 +- tests-system/simple/tracing | 1 + trlc/ast.py | 3 +++ trlc/parser.py | 4 ++++ 58 files changed, 299 insertions(+), 4 deletions(-) create mode 100644 tests-system/checks-10/foo.rsl create mode 100644 tests-system/checks-10/output create mode 100644 tests-system/checks-10/output.brief create mode 100644 tests-system/checks-10/output.json create mode 100644 tests-system/checks-10/output.smtlib create mode 100644 tests-system/checks-10/tracing create mode 100644 tests-system/checks-11/foo.rsl create mode 100644 tests-system/checks-11/foo.trlc create mode 100644 tests-system/checks-11/output create mode 100644 tests-system/checks-11/output.brief create mode 100644 tests-system/checks-11/output.json create mode 100644 tests-system/checks-11/output.smtlib create mode 100644 tests-system/checks-11/tracing create mode 100644 tests-system/checks-12/bar.rsl create mode 100644 tests-system/checks-12/bar.trlc create mode 100644 tests-system/checks-12/foo.rsl create mode 100644 tests-system/checks-12/output create mode 100644 tests-system/checks-12/output.brief create mode 100644 tests-system/checks-12/output.json create mode 100644 tests-system/checks-12/output.smtlib create mode 100644 tests-system/checks-12/tracing create mode 100644 tests-system/checks-9/bar.rsl create mode 100644 tests-system/checks-9/foo.rsl create mode 100644 tests-system/checks-9/output create mode 100644 tests-system/checks-9/output.brief create mode 100644 tests-system/checks-9/output.json create mode 100644 tests-system/checks-9/output.smtlib create mode 100644 tests-system/checks-9/tracing create mode 100644 tests-system/checks-error/foo.rsl create mode 100644 tests-system/checks-error/foo.trlc create mode 100644 tests-system/checks-error/output create mode 100644 tests-system/checks-error/output.brief create mode 100644 tests-system/checks-error/output.json create mode 100644 tests-system/checks-error/output.smtlib create mode 100644 tests-system/checks-error/tracing create mode 100644 tests-system/checks-fatal/foo.rsl create mode 100644 tests-system/checks-fatal/foo.trlc create mode 100644 tests-system/checks-fatal/output create mode 100644 tests-system/checks-fatal/output.brief create mode 100644 tests-system/checks-fatal/output.json create mode 100644 tests-system/checks-fatal/output.smtlib create mode 100644 tests-system/checks-fatal/tracing create mode 100644 tests-system/checks-warning/foo.rsl create mode 100644 tests-system/checks-warning/foo.trlc create mode 100644 tests-system/checks-warning/output create mode 100644 tests-system/checks-warning/output.brief create mode 100644 tests-system/checks-warning/output.json create mode 100644 tests-system/checks-warning/output.smtlib create mode 100644 tests-system/checks-warning/tracing create mode 100644 tests-system/simple/foo.rsl diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index 5c927315..f8319774 100644 --- a/language-reference-manual/lrm.trlc +++ b/language-reference-manual/lrm.trlc @@ -886,7 +886,7 @@ section "Checks" { order.''' } - Dynamic_Semantics Check_Evaluation_Order_Across_Blocks { + Note Check_Evaluation_Order_Across_Blocks { text = '''If multiple check blocks are declared for the same type, then the order of evaluation of each check block is unspecified.''' @@ -1001,6 +1001,7 @@ section "Checks" { error "CB Version must be positive", version } """ + untraced_reason = "Example code" } } diff --git a/tests-system/checks-10/foo.rsl b/tests-system/checks-10/foo.rsl new file mode 100644 index 00000000..cf88f135 --- /dev/null +++ b/tests-system/checks-10/foo.rsl @@ -0,0 +1,10 @@ +package Foo + +type T { + a String + b String +} + +checks T { + len(c) > 10, "c is too short", c +} diff --git a/tests-system/checks-10/output b/tests-system/checks-10/output new file mode 100644 index 00000000..01e426da --- /dev/null +++ b/tests-system/checks-10/output @@ -0,0 +1,3 @@ +len(c) > 10, "c is too short", c + ^ checks-10/foo.rsl:9: error: unknown symbol c +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/checks-10/output.brief b/tests-system/checks-10/output.brief new file mode 100644 index 00000000..0f4cd339 --- /dev/null +++ b/tests-system/checks-10/output.brief @@ -0,0 +1 @@ +checks-10/foo.rsl:9:9: trlc error: unknown symbol c diff --git a/tests-system/checks-10/output.json b/tests-system/checks-10/output.json new file mode 100644 index 00000000..01e426da --- /dev/null +++ b/tests-system/checks-10/output.json @@ -0,0 +1,3 @@ +len(c) > 10, "c is too short", c + ^ checks-10/foo.rsl:9: error: unknown symbol c +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/checks-10/output.smtlib b/tests-system/checks-10/output.smtlib new file mode 100644 index 00000000..01e426da --- /dev/null +++ b/tests-system/checks-10/output.smtlib @@ -0,0 +1,3 @@ +len(c) > 10, "c is too short", c + ^ checks-10/foo.rsl:9: error: unknown symbol c +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/checks-10/tracing b/tests-system/checks-10/tracing new file mode 100644 index 00000000..ffcd6270 --- /dev/null +++ b/tests-system/checks-10/tracing @@ -0,0 +1 @@ +LRM.Applicable_Components diff --git a/tests-system/checks-11/foo.rsl b/tests-system/checks-11/foo.rsl new file mode 100644 index 00000000..31a819a5 --- /dev/null +++ b/tests-system/checks-11/foo.rsl @@ -0,0 +1,12 @@ +package Foo + +type T { + a Integer + b Integer +} + +checks T { + a < 0, warning "First warning: a is positive", a + b > 0, warning "Second warning: b is negative", b + a < b, warning "Third warning: a is greater than b" +} diff --git a/tests-system/checks-11/foo.trlc b/tests-system/checks-11/foo.trlc new file mode 100644 index 00000000..f628a73e --- /dev/null +++ b/tests-system/checks-11/foo.trlc @@ -0,0 +1,6 @@ +package Foo + +T Bar { + a = 1 + b = -1 +} diff --git a/tests-system/checks-11/output b/tests-system/checks-11/output new file mode 100644 index 00000000..9882581b --- /dev/null +++ b/tests-system/checks-11/output @@ -0,0 +1,7 @@ +a = 1 + ^ checks-11/foo.trlc:4: check warning: First warning: a is positive +b = -1 + ^ checks-11/foo.trlc:5: check warning: Second warning: b is negative +T Bar { + ^^^ checks-11/foo.trlc:3: check warning: Third warning: a is greater than b +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s) diff --git a/tests-system/checks-11/output.brief b/tests-system/checks-11/output.brief new file mode 100644 index 00000000..70e565e4 --- /dev/null +++ b/tests-system/checks-11/output.brief @@ -0,0 +1,3 @@ +checks-11/foo.trlc:4:7: trlc check warning: First warning: a is positive +checks-11/foo.trlc:5:7: trlc check warning: Second warning: b is negative +checks-11/foo.trlc:3:3: trlc check warning: Third warning: a is greater than b diff --git a/tests-system/checks-11/output.json b/tests-system/checks-11/output.json new file mode 100644 index 00000000..e7d33d34 --- /dev/null +++ b/tests-system/checks-11/output.json @@ -0,0 +1,13 @@ +a = 1 + ^ checks-11/foo.trlc:4: check warning: First warning: a is positive +b = -1 + ^ checks-11/foo.trlc:5: check warning: Second warning: b is negative +T Bar { + ^^^ checks-11/foo.trlc:3: check warning: Third warning: a is greater than b +{ + "Bar": { + "a": 1, + "b": -1 + } +} +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s) diff --git a/tests-system/checks-11/output.smtlib b/tests-system/checks-11/output.smtlib new file mode 100644 index 00000000..9882581b --- /dev/null +++ b/tests-system/checks-11/output.smtlib @@ -0,0 +1,7 @@ +a = 1 + ^ checks-11/foo.trlc:4: check warning: First warning: a is positive +b = -1 + ^ checks-11/foo.trlc:5: check warning: Second warning: b is negative +T Bar { + ^^^ checks-11/foo.trlc:3: check warning: Third warning: a is greater than b +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s) diff --git a/tests-system/checks-11/tracing b/tests-system/checks-11/tracing new file mode 100644 index 00000000..90b23a29 --- /dev/null +++ b/tests-system/checks-11/tracing @@ -0,0 +1 @@ +LRM.Check_Evaluation_Order diff --git a/tests-system/checks-12/bar.rsl b/tests-system/checks-12/bar.rsl new file mode 100644 index 00000000..829805f6 --- /dev/null +++ b/tests-system/checks-12/bar.rsl @@ -0,0 +1,11 @@ +package Bar +import Foo + +type T extends Foo.T { + b String +} + +checks T { + len(a) > 10, "a has to be more than 10 chars", a + len(b) > 10, "b has to be more than 10 chars", b +} diff --git a/tests-system/checks-12/bar.trlc b/tests-system/checks-12/bar.trlc new file mode 100644 index 00000000..60faaa18 --- /dev/null +++ b/tests-system/checks-12/bar.trlc @@ -0,0 +1,6 @@ +package Bar + +T Test { + a = "potato" + b = "more potatoes" +} diff --git a/tests-system/checks-12/foo.rsl b/tests-system/checks-12/foo.rsl new file mode 100644 index 00000000..d09d18ae --- /dev/null +++ b/tests-system/checks-12/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type T { + a String +} + +checks T { + len(a) > 10, warning "a has to be more than 7 chars", a +} diff --git a/tests-system/checks-12/output b/tests-system/checks-12/output new file mode 100644 index 00000000..68c6a585 --- /dev/null +++ b/tests-system/checks-12/output @@ -0,0 +1,5 @@ +a = "potato" + ^^^^^^^^ checks-12/bar.trlc:4: check warning: a has to be more than 7 chars +a = "potato" + ^^^^^^^^ checks-12/bar.trlc:4: check error: a has to be more than 10 chars +Processed 2 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/checks-12/output.brief b/tests-system/checks-12/output.brief new file mode 100644 index 00000000..38f5901a --- /dev/null +++ b/tests-system/checks-12/output.brief @@ -0,0 +1,2 @@ +checks-12/bar.trlc:4:9: trlc check warning: a has to be more than 7 chars +checks-12/bar.trlc:4:9: trlc check error: a has to be more than 10 chars diff --git a/tests-system/checks-12/output.json b/tests-system/checks-12/output.json new file mode 100644 index 00000000..68c6a585 --- /dev/null +++ b/tests-system/checks-12/output.json @@ -0,0 +1,5 @@ +a = "potato" + ^^^^^^^^ checks-12/bar.trlc:4: check warning: a has to be more than 7 chars +a = "potato" + ^^^^^^^^ checks-12/bar.trlc:4: check error: a has to be more than 10 chars +Processed 2 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/checks-12/output.smtlib b/tests-system/checks-12/output.smtlib new file mode 100644 index 00000000..68c6a585 --- /dev/null +++ b/tests-system/checks-12/output.smtlib @@ -0,0 +1,5 @@ +a = "potato" + ^^^^^^^^ checks-12/bar.trlc:4: check warning: a has to be more than 7 chars +a = "potato" + ^^^^^^^^ checks-12/bar.trlc:4: check error: a has to be more than 10 chars +Processed 2 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/checks-12/tracing b/tests-system/checks-12/tracing new file mode 100644 index 00000000..e203a319 --- /dev/null +++ b/tests-system/checks-12/tracing @@ -0,0 +1,2 @@ +LRM.Check_Evaluation_Order_For_Extensions +LRM.Check_Messages diff --git a/tests-system/checks-9/bar.rsl b/tests-system/checks-9/bar.rsl new file mode 100644 index 00000000..5898c979 --- /dev/null +++ b/tests-system/checks-9/bar.rsl @@ -0,0 +1,5 @@ +package Bar + +type B { + a String +} diff --git a/tests-system/checks-9/foo.rsl b/tests-system/checks-9/foo.rsl new file mode 100644 index 00000000..a8b1b2de --- /dev/null +++ b/tests-system/checks-9/foo.rsl @@ -0,0 +1,10 @@ +package Foo +import Bar + +type T { + a String +} + +checks B { + len(a) > 10, "a is too short", a +} diff --git a/tests-system/checks-9/output b/tests-system/checks-9/output new file mode 100644 index 00000000..974f5ef5 --- /dev/null +++ b/tests-system/checks-9/output @@ -0,0 +1,3 @@ +checks B { + ^ checks-9/foo.rsl:8: error: unknown symbol B +Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/checks-9/output.brief b/tests-system/checks-9/output.brief new file mode 100644 index 00000000..d6acfcd5 --- /dev/null +++ b/tests-system/checks-9/output.brief @@ -0,0 +1 @@ +checks-9/foo.rsl:8:8: trlc error: unknown symbol B diff --git a/tests-system/checks-9/output.json b/tests-system/checks-9/output.json new file mode 100644 index 00000000..974f5ef5 --- /dev/null +++ b/tests-system/checks-9/output.json @@ -0,0 +1,3 @@ +checks B { + ^ checks-9/foo.rsl:8: error: unknown symbol B +Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/checks-9/output.smtlib b/tests-system/checks-9/output.smtlib new file mode 100644 index 00000000..974f5ef5 --- /dev/null +++ b/tests-system/checks-9/output.smtlib @@ -0,0 +1,3 @@ +checks B { + ^ checks-9/foo.rsl:8: error: unknown symbol B +Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/checks-9/tracing b/tests-system/checks-9/tracing new file mode 100644 index 00000000..f3ec06d7 --- /dev/null +++ b/tests-system/checks-9/tracing @@ -0,0 +1 @@ +LRM.Applicable_Types diff --git a/tests-system/checks-error/foo.rsl b/tests-system/checks-error/foo.rsl new file mode 100644 index 00000000..1271d5a7 --- /dev/null +++ b/tests-system/checks-error/foo.rsl @@ -0,0 +1,13 @@ +package Foo + +type T { + a String + b String + c String +} + +checks T { + len(a) > 3, error "a must be longer than 3", a + len(b) > 7, "b must be longer than 7", b + len(c) > 10, "c must be longer than 10", c +} diff --git a/tests-system/checks-error/foo.trlc b/tests-system/checks-error/foo.trlc new file mode 100644 index 00000000..359be741 --- /dev/null +++ b/tests-system/checks-error/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Test { + a = "po" + b = "potato" + c = "potatoes" +} diff --git a/tests-system/checks-error/output b/tests-system/checks-error/output new file mode 100644 index 00000000..4cf00dff --- /dev/null +++ b/tests-system/checks-error/output @@ -0,0 +1,7 @@ +a = "po" + ^^^^ checks-error/foo.trlc:4: check error: a must be longer than 3 +b = "potato" + ^^^^^^^^ checks-error/foo.trlc:5: check error: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ checks-error/foo.trlc:6: check error: c must be longer than 10 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 error(s) diff --git a/tests-system/checks-error/output.brief b/tests-system/checks-error/output.brief new file mode 100644 index 00000000..72fc70b7 --- /dev/null +++ b/tests-system/checks-error/output.brief @@ -0,0 +1,3 @@ +checks-error/foo.trlc:4:9: trlc check error: a must be longer than 3 +checks-error/foo.trlc:5:9: trlc check error: b must be longer than 7 +checks-error/foo.trlc:6:9: trlc check error: c must be longer than 10 diff --git a/tests-system/checks-error/output.json b/tests-system/checks-error/output.json new file mode 100644 index 00000000..4cf00dff --- /dev/null +++ b/tests-system/checks-error/output.json @@ -0,0 +1,7 @@ +a = "po" + ^^^^ checks-error/foo.trlc:4: check error: a must be longer than 3 +b = "potato" + ^^^^^^^^ checks-error/foo.trlc:5: check error: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ checks-error/foo.trlc:6: check error: c must be longer than 10 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 error(s) diff --git a/tests-system/checks-error/output.smtlib b/tests-system/checks-error/output.smtlib new file mode 100644 index 00000000..4cf00dff --- /dev/null +++ b/tests-system/checks-error/output.smtlib @@ -0,0 +1,7 @@ +a = "po" + ^^^^ checks-error/foo.trlc:4: check error: a must be longer than 3 +b = "potato" + ^^^^^^^^ checks-error/foo.trlc:5: check error: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ checks-error/foo.trlc:6: check error: c must be longer than 10 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 error(s) diff --git a/tests-system/checks-error/tracing b/tests-system/checks-error/tracing new file mode 100644 index 00000000..e278c5f2 --- /dev/null +++ b/tests-system/checks-error/tracing @@ -0,0 +1 @@ +LRM.Check_Severity diff --git a/tests-system/checks-fatal/foo.rsl b/tests-system/checks-fatal/foo.rsl new file mode 100644 index 00000000..3cff4469 --- /dev/null +++ b/tests-system/checks-fatal/foo.rsl @@ -0,0 +1,13 @@ +package Foo + +type T { + a String + b String + c String +} + +checks T { + len(a) > 3, fatal "a must be longer than 3", a + len(b) > 7, "b must be longer than 7", b + len(c) > 10, "c must be longer than 10", c +} diff --git a/tests-system/checks-fatal/foo.trlc b/tests-system/checks-fatal/foo.trlc new file mode 100644 index 00000000..359be741 --- /dev/null +++ b/tests-system/checks-fatal/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Test { + a = "po" + b = "potato" + c = "potatoes" +} diff --git a/tests-system/checks-fatal/output b/tests-system/checks-fatal/output new file mode 100644 index 00000000..5d672723 --- /dev/null +++ b/tests-system/checks-fatal/output @@ -0,0 +1,3 @@ +a = "po" + ^^^^ checks-fatal/foo.trlc:4: check error: a must be longer than 3 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/checks-fatal/output.brief b/tests-system/checks-fatal/output.brief new file mode 100644 index 00000000..64a2fa3f --- /dev/null +++ b/tests-system/checks-fatal/output.brief @@ -0,0 +1 @@ +checks-fatal/foo.trlc:4:9: trlc check error: a must be longer than 3 diff --git a/tests-system/checks-fatal/output.json b/tests-system/checks-fatal/output.json new file mode 100644 index 00000000..5d672723 --- /dev/null +++ b/tests-system/checks-fatal/output.json @@ -0,0 +1,3 @@ +a = "po" + ^^^^ checks-fatal/foo.trlc:4: check error: a must be longer than 3 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/checks-fatal/output.smtlib b/tests-system/checks-fatal/output.smtlib new file mode 100644 index 00000000..5d672723 --- /dev/null +++ b/tests-system/checks-fatal/output.smtlib @@ -0,0 +1,3 @@ +a = "po" + ^^^^ checks-fatal/foo.trlc:4: check error: a must be longer than 3 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/checks-fatal/tracing b/tests-system/checks-fatal/tracing new file mode 100644 index 00000000..e278c5f2 --- /dev/null +++ b/tests-system/checks-fatal/tracing @@ -0,0 +1 @@ +LRM.Check_Severity diff --git a/tests-system/checks-warning/foo.rsl b/tests-system/checks-warning/foo.rsl new file mode 100644 index 00000000..beb96f55 --- /dev/null +++ b/tests-system/checks-warning/foo.rsl @@ -0,0 +1,13 @@ +package Foo + +type T { + a String + b String + c String +} + +checks T { + len(a) > 3, warning "a must be longer than 3", a + len(b) > 7, warning "b must be longer than 7", b + len(c) > 10, warning "c must be longer than 10", c +} diff --git a/tests-system/checks-warning/foo.trlc b/tests-system/checks-warning/foo.trlc new file mode 100644 index 00000000..359be741 --- /dev/null +++ b/tests-system/checks-warning/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Test { + a = "po" + b = "potato" + c = "potatoes" +} diff --git a/tests-system/checks-warning/output b/tests-system/checks-warning/output new file mode 100644 index 00000000..32ac085f --- /dev/null +++ b/tests-system/checks-warning/output @@ -0,0 +1,7 @@ +a = "po" + ^^^^ checks-warning/foo.trlc:4: check warning: a must be longer than 3 +b = "potato" + ^^^^^^^^ checks-warning/foo.trlc:5: check warning: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ checks-warning/foo.trlc:6: check warning: c must be longer than 10 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s) diff --git a/tests-system/checks-warning/output.brief b/tests-system/checks-warning/output.brief new file mode 100644 index 00000000..3c0f5b56 --- /dev/null +++ b/tests-system/checks-warning/output.brief @@ -0,0 +1,3 @@ +checks-warning/foo.trlc:4:9: trlc check warning: a must be longer than 3 +checks-warning/foo.trlc:5:9: trlc check warning: b must be longer than 7 +checks-warning/foo.trlc:6:9: trlc check warning: c must be longer than 10 diff --git a/tests-system/checks-warning/output.json b/tests-system/checks-warning/output.json new file mode 100644 index 00000000..e4c109e5 --- /dev/null +++ b/tests-system/checks-warning/output.json @@ -0,0 +1,14 @@ +a = "po" + ^^^^ checks-warning/foo.trlc:4: check warning: a must be longer than 3 +b = "potato" + ^^^^^^^^ checks-warning/foo.trlc:5: check warning: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ checks-warning/foo.trlc:6: check warning: c must be longer than 10 +{ + "Test": { + "a": "po", + "b": "potato", + "c": "potatoes" + } +} +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s) diff --git a/tests-system/checks-warning/output.smtlib b/tests-system/checks-warning/output.smtlib new file mode 100644 index 00000000..32ac085f --- /dev/null +++ b/tests-system/checks-warning/output.smtlib @@ -0,0 +1,7 @@ +a = "po" + ^^^^ checks-warning/foo.trlc:4: check warning: a must be longer than 3 +b = "potato" + ^^^^^^^^ checks-warning/foo.trlc:5: check warning: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ checks-warning/foo.trlc:6: check warning: c must be longer than 10 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s) diff --git a/tests-system/checks-warning/tracing b/tests-system/checks-warning/tracing new file mode 100644 index 00000000..e278c5f2 --- /dev/null +++ b/tests-system/checks-warning/tracing @@ -0,0 +1 @@ +LRM.Check_Severity diff --git a/tests-system/simple/foo.rsl b/tests-system/simple/foo.rsl new file mode 100644 index 00000000..570d6cee --- /dev/null +++ b/tests-system/simple/foo.rsl @@ -0,0 +1,9 @@ +package foo + +type MyType { + name String +} + +checks MyType { + len(name) > 10, warning "name is too short", name +} diff --git a/tests-system/simple/instances.trlc b/tests-system/simple/instances.trlc index 8dace288..4915a81b 100644 --- a/tests-system/simple/instances.trlc +++ b/tests-system/simple/instances.trlc @@ -1,6 +1,11 @@ package instances import bar +import foo bar.MyType SomeThing { name = "Qbert" // does start with Q } + +foo.MyType OtherThing { + name = "long enough" +} diff --git a/tests-system/simple/output b/tests-system/simple/output index 2caadc10..72fa9b7b 100644 --- a/tests-system/simple/output +++ b/tests-system/simple/output @@ -1,3 +1,3 @@ checks MyType { ^^^^^^ simple/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] -Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) +Processed 2 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) diff --git a/tests-system/simple/output.json b/tests-system/simple/output.json index c1085680..7bc74ba9 100644 --- a/tests-system/simple/output.json +++ b/tests-system/simple/output.json @@ -1,6 +1,9 @@ { + "OtherThing": { + "name": "long enough" + }, "SomeThing": { "name": "Qbert" } } -Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found no issues +Processed 2 model(s), 1 check(s) and 1 requirement file(s) and found no issues diff --git a/tests-system/simple/output.smtlib b/tests-system/simple/output.smtlib index 2caadc10..72fa9b7b 100644 --- a/tests-system/simple/output.smtlib +++ b/tests-system/simple/output.smtlib @@ -1,3 +1,3 @@ checks MyType { ^^^^^^ simple/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] -Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) +Processed 2 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) diff --git a/tests-system/simple/tracing b/tests-system/simple/tracing index b6ac5987..6604db35 100644 --- a/tests-system/simple/tracing +++ b/tests-system/simple/tracing @@ -2,3 +2,4 @@ LRM.Layout LRM.File_Parsing_Order LRM.Preamble LRM.RSL_File +LRM.Check_Block diff --git a/trlc/ast.py b/trlc/ast.py index 080c1cd7..c747973c 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -190,6 +190,7 @@ def __init__(self, location, n_typ): self.checks = [] def add_check(self, n_check): + # lobster-trace: LRM.Check_Evaluation_Order assert isinstance(n_check, Check) self.checks.append(n_check) @@ -363,6 +364,8 @@ def get_real_location(self, composite_object): return fields[self.n_anchor.name].location def perform(self, mh, composite_object): + # lobster-trace: LRM.Check_Messages + # lobster-trace: LRM.Check_Severity assert isinstance(mh, Message_Handler) assert isinstance(composite_object, (Record_Object, Tuple_Aggregate)) diff --git a/trlc/parser.py b/trlc/parser.py index 3db7c648..00d2ef20 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -1237,8 +1237,11 @@ def parse_name(self, scope): return n_name def parse_check_block(self): + # lobster-trace: LRM.Check_Block self.match_kw("checks") self.match("IDENTIFIER") + # lobster-trace: LRM.Applicable_Types + # lobster-trace: LRM.Applicable_Components n_ctype = self.cu.package.symbols.lookup(self.mh, self.ct, ast.Composite_Type) @@ -1249,6 +1252,7 @@ def parse_check_block(self): scope.push(self.cu.package.symbols) scope.push(n_ctype.components) self.match("C_BRA") + # lobster-trace: LRM.Check_Evaluation_Order_For_Extensions while not self.peek("C_KET"): c_expr = self.parse_expression(scope) if not isinstance(c_expr.typ, ast.Builtin_Boolean):