diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index 5c927315..290888be 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.''' diff --git a/tests-system/rbt-applicable-components/foo.rsl b/tests-system/rbt-applicable-components/foo.rsl new file mode 100644 index 00000000..cf88f135 --- /dev/null +++ b/tests-system/rbt-applicable-components/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/rbt-applicable-components/output b/tests-system/rbt-applicable-components/output new file mode 100644 index 00000000..9fca2495 --- /dev/null +++ b/tests-system/rbt-applicable-components/output @@ -0,0 +1,3 @@ +len(c) > 10, "c is too short", c + ^ rbt-applicable-components/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/rbt-applicable-components/output.brief b/tests-system/rbt-applicable-components/output.brief new file mode 100644 index 00000000..5fc6908a --- /dev/null +++ b/tests-system/rbt-applicable-components/output.brief @@ -0,0 +1 @@ +rbt-applicable-components/foo.rsl:9:9: trlc error: unknown symbol c diff --git a/tests-system/rbt-applicable-components/output.json b/tests-system/rbt-applicable-components/output.json new file mode 100644 index 00000000..9fca2495 --- /dev/null +++ b/tests-system/rbt-applicable-components/output.json @@ -0,0 +1,3 @@ +len(c) > 10, "c is too short", c + ^ rbt-applicable-components/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/rbt-applicable-components/output.smtlib b/tests-system/rbt-applicable-components/output.smtlib new file mode 100644 index 00000000..9fca2495 --- /dev/null +++ b/tests-system/rbt-applicable-components/output.smtlib @@ -0,0 +1,3 @@ +len(c) > 10, "c is too short", c + ^ rbt-applicable-components/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/rbt-applicable-types/bar.rsl b/tests-system/rbt-applicable-types/bar.rsl new file mode 100644 index 00000000..5898c979 --- /dev/null +++ b/tests-system/rbt-applicable-types/bar.rsl @@ -0,0 +1,5 @@ +package Bar + +type B { + a String +} diff --git a/tests-system/rbt-applicable-types/foo.rsl b/tests-system/rbt-applicable-types/foo.rsl new file mode 100644 index 00000000..a8b1b2de --- /dev/null +++ b/tests-system/rbt-applicable-types/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/rbt-applicable-types/output b/tests-system/rbt-applicable-types/output new file mode 100644 index 00000000..270ebd4c --- /dev/null +++ b/tests-system/rbt-applicable-types/output @@ -0,0 +1,3 @@ +checks B { + ^ rbt-applicable-types/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/rbt-applicable-types/output.brief b/tests-system/rbt-applicable-types/output.brief new file mode 100644 index 00000000..de9b8583 --- /dev/null +++ b/tests-system/rbt-applicable-types/output.brief @@ -0,0 +1 @@ +rbt-applicable-types/foo.rsl:8:8: trlc error: unknown symbol B diff --git a/tests-system/rbt-applicable-types/output.json b/tests-system/rbt-applicable-types/output.json new file mode 100644 index 00000000..270ebd4c --- /dev/null +++ b/tests-system/rbt-applicable-types/output.json @@ -0,0 +1,3 @@ +checks B { + ^ rbt-applicable-types/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/rbt-applicable-types/output.smtlib b/tests-system/rbt-applicable-types/output.smtlib new file mode 100644 index 00000000..270ebd4c --- /dev/null +++ b/tests-system/rbt-applicable-types/output.smtlib @@ -0,0 +1,3 @@ +checks B { + ^ rbt-applicable-types/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/rbt-check-evaluation-order-for-extensions/bar.rsl b/tests-system/rbt-check-evaluation-order-for-extensions/bar.rsl new file mode 100644 index 00000000..829805f6 --- /dev/null +++ b/tests-system/rbt-check-evaluation-order-for-extensions/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/rbt-check-evaluation-order-for-extensions/bar.trlc b/tests-system/rbt-check-evaluation-order-for-extensions/bar.trlc new file mode 100644 index 00000000..60faaa18 --- /dev/null +++ b/tests-system/rbt-check-evaluation-order-for-extensions/bar.trlc @@ -0,0 +1,6 @@ +package Bar + +T Test { + a = "potato" + b = "more potatoes" +} diff --git a/tests-system/rbt-check-evaluation-order-for-extensions/foo.rsl b/tests-system/rbt-check-evaluation-order-for-extensions/foo.rsl new file mode 100644 index 00000000..d09d18ae --- /dev/null +++ b/tests-system/rbt-check-evaluation-order-for-extensions/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/rbt-check-evaluation-order-for-extensions/output b/tests-system/rbt-check-evaluation-order-for-extensions/output new file mode 100644 index 00000000..f90fd687 --- /dev/null +++ b/tests-system/rbt-check-evaluation-order-for-extensions/output @@ -0,0 +1,5 @@ +a = "potato" + ^^^^^^^^ rbt-check-evaluation-order-for-extensions/bar.trlc:4: check warning: a has to be more than 7 chars +a = "potato" + ^^^^^^^^ rbt-check-evaluation-order-for-extensions/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/rbt-check-evaluation-order-for-extensions/output.brief b/tests-system/rbt-check-evaluation-order-for-extensions/output.brief new file mode 100644 index 00000000..2bad5b36 --- /dev/null +++ b/tests-system/rbt-check-evaluation-order-for-extensions/output.brief @@ -0,0 +1,2 @@ +rbt-check-evaluation-order-for-extensions/bar.trlc:4:9: trlc check warning: a has to be more than 7 chars +rbt-check-evaluation-order-for-extensions/bar.trlc:4:9: trlc check error: a has to be more than 10 chars diff --git a/tests-system/rbt-check-evaluation-order-for-extensions/output.json b/tests-system/rbt-check-evaluation-order-for-extensions/output.json new file mode 100644 index 00000000..f90fd687 --- /dev/null +++ b/tests-system/rbt-check-evaluation-order-for-extensions/output.json @@ -0,0 +1,5 @@ +a = "potato" + ^^^^^^^^ rbt-check-evaluation-order-for-extensions/bar.trlc:4: check warning: a has to be more than 7 chars +a = "potato" + ^^^^^^^^ rbt-check-evaluation-order-for-extensions/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/rbt-check-evaluation-order-for-extensions/output.smtlib b/tests-system/rbt-check-evaluation-order-for-extensions/output.smtlib new file mode 100644 index 00000000..f90fd687 --- /dev/null +++ b/tests-system/rbt-check-evaluation-order-for-extensions/output.smtlib @@ -0,0 +1,5 @@ +a = "potato" + ^^^^^^^^ rbt-check-evaluation-order-for-extensions/bar.trlc:4: check warning: a has to be more than 7 chars +a = "potato" + ^^^^^^^^ rbt-check-evaluation-order-for-extensions/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/rbt-check-evaluation-order-for-extensions/tracing b/tests-system/rbt-check-evaluation-order-for-extensions/tracing new file mode 100644 index 00000000..f8361b5a --- /dev/null +++ b/tests-system/rbt-check-evaluation-order-for-extensions/tracing @@ -0,0 +1 @@ +LRM.Check_Messages diff --git a/tests-system/rbt-check-evaluation-order/foo.rsl b/tests-system/rbt-check-evaluation-order/foo.rsl new file mode 100644 index 00000000..31a819a5 --- /dev/null +++ b/tests-system/rbt-check-evaluation-order/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/rbt-check-evaluation-order/foo.trlc b/tests-system/rbt-check-evaluation-order/foo.trlc new file mode 100644 index 00000000..f628a73e --- /dev/null +++ b/tests-system/rbt-check-evaluation-order/foo.trlc @@ -0,0 +1,6 @@ +package Foo + +T Bar { + a = 1 + b = -1 +} diff --git a/tests-system/rbt-check-evaluation-order/output b/tests-system/rbt-check-evaluation-order/output new file mode 100644 index 00000000..4de1455f --- /dev/null +++ b/tests-system/rbt-check-evaluation-order/output @@ -0,0 +1,7 @@ +a = 1 + ^ rbt-check-evaluation-order/foo.trlc:4: check warning: First warning: a is positive +b = -1 + ^ rbt-check-evaluation-order/foo.trlc:5: check warning: Second warning: b is negative +T Bar { + ^^^ rbt-check-evaluation-order/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/rbt-check-evaluation-order/output.brief b/tests-system/rbt-check-evaluation-order/output.brief new file mode 100644 index 00000000..86e4d33c --- /dev/null +++ b/tests-system/rbt-check-evaluation-order/output.brief @@ -0,0 +1,3 @@ +rbt-check-evaluation-order/foo.trlc:4:7: trlc check warning: First warning: a is positive +rbt-check-evaluation-order/foo.trlc:5:7: trlc check warning: Second warning: b is negative +rbt-check-evaluation-order/foo.trlc:3:3: trlc check warning: Third warning: a is greater than b diff --git a/tests-system/rbt-check-evaluation-order/output.json b/tests-system/rbt-check-evaluation-order/output.json new file mode 100644 index 00000000..c8b810be --- /dev/null +++ b/tests-system/rbt-check-evaluation-order/output.json @@ -0,0 +1,13 @@ +a = 1 + ^ rbt-check-evaluation-order/foo.trlc:4: check warning: First warning: a is positive +b = -1 + ^ rbt-check-evaluation-order/foo.trlc:5: check warning: Second warning: b is negative +T Bar { + ^^^ rbt-check-evaluation-order/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/rbt-check-evaluation-order/output.smtlib b/tests-system/rbt-check-evaluation-order/output.smtlib new file mode 100644 index 00000000..4de1455f --- /dev/null +++ b/tests-system/rbt-check-evaluation-order/output.smtlib @@ -0,0 +1,7 @@ +a = 1 + ^ rbt-check-evaluation-order/foo.trlc:4: check warning: First warning: a is positive +b = -1 + ^ rbt-check-evaluation-order/foo.trlc:5: check warning: Second warning: b is negative +T Bar { + ^^^ rbt-check-evaluation-order/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/rbt-check-severity-1/foo.rsl b/tests-system/rbt-check-severity-1/foo.rsl new file mode 100644 index 00000000..1271d5a7 --- /dev/null +++ b/tests-system/rbt-check-severity-1/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/rbt-check-severity-1/foo.trlc b/tests-system/rbt-check-severity-1/foo.trlc new file mode 100644 index 00000000..359be741 --- /dev/null +++ b/tests-system/rbt-check-severity-1/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Test { + a = "po" + b = "potato" + c = "potatoes" +} diff --git a/tests-system/rbt-check-severity-1/output b/tests-system/rbt-check-severity-1/output new file mode 100644 index 00000000..707371b9 --- /dev/null +++ b/tests-system/rbt-check-severity-1/output @@ -0,0 +1,7 @@ +a = "po" + ^^^^ rbt-check-severity-1/foo.trlc:4: check error: a must be longer than 3 +b = "potato" + ^^^^^^^^ rbt-check-severity-1/foo.trlc:5: check error: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ rbt-check-severity-1/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/rbt-check-severity-1/output.brief b/tests-system/rbt-check-severity-1/output.brief new file mode 100644 index 00000000..f93cb0ed --- /dev/null +++ b/tests-system/rbt-check-severity-1/output.brief @@ -0,0 +1,3 @@ +rbt-check-severity-1/foo.trlc:4:9: trlc check error: a must be longer than 3 +rbt-check-severity-1/foo.trlc:5:9: trlc check error: b must be longer than 7 +rbt-check-severity-1/foo.trlc:6:9: trlc check error: c must be longer than 10 diff --git a/tests-system/rbt-check-severity-1/output.json b/tests-system/rbt-check-severity-1/output.json new file mode 100644 index 00000000..707371b9 --- /dev/null +++ b/tests-system/rbt-check-severity-1/output.json @@ -0,0 +1,7 @@ +a = "po" + ^^^^ rbt-check-severity-1/foo.trlc:4: check error: a must be longer than 3 +b = "potato" + ^^^^^^^^ rbt-check-severity-1/foo.trlc:5: check error: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ rbt-check-severity-1/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/rbt-check-severity-1/output.smtlib b/tests-system/rbt-check-severity-1/output.smtlib new file mode 100644 index 00000000..707371b9 --- /dev/null +++ b/tests-system/rbt-check-severity-1/output.smtlib @@ -0,0 +1,7 @@ +a = "po" + ^^^^ rbt-check-severity-1/foo.trlc:4: check error: a must be longer than 3 +b = "potato" + ^^^^^^^^ rbt-check-severity-1/foo.trlc:5: check error: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ rbt-check-severity-1/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/rbt-check-severity-2/foo.rsl b/tests-system/rbt-check-severity-2/foo.rsl new file mode 100644 index 00000000..3cff4469 --- /dev/null +++ b/tests-system/rbt-check-severity-2/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/rbt-check-severity-2/foo.trlc b/tests-system/rbt-check-severity-2/foo.trlc new file mode 100644 index 00000000..359be741 --- /dev/null +++ b/tests-system/rbt-check-severity-2/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Test { + a = "po" + b = "potato" + c = "potatoes" +} diff --git a/tests-system/rbt-check-severity-2/output b/tests-system/rbt-check-severity-2/output new file mode 100644 index 00000000..6e25f333 --- /dev/null +++ b/tests-system/rbt-check-severity-2/output @@ -0,0 +1,3 @@ +a = "po" + ^^^^ rbt-check-severity-2/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/rbt-check-severity-2/output.brief b/tests-system/rbt-check-severity-2/output.brief new file mode 100644 index 00000000..701bfbe5 --- /dev/null +++ b/tests-system/rbt-check-severity-2/output.brief @@ -0,0 +1 @@ +rbt-check-severity-2/foo.trlc:4:9: trlc check error: a must be longer than 3 diff --git a/tests-system/rbt-check-severity-2/output.json b/tests-system/rbt-check-severity-2/output.json new file mode 100644 index 00000000..6e25f333 --- /dev/null +++ b/tests-system/rbt-check-severity-2/output.json @@ -0,0 +1,3 @@ +a = "po" + ^^^^ rbt-check-severity-2/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/rbt-check-severity-2/output.smtlib b/tests-system/rbt-check-severity-2/output.smtlib new file mode 100644 index 00000000..6e25f333 --- /dev/null +++ b/tests-system/rbt-check-severity-2/output.smtlib @@ -0,0 +1,3 @@ +a = "po" + ^^^^ rbt-check-severity-2/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/rbt-check-severity-3/foo.rsl b/tests-system/rbt-check-severity-3/foo.rsl new file mode 100644 index 00000000..beb96f55 --- /dev/null +++ b/tests-system/rbt-check-severity-3/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/rbt-check-severity-3/foo.trlc b/tests-system/rbt-check-severity-3/foo.trlc new file mode 100644 index 00000000..359be741 --- /dev/null +++ b/tests-system/rbt-check-severity-3/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Test { + a = "po" + b = "potato" + c = "potatoes" +} diff --git a/tests-system/rbt-check-severity-3/output b/tests-system/rbt-check-severity-3/output new file mode 100644 index 00000000..573f67e1 --- /dev/null +++ b/tests-system/rbt-check-severity-3/output @@ -0,0 +1,7 @@ +a = "po" + ^^^^ rbt-check-severity-3/foo.trlc:4: check warning: a must be longer than 3 +b = "potato" + ^^^^^^^^ rbt-check-severity-3/foo.trlc:5: check warning: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ rbt-check-severity-3/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/rbt-check-severity-3/output.brief b/tests-system/rbt-check-severity-3/output.brief new file mode 100644 index 00000000..038ae7fe --- /dev/null +++ b/tests-system/rbt-check-severity-3/output.brief @@ -0,0 +1,3 @@ +rbt-check-severity-3/foo.trlc:4:9: trlc check warning: a must be longer than 3 +rbt-check-severity-3/foo.trlc:5:9: trlc check warning: b must be longer than 7 +rbt-check-severity-3/foo.trlc:6:9: trlc check warning: c must be longer than 10 diff --git a/tests-system/rbt-check-severity-3/output.json b/tests-system/rbt-check-severity-3/output.json new file mode 100644 index 00000000..4766479d --- /dev/null +++ b/tests-system/rbt-check-severity-3/output.json @@ -0,0 +1,14 @@ +a = "po" + ^^^^ rbt-check-severity-3/foo.trlc:4: check warning: a must be longer than 3 +b = "potato" + ^^^^^^^^ rbt-check-severity-3/foo.trlc:5: check warning: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ rbt-check-severity-3/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/rbt-check-severity-3/output.smtlib b/tests-system/rbt-check-severity-3/output.smtlib new file mode 100644 index 00000000..573f67e1 --- /dev/null +++ b/tests-system/rbt-check-severity-3/output.smtlib @@ -0,0 +1,7 @@ +a = "po" + ^^^^ rbt-check-severity-3/foo.trlc:4: check warning: a must be longer than 3 +b = "potato" + ^^^^^^^^ rbt-check-severity-3/foo.trlc:5: check warning: b must be longer than 7 +c = "potatoes" + ^^^^^^^^^^ rbt-check-severity-3/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/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 3c4844bf..002c42f3 100644 --- a/tests-system/simple/tracing +++ b/tests-system/simple/tracing @@ -4,3 +4,4 @@ LRM.Preamble LRM.RSL_File LRM.Check_File LRM.Deprecated_Check_Files +LRM.Check_Block diff --git a/trlc/ast.py b/trlc/ast.py index 080c1cd7..858fc0a1 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -183,13 +183,14 @@ class Check_Block(Node): """ def __init__(self, location, n_typ): - # lobster-exclude: Constructor only declares variables + # lobster-trace: LRM.Check_Block super().__init__(location) assert isinstance(n_typ, Composite_Type) self.n_typ = 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) @@ -319,7 +320,7 @@ def __init__(self, severity, t_message, extrainfo): - # lobster-exclude: Constructor only declares variables + # lobster-trace: LRM.Check_Block assert isinstance(n_type, Composite_Type) assert isinstance(n_expr, Expression) assert isinstance(n_anchor, Composite_Component) or n_anchor is None @@ -333,6 +334,10 @@ def __init__(self, self.n_expr = n_expr self.n_anchor = n_anchor self.severity = severity + # lobster-trace: LRM.No_Newlines_In_Message + # This is the error recovery strategy if we find newlines in + # the short error messages: we just remove them. The error + # raised is non-fatal. self.message = t_message.value.replace("\n", " ") self.extrainfo = extrainfo @@ -363,6 +368,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)) @@ -2389,13 +2396,16 @@ def __init__(self, self.checks = [] def add_check(self, n_check): + # lobster-trace: LRM.Check_Evaluation_Order assert isinstance(n_check, Check) self.checks.append(n_check) def iter_checks(self): + # lobster-trace: LRM.Check_Evaluation_Order yield from self.checks def all_components(self): + # lobster-exclude: Convenience function """Convenience function to get a list of all components. :rtype: list[Composite_Component] @@ -2495,6 +2505,8 @@ def __init__(self, self.is_abstract = is_abstract def iter_checks(self): + # lobster-trace: LRM.Check_Evaluation_Order + # lobster-trace: LRM.Check_Evaluation_Order_For_Extensions if self.parent: yield from self.parent.iter_checks() yield from self.checks @@ -2651,6 +2663,7 @@ def dump(self, indent=0): # pragma: no cover self.write_indent(indent + 1, "Checks: None") def perform_type_checks(self, mh, value): + # lobster-trace: LRM.Check_Evaluation_Order assert isinstance(mh, Message_Handler) if isinstance(value, Tuple_Aggregate): ok = True @@ -2873,6 +2886,7 @@ def resolve_references(self, mh): val.resolve_references(mh) def perform_checks(self, mh): + # lobster-trace: LRM.Check_Evaluation_Order assert isinstance(mh, Message_Handler) ok = True diff --git a/trlc/parser.py b/trlc/parser.py index dfeb1226..1defed0e 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)