Tracing/chapter 20 (#44)

Co-authored-by: christophkloeffel <[email protected]>

tests-system/rbt-restricted-null-1/foo.rsl

@@ -0,0 +1,14 @@
+package Foo
+
+type T {
+    a optional Integer
+    b optional Integer
+    d optional Integer
+}
+
+checks T {
+    a != null, "a is null", a
+    a == null, "a is not null", a
+    null == null, "null is not null"
+    d == null, "d is not null", d
+}

tests-system/rbt-restricted-null-1/foo.trlc

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

tests-system/rbt-restricted-null-1/output

@@ -0,0 +1,5 @@
+null == null, "null is not null"
+     ^^ rbt-restricted-null-1/foo.rsl:12: issue: expression is always true [vcg-always-true]
+a = 1
+    ^ rbt-restricted-null-1/foo.trlc:4: check error: a is not null
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s)

tests-system/rbt-restricted-null-1/output.brief

@@ -0,0 +1 @@
+rbt-restricted-null-1/foo.trlc:4:9: trlc check error: a is not null

tests-system/rbt-restricted-null-1/output.json

@@ -0,0 +1,3 @@
+a = 1
+    ^ rbt-restricted-null-1/foo.trlc:4: check error: a is not null
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s)

tests-system/rbt-restricted-null-1/output.smtlib

@@ -0,0 +1,5 @@
+null == null, "null is not null"
+     ^^ rbt-restricted-null-1/foo.rsl:12: issue: expression is always true [vcg-always-true]
+a = 1
+    ^ rbt-restricted-null-1/foo.trlc:4: check error: a is not null
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s)

tests-system/rbt-restricted-null-1/tracing

@@ -0,0 +1,2 @@
+LRM.Null_Equivalence
+LRM.Unspecified_Optional_Components

tests-system/rbt-restricted-null-2/foo.rsl

@@ -0,0 +1,19 @@
+package Foo
+
+type A {
+    a optional Integer
+    b optional Integer
+}
+
+type T {
+    c optional Integer
+    d optional Integer
+}
+
+checks A {
+    (a + b) > null, "(a+b) < null", a
+}
+
+checks T {
+    d == (if c then null else d), "not permitted"
+}

tests-system/rbt-restricted-null-2/foo.trlc

@@ -0,0 +1,5 @@
+package Foo
+
+T Test {
+    c = 3
+}

tests-system/rbt-restricted-null-2/output

@@ -0,0 +1,5 @@
+(a + b) > null, "(a+b) < null", a
+          ^^^^ rbt-restricted-null-2/foo.rsl:14: error: null is not permitted here
+d == (if c then null else d), "not permitted"
+                ^^^^ rbt-restricted-null-2/foo.rsl:18: error: null is not permitted here
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 error(s)

tests-system/rbt-restricted-null-2/output.brief

@@ -0,0 +1,2 @@
+rbt-restricted-null-2/foo.rsl:14:15: trlc error: null is not permitted here
+rbt-restricted-null-2/foo.rsl:18:21: trlc error: null is not permitted here

tests-system/rbt-restricted-null-2/output.json

@@ -0,0 +1,5 @@
+(a + b) > null, "(a+b) < null", a
+          ^^^^ rbt-restricted-null-2/foo.rsl:14: error: null is not permitted here
+d == (if c then null else d), "not permitted"
+                ^^^^ rbt-restricted-null-2/foo.rsl:18: error: null is not permitted here
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 error(s)

tests-system/rbt-restricted-null-2/output.smtlib

@@ -0,0 +1,5 @@
+(a + b) > null, "(a+b) < null", a
+          ^^^^ rbt-restricted-null-2/foo.rsl:14: error: null is not permitted here
+d == (if c then null else d), "not permitted"
+                ^^^^ rbt-restricted-null-2/foo.rsl:18: error: null is not permitted here
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 error(s)

tests-system/rbt-restricted-null-2/tracing

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

trlc/ast.py

@@ -487,6 +487,8 @@ def to_string(self):  # pragma: no cover
             self.__class__.__name__
 
     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,
@@ -550,7 +552,7 @@ class Implicit_Null(Expression):
 
     """
     def __init__(self, composite_object, composite_component):
-        # lobster-exclude: Constructor only declares variables
+        # lobster-trace: LRM.Unspecified_Optional_Components
         assert isinstance(composite_object, (Record_Object,
                                              Tuple_Aggregate))
         assert isinstance(composite_component, Composite_Component)
@@ -560,6 +562,7 @@ def to_string(self):
         return "null"
 
     def evaluate(self, mh, context):
+        # lobster-trace: LRM.Unspecified_Optional_Components
         assert isinstance(mh, Message_Handler)
         assert context is None or isinstance(context, dict)
         return Value(self.location, None, None)
@@ -942,6 +945,7 @@ class Tuple_Aggregate(Expression):
 
     """
     def __init__(self, location, typ):
+        # lobster-trace: LRM.Unspecified_Optional_Components
         super().__init__(location, typ)
         self.value = {n_field.name : Implicit_Null(self, n_field)
                       for n_field in self.typ.components.values()}
@@ -1223,6 +1227,7 @@ def dump(self, indent=0):  # pragma: no cover
         self.n_operand.dump(indent + 1)
 
     def evaluate(self, mh, context):
+        # lobster-trace: LRM.Null_Is_Invalid
         assert isinstance(mh, Message_Handler)
         assert context is None or isinstance(context, dict)
 
@@ -1457,6 +1462,8 @@ def to_string(self):
             assert False
 
     def evaluate(self, mh, context):
+        # lobster-trace: LRM.Null_Equivalence
+        # lobster-trace: LRM.Null_Is_Invalid
         assert isinstance(mh, Message_Handler)
         assert context is None or isinstance(context, dict)
 
@@ -1758,6 +1765,7 @@ def dump(self, indent=0):  # pragma: no cover
         self.n_upper.dump(indent + 1)
 
     def evaluate(self, mh, context):
+        # lobster-trace: LRM.Null_Is_Invalid
         assert isinstance(mh, Message_Handler)
         assert context is None or isinstance(context, dict)
 
@@ -1911,6 +1919,7 @@ def to_string(self):
     def evaluate(self, mh, context):
         # lobster-trace: LRM.Conditional_Expression_Else
         # lobster-trace: LRM.Conditional_Expression_Evaluation
+        # lobster-trace: LRM.Null_Is_Invalid
         assert isinstance(mh, Message_Handler)
         assert context is None or isinstance(context, dict)
 
@@ -1996,6 +2005,7 @@ def to_string(self):
                                         self.n_expr.to_string())
 
     def evaluate(self, mh, context):
+        # lobster-trace: LRM.Null_Is_Invalid
         assert isinstance(mh, Message_Handler)
         assert context is None or isinstance(context, dict)
 
@@ -2832,6 +2842,7 @@ class Record_Object(Typed_Entity):
     """
     def __init__(self, name, location, n_typ, section, n_package):
         # lobster-trace: LRM.Section_Declaration
+        # lobster-trace: LRM.Unspecified_Optional_Components
         assert isinstance(n_typ, Record_Type)
         assert isinstance(section, Section) or section is None
         assert isinstance(n_package, Package)

trlc/parser.py

@@ -967,6 +967,7 @@ def parse_quantified_expression(self, scope):
 
     def parse_conditional_expression(self, scope):
         # lobster-trace: LRM.Conditional_Expression
+        # lobster-trace: LRM.Restricted_Null
         assert isinstance(scope, ast.Scope)
 
         self.match_kw("if")