adds tracing for checks

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"
   }
 
 }

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
+}

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)

tests-system/checks-10/output.brief

@@ -0,0 +1 @@
+checks-10/foo.rsl:9:9: trlc error: unknown symbol c

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)

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)

tests-system/checks-10/tracing

@@ -0,0 +1 @@
+LRM.Applicable_Components

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"
+}

tests-system/checks-11/foo.trlc

@@ -0,0 +1,6 @@
+package Foo
+
+T Bar {
+  a = 1
+  b = -1
+}

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)

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

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)

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)

tests-system/checks-11/tracing

@@ -0,0 +1 @@
+LRM.Check_Evaluation_Order

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
+}

tests-system/checks-12/bar.trlc

@@ -0,0 +1,6 @@
+package Bar
+
+T Test {
+    a = "potato"
+    b = "more potatoes"
+}

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
+}

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)

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

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)

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)

tests-system/checks-12/tracing

@@ -0,0 +1,2 @@
+LRM.Check_Evaluation_Order_For_Extensions
+LRM.Check_Messages

tests-system/checks-9/bar.rsl

@@ -0,0 +1,5 @@
+package Bar
+
+type B {
+    a String
+}

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
+}

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)

tests-system/checks-9/output.brief

@@ -0,0 +1 @@
+checks-9/foo.rsl:8:8: trlc error: unknown symbol 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)

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)

tests-system/checks-9/tracing

@@ -0,0 +1 @@
+LRM.Applicable_Types

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
+}

tests-system/checks-error/foo.trlc

@@ -0,0 +1,7 @@
+package Foo
+
+T Test {
+    a = "po"
+    b = "potato"
+    c = "potatoes"
+}

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)

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

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)

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)

tests-system/checks-error/tracing

@@ -0,0 +1 @@
+LRM.Check_Severity

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
+}

tests-system/checks-fatal/foo.trlc

@@ -0,0 +1,7 @@
+package Foo
+
+T Test {
+    a = "po"
+    b = "potato"
+    c = "potatoes"
+}

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)

tests-system/checks-fatal/output.brief

@@ -0,0 +1 @@
+checks-fatal/foo.trlc:4:9: trlc check error: a must be longer than 3

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)

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)

tests-system/checks-fatal/tracing

@@ -0,0 +1 @@
+LRM.Check_Severity

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
+}

tests-system/checks-warning/foo.trlc

@@ -0,0 +1,7 @@
+package Foo
+
+T Test {
+    a = "po"
+    b = "potato"
+    c = "potatoes"
+}

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)

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

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)

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)

tests-system/checks-warning/tracing

@@ -0,0 +1 @@
+LRM.Check_Severity

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
+}

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"
+}

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)

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

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)

tests-system/simple/tracing

@@ -2,3 +2,4 @@ LRM.Layout
 LRM.File_Parsing_Order
 LRM.Preamble
 LRM.RSL_File
+LRM.Check_Block

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))