Skip to content

Commit

Permalink
adds tracing for names (bmw-software-engineering#66)
Browse files Browse the repository at this point in the history
adds tracing for chapter 12
  • Loading branch information
christophkloeffel authored Oct 15, 2024
1 parent e316003 commit b22befc
Show file tree
Hide file tree
Showing 108 changed files with 564 additions and 4 deletions.
4 changes: 0 additions & 4 deletions language-reference-manual/lrm.trlc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
9 changes: 9 additions & 0 deletions tests-system/rbt-endswith-semantics/foo.rsl
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
package Foo

type T {
b String
}

checks T {
endswith(b, "en"), warning "b should end with en", b
}
5 changes: 5 additions & 0 deletions tests-system/rbt-endswith-semantics/foo.trlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
package Foo

T Bar {
b = "kitten"
}
1 change: 1 addition & 0 deletions tests-system/rbt-endswith-semantics/output
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Processed 1 model and 1 requirement file and found no issues
Empty file.
6 changes: 6 additions & 0 deletions tests-system/rbt-endswith-semantics/output.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
{
"Bar": {
"b": "kitten"
}
}
Processed 1 model and 1 requirement file and found no issues
1 change: 1 addition & 0 deletions tests-system/rbt-endswith-semantics/output.smtlib
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Processed 1 model and 1 requirement file and found no issues
12 changes: 12 additions & 0 deletions tests-system/rbt-len-semantics/foo.rsl
Original file line number Diff line number Diff line change
@@ -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"
}
7 changes: 7 additions & 0 deletions tests-system/rbt-len-semantics/foo.trlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package Foo

T Bar {
a = "potato"
b = 1
c = [2,1]
}
1 change: 1 addition & 0 deletions tests-system/rbt-len-semantics/output
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Processed 1 model and 1 requirement file and found no issues
Empty file.
11 changes: 11 additions & 0 deletions tests-system/rbt-len-semantics/output.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"Bar": {
"a": "potato",
"b": 1,
"c": [
2,
1
]
}
}
Processed 1 model and 1 requirement file and found no issues
1 change: 1 addition & 0 deletions tests-system/rbt-len-semantics/output.smtlib
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Processed 1 model and 1 requirement file and found no issues
11 changes: 11 additions & 0 deletions tests-system/rbt-matches-semantics/foo.rsl
Original file line number Diff line number Diff line change
@@ -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
}
7 changes: 7 additions & 0 deletions tests-system/rbt-matches-semantics/foo.trlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package Foo

T Bar {
a = "potato"
b = "kitten"
c = 1
}
1 change: 1 addition & 0 deletions tests-system/rbt-matches-semantics/output
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Processed 1 model and 1 requirement file and found no issues
Empty file.
8 changes: 8 additions & 0 deletions tests-system/rbt-matches-semantics/output.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
{
"Bar": {
"a": "potato",
"b": "kitten",
"c": 1
}
}
Processed 1 model and 1 requirement file and found no issues
1 change: 1 addition & 0 deletions tests-system/rbt-matches-semantics/output.smtlib
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Processed 1 model and 1 requirement file and found no issues
25 changes: 25 additions & 0 deletions tests-system/rbt-names/foo.rsl
Original file line number Diff line number Diff line change
@@ -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
}
7 changes: 7 additions & 0 deletions tests-system/rbt-names/foo.trlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package Foo

Bar potato {
e = E.A
t = 1@2
b = [1,2,3,4,5,6]
}
3 changes: 3 additions & 0 deletions tests-system/rbt-names/output
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions tests-system/rbt-names/output.brief
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rbt-names/foo.trlc:6:9: trlc check warning: try to minimize the length
20 changes: 20 additions & 0 deletions tests-system/rbt-names/output.json
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions tests-system/rbt-names/output.smtlib
Original file line number Diff line number Diff line change
@@ -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
12 changes: 12 additions & 0 deletions tests-system/rbt-signature-len-1/foo.rsl
Original file line number Diff line number Diff line change
@@ -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"
}
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-len-1/output
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions tests-system/rbt-signature-len-1/output.brief
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rbt-signature-len-1/foo.rsl:11:9: trlc error: expected expression of type Array_Type, got Builtin_Integer instead
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-len-1/output.json
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-len-1/output.smtlib
Original file line number Diff line number Diff line change
@@ -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
13 changes: 13 additions & 0 deletions tests-system/rbt-signature-len-2/foo.rsl
Original file line number Diff line number Diff line change
@@ -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"
}
7 changes: 7 additions & 0 deletions tests-system/rbt-signature-len-2/foo.trlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package Foo

T Bar {
a = "potato"
b = 1
c = [2,1]
}
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-len-2/output
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions tests-system/rbt-signature-len-2/output.brief
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rbt-signature-len-2/foo.rsl:12:5: trlc error: function requires 1 parameters
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-len-2/output.json
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-len-2/output.smtlib
Original file line number Diff line number Diff line change
@@ -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
11 changes: 11 additions & 0 deletions tests-system/rbt-signature-matches-1/foo.rsl
Original file line number Diff line number Diff line change
@@ -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
}
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-matches-1/output
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions tests-system/rbt-signature-matches-1/output.brief
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rbt-signature-matches-1/foo.rsl:10:13: trlc error: expected expression of type Builtin_String, got Builtin_Integer instead
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-matches-1/output.json
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-matches-1/output.smtlib
Original file line number Diff line number Diff line change
@@ -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
11 changes: 11 additions & 0 deletions tests-system/rbt-signature-matches-2/foo.rsl
Original file line number Diff line number Diff line change
@@ -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
}
7 changes: 7 additions & 0 deletions tests-system/rbt-signature-matches-2/foo.trlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package Foo

T Bar {
a = "potato"
b = "kitten"
c = 1
}
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-matches-2/output
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions tests-system/rbt-signature-matches-2/output.brief
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rbt-signature-matches-2/foo.rsl:10:5: trlc error: function requires 2 parameters
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-matches-2/output.json
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-matches-2/output.smtlib
Original file line number Diff line number Diff line change
@@ -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
11 changes: 11 additions & 0 deletions tests-system/rbt-signature-matches-3/foo.rsl
Original file line number Diff line number Diff line change
@@ -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
}
7 changes: 7 additions & 0 deletions tests-system/rbt-signature-matches-3/foo.trlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package Foo

T Bar {
a = "(abc(def)"
b = "kitten"
c = 1
}
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-matches-3/output
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions tests-system/rbt-signature-matches-3/output.brief
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rbt-signature-matches-3/foo.rsl:10:16: trlc error: missing ), unterminated subpattern at position 0
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-matches-3/output.json
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-matches-3/output.smtlib
Original file line number Diff line number Diff line change
@@ -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
14 changes: 14 additions & 0 deletions tests-system/rbt-signature-string-end-functions-1/foo.rsl
Original file line number Diff line number Diff line change
@@ -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
}
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-string-end-functions-1/output
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-string-end-functions-1/output.json
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -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
14 changes: 14 additions & 0 deletions tests-system/rbt-signature-string-end-functions-2/foo.rsl
Original file line number Diff line number Diff line change
@@ -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
}
7 changes: 7 additions & 0 deletions tests-system/rbt-signature-string-end-functions-2/foo.trlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package Foo

T Bar {
a = "potato"
b = "kitten"
c = 1
}
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-string-end-functions-2/output
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rbt-signature-string-end-functions-2/foo.rsl:13:5: trlc error: function requires 2 parameters
3 changes: 3 additions & 0 deletions tests-system/rbt-signature-string-end-functions-2/output.json
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -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
Loading

0 comments on commit b22befc

Please sign in to comment.