From 9096ff1863b3011a745b220786e366fd3af854f2 Mon Sep 17 00:00:00 2001 From: christophkloeffel Date: Sun, 15 Oct 2023 22:24:31 +0200 Subject: [PATCH 1/2] adds tracing for expressions --- language-reference-manual/lrm.trlc | 1 + tests-system/expressions/foo.rsl | 12 -- tests-system/expressions/output | 171 ------------------ tests-system/expressions/output.brief | 39 ---- tests-system/expressions/output.json | 91 ---------- tests-system/expressions/output.smtlib | 171 ------------------ .../foo.check => rbt-expression/foo.rsl} | 11 ++ .../{expressions => rbt-expression}/foo.trlc | 0 tests-system/rbt-expression/output | 169 +++++++++++++++++ tests-system/rbt-expression/output.brief | 39 ++++ tests-system/rbt-expression/output.json | 91 ++++++++++ tests-system/rbt-expression/output.smtlib | 169 +++++++++++++++++ tests-system/rbt-expression/tracing | 5 + trlc/parser.py | 6 + 14 files changed, 491 insertions(+), 484 deletions(-) delete mode 100644 tests-system/expressions/foo.rsl delete mode 100644 tests-system/expressions/output delete mode 100644 tests-system/expressions/output.brief delete mode 100644 tests-system/expressions/output.json delete mode 100644 tests-system/expressions/output.smtlib rename tests-system/{expressions/foo.check => rbt-expression/foo.rsl} (96%) rename tests-system/{expressions => rbt-expression}/foo.trlc (100%) create mode 100644 tests-system/rbt-expression/output create mode 100644 tests-system/rbt-expression/output.brief create mode 100644 tests-system/rbt-expression/output.json create mode 100644 tests-system/rbt-expression/output.smtlib create mode 100644 tests-system/rbt-expression/tracing diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index 290888be..d399dfb5 100644 --- a/language-reference-manual/lrm.trlc +++ b/language-reference-manual/lrm.trlc @@ -1070,6 +1070,7 @@ section "Expressions" { is recommended that a linter warns whenever a unary minus is encountered that has a non-trivial `term` or `factor` as its operand.''' + untraced_reason = "Non-normative recommendation" } Example Expression_Examples { diff --git a/tests-system/expressions/foo.rsl b/tests-system/expressions/foo.rsl deleted file mode 100644 index b7f715fe..00000000 --- a/tests-system/expressions/foo.rsl +++ /dev/null @@ -1,12 +0,0 @@ -package Foo - -type T { - ione Integer - itwo Integer - done Decimal - dtwo Decimal - yay Boolean - nay Boolean - foo String - foobar String -} diff --git a/tests-system/expressions/output b/tests-system/expressions/output deleted file mode 100644 index 304cb072..00000000 --- a/tests-system/expressions/output +++ /dev/null @@ -1,171 +0,0 @@ -checks T { - ^ expressions/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature] -yay and yay and yay, "01: good and" - ^^^ expressions/foo.check:13: issue: expression is always true [vcg-always-true] -nay or yay or nay, "02: or" - ^^ expressions/foo.check:16: issue: expression is always true [vcg-always-true] -nay xor yay, "03: good xor" - ^^^ expressions/foo.check:19: issue: expression is always true [vcg-always-true] -yay implies yay, "04: good implies" - ^^^^^^^ expressions/foo.check:22: issue: expression is always true [vcg-always-true] -ione < itwo, "05: good i<" - ^ expressions/foo.check:25: issue: expression is always true [vcg-always-true] -done < dtwo, "06: good d<" - ^ expressions/foo.check:28: issue: expression is always true [vcg-always-true] -ione <= ione, "07: good i<=" - ^^ expressions/foo.check:31: issue: expression is always true [vcg-always-true] -done <= done, "08: good d<=" - ^^ expressions/foo.check:34: issue: expression is always true [vcg-always-true] -itwo > ione, "09: good i>" - ^ expressions/foo.check:37: issue: expression is always true [vcg-always-true] -dtwo > done, "10: good d>" - ^ expressions/foo.check:40: issue: expression is always true [vcg-always-true] -itwo >= ione, "11: good i>=" - ^^ expressions/foo.check:43: issue: expression is always true [vcg-always-true] -dtwo >= done, "12: good d>=" - ^^ expressions/foo.check:46: issue: expression is always true [vcg-always-true] -ione == ione, "13: good i==" - ^^ expressions/foo.check:49: issue: expression is always true [vcg-always-true] -done == done, "14: good d==" - ^^ expressions/foo.check:52: issue: expression is always true [vcg-always-true] -ione != itwo, "15: good i!=" - ^^ expressions/foo.check:55: issue: expression is always true [vcg-always-true] -done != dtwo, "16: good d!=" - ^^ expressions/foo.check:58: issue: expression is always true [vcg-always-true] -ione in 0 .. 10, "17: good range iin" - ^^ expressions/foo.check:61: issue: expression is always true [vcg-always-true] -done in 0.0 .. 10.0, "18: good range din" - ^^ expressions/foo.check:64: issue: expression is always true [vcg-always-true] -ione not in 5 .. 10, "19: good range not iin" - ^^^ expressions/foo.check:67: issue: expression is always true [vcg-always-true] -done not in 5.0 .. 10.0, "20: good range not din" - ^^^ expressions/foo.check:70: issue: expression is always true [vcg-always-true] -foo in foobar, "21: good substring" - ^^ expressions/foo.check:73: issue: expression is always true [vcg-always-true] -(-ione) + ione + itwo == itwo, "22: good i adding" - ^^ expressions/foo.check:76: issue: expression is always true [vcg-always-true] -(-done) + done + dtwo == dtwo, "23: good d adding" - ^^ expressions/foo.check:80: issue: expression is always true [vcg-always-true] -ione * itwo * ione * itwo == itwo + itwo, "24: good i*" - ^^ expressions/foo.check:84: issue: expression is always true [vcg-always-true] -done * dtwo * done * dtwo == dtwo + dtwo, "25: good d*" - ^^ expressions/foo.check:87: issue: expression is always true [vcg-always-true] -10 / itwo / itwo == itwo, "26: good i/" - ^^ expressions/foo.check:90: issue: expression is always true [vcg-always-true] -10.0 / dtwo / dtwo == 2.5, "27: good d/" - ^^ expressions/foo.check:93: issue: expression is always true [vcg-always-true] -10 % 5 == 0, "28: good % (1/12)" - ^^ expressions/foo.check:96: issue: expression is always true [vcg-always-true] -11 % 5 == 1, "28: good % (2/12)" - ^^ expressions/foo.check:97: issue: expression is always true [vcg-always-true] -14 % 5 == 4, "28: good % (3/12)" - ^^ expressions/foo.check:98: issue: expression is always true [vcg-always-true] -(-10) % 5 == 0, "28: good % (4/12)" - ^^ expressions/foo.check:99: issue: expression is always true [vcg-always-true] -(-11) % 5 == -1, "28: good % (5/12)" - ^^ expressions/foo.check:100: issue: expression is always true [vcg-always-true] -(-14) % 5 == -4, "28: good % (6/12)" - ^^ expressions/foo.check:101: issue: expression is always true [vcg-always-true] -10 % (-5) == 0, "28: good % (7/12)" - ^^ expressions/foo.check:102: issue: expression is always true [vcg-always-true] -11 % (-5) == 1, "28: good % (8/12)" - ^^ expressions/foo.check:103: issue: expression is always true [vcg-always-true] -14 % (-5) == 4, "28: good % (9/12)" - ^^ expressions/foo.check:104: issue: expression is always true [vcg-always-true] -(-10) % (-5) == 0, "28: good % (10/12)" - ^^ expressions/foo.check:105: issue: expression is always true [vcg-always-true] -(-11) % (-5) == -1, "28: good % (11/12)" - ^^ expressions/foo.check:106: issue: expression is always true [vcg-always-true] -(-14) % (-5) == -4, "28: good % (12/12)" - ^^ expressions/foo.check:107: issue: expression is always true [vcg-always-true] -itwo ** (2 + 1) == 8, "29: good iexp" - ^^ expressions/foo.check:113: issue: expression is always true [vcg-always-true] -dtwo ** (2 + 1) == 8.0, "30: good dexp" - ^^ expressions/foo.check:116: issue: expression is always true [vcg-always-true] -not nay, "31: good lnot" -^^^ expressions/foo.check:119: issue: expression is always true [vcg-always-true] -abs (ione - itwo) == ione, "32: good iabs" - ^^ expressions/foo.check:122: issue: expression is always true [vcg-always-true] -abs (done - dtwo) == done, "33: good dabs" - ^^ expressions/foo.check:125: issue: expression is always true [vcg-always-true] -(if yay then ione else itwo) == ione, "34: good ifexpr" - ^^ expressions/foo.check:128: issue: expression is always true [vcg-always-true] -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 01: bad and -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 02: bad or -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 03: bad xor -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 04: bad implies -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 05: bad i< -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 06: bad d< -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 07: bad i<= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 08: bad d<= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 09: bad i> -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 10: bad d> -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 11: bad i>= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 12: bad d>= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 13: bad i== -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 14: bad d== -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 15: bad i!= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 16: bad d!= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 17: bad range iin -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 18: bad range din -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 19: bad range not iin -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 20: bad range not din -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 21: bad substring -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 22: bad i adding (1/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 22: bad i adding (2/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 23: bad d adding (1/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 23: bad d adding (2/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 24: bad i* -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 25: bad d* -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 26: bad i/ -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 27: bad d/ -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (1/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (2/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (3/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (4/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 29: bad iexp -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 30: bad dexp -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 31: bad lnot -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 32: bad iabs -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 33: bad dabs -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 34: bad ifexpr -Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 85 warning(s) diff --git a/tests-system/expressions/output.brief b/tests-system/expressions/output.brief deleted file mode 100644 index 04a93443..00000000 --- a/tests-system/expressions/output.brief +++ /dev/null @@ -1,39 +0,0 @@ -expressions/foo.trlc:3:3: trlc check warning: 01: bad and -expressions/foo.trlc:3:3: trlc check warning: 02: bad or -expressions/foo.trlc:3:3: trlc check warning: 03: bad xor -expressions/foo.trlc:3:3: trlc check warning: 04: bad implies -expressions/foo.trlc:3:3: trlc check warning: 05: bad i< -expressions/foo.trlc:3:3: trlc check warning: 06: bad d< -expressions/foo.trlc:3:3: trlc check warning: 07: bad i<= -expressions/foo.trlc:3:3: trlc check warning: 08: bad d<= -expressions/foo.trlc:3:3: trlc check warning: 09: bad i> -expressions/foo.trlc:3:3: trlc check warning: 10: bad d> -expressions/foo.trlc:3:3: trlc check warning: 11: bad i>= -expressions/foo.trlc:3:3: trlc check warning: 12: bad d>= -expressions/foo.trlc:3:3: trlc check warning: 13: bad i== -expressions/foo.trlc:3:3: trlc check warning: 14: bad d== -expressions/foo.trlc:3:3: trlc check warning: 15: bad i!= -expressions/foo.trlc:3:3: trlc check warning: 16: bad d!= -expressions/foo.trlc:3:3: trlc check warning: 17: bad range iin -expressions/foo.trlc:3:3: trlc check warning: 18: bad range din -expressions/foo.trlc:3:3: trlc check warning: 19: bad range not iin -expressions/foo.trlc:3:3: trlc check warning: 20: bad range not din -expressions/foo.trlc:3:3: trlc check warning: 21: bad substring -expressions/foo.trlc:3:3: trlc check warning: 22: bad i adding (1/2) -expressions/foo.trlc:3:3: trlc check warning: 22: bad i adding (2/2) -expressions/foo.trlc:3:3: trlc check warning: 23: bad d adding (1/2) -expressions/foo.trlc:3:3: trlc check warning: 23: bad d adding (2/2) -expressions/foo.trlc:3:3: trlc check warning: 24: bad i* -expressions/foo.trlc:3:3: trlc check warning: 25: bad d* -expressions/foo.trlc:3:3: trlc check warning: 26: bad i/ -expressions/foo.trlc:3:3: trlc check warning: 27: bad d/ -expressions/foo.trlc:3:3: trlc check warning: 28: bad % (1/4) -expressions/foo.trlc:3:3: trlc check warning: 28: bad % (2/4) -expressions/foo.trlc:3:3: trlc check warning: 28: bad % (3/4) -expressions/foo.trlc:3:3: trlc check warning: 28: bad % (4/4) -expressions/foo.trlc:3:3: trlc check warning: 29: bad iexp -expressions/foo.trlc:3:3: trlc check warning: 30: bad dexp -expressions/foo.trlc:3:3: trlc check warning: 31: bad lnot -expressions/foo.trlc:3:3: trlc check warning: 32: bad iabs -expressions/foo.trlc:3:3: trlc check warning: 33: bad dabs -expressions/foo.trlc:3:3: trlc check warning: 34: bad ifexpr diff --git a/tests-system/expressions/output.json b/tests-system/expressions/output.json deleted file mode 100644 index 49fd428e..00000000 --- a/tests-system/expressions/output.json +++ /dev/null @@ -1,91 +0,0 @@ -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 01: bad and -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 02: bad or -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 03: bad xor -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 04: bad implies -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 05: bad i< -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 06: bad d< -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 07: bad i<= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 08: bad d<= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 09: bad i> -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 10: bad d> -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 11: bad i>= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 12: bad d>= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 13: bad i== -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 14: bad d== -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 15: bad i!= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 16: bad d!= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 17: bad range iin -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 18: bad range din -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 19: bad range not iin -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 20: bad range not din -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 21: bad substring -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 22: bad i adding (1/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 22: bad i adding (2/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 23: bad d adding (1/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 23: bad d adding (2/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 24: bad i* -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 25: bad d* -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 26: bad i/ -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 27: bad d/ -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (1/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (2/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (3/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (4/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 29: bad iexp -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 30: bad dexp -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 31: bad lnot -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 32: bad iabs -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 33: bad dabs -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 34: bad ifexpr -{ - "Test": { - "done": 1.0, - "dtwo": 2.0, - "foo": "foo", - "foobar": "foobar", - "ione": 1, - "itwo": 2, - "nay": false, - "yay": true - } -} -Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 39 warning(s) diff --git a/tests-system/expressions/output.smtlib b/tests-system/expressions/output.smtlib deleted file mode 100644 index 304cb072..00000000 --- a/tests-system/expressions/output.smtlib +++ /dev/null @@ -1,171 +0,0 @@ -checks T { - ^ expressions/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature] -yay and yay and yay, "01: good and" - ^^^ expressions/foo.check:13: issue: expression is always true [vcg-always-true] -nay or yay or nay, "02: or" - ^^ expressions/foo.check:16: issue: expression is always true [vcg-always-true] -nay xor yay, "03: good xor" - ^^^ expressions/foo.check:19: issue: expression is always true [vcg-always-true] -yay implies yay, "04: good implies" - ^^^^^^^ expressions/foo.check:22: issue: expression is always true [vcg-always-true] -ione < itwo, "05: good i<" - ^ expressions/foo.check:25: issue: expression is always true [vcg-always-true] -done < dtwo, "06: good d<" - ^ expressions/foo.check:28: issue: expression is always true [vcg-always-true] -ione <= ione, "07: good i<=" - ^^ expressions/foo.check:31: issue: expression is always true [vcg-always-true] -done <= done, "08: good d<=" - ^^ expressions/foo.check:34: issue: expression is always true [vcg-always-true] -itwo > ione, "09: good i>" - ^ expressions/foo.check:37: issue: expression is always true [vcg-always-true] -dtwo > done, "10: good d>" - ^ expressions/foo.check:40: issue: expression is always true [vcg-always-true] -itwo >= ione, "11: good i>=" - ^^ expressions/foo.check:43: issue: expression is always true [vcg-always-true] -dtwo >= done, "12: good d>=" - ^^ expressions/foo.check:46: issue: expression is always true [vcg-always-true] -ione == ione, "13: good i==" - ^^ expressions/foo.check:49: issue: expression is always true [vcg-always-true] -done == done, "14: good d==" - ^^ expressions/foo.check:52: issue: expression is always true [vcg-always-true] -ione != itwo, "15: good i!=" - ^^ expressions/foo.check:55: issue: expression is always true [vcg-always-true] -done != dtwo, "16: good d!=" - ^^ expressions/foo.check:58: issue: expression is always true [vcg-always-true] -ione in 0 .. 10, "17: good range iin" - ^^ expressions/foo.check:61: issue: expression is always true [vcg-always-true] -done in 0.0 .. 10.0, "18: good range din" - ^^ expressions/foo.check:64: issue: expression is always true [vcg-always-true] -ione not in 5 .. 10, "19: good range not iin" - ^^^ expressions/foo.check:67: issue: expression is always true [vcg-always-true] -done not in 5.0 .. 10.0, "20: good range not din" - ^^^ expressions/foo.check:70: issue: expression is always true [vcg-always-true] -foo in foobar, "21: good substring" - ^^ expressions/foo.check:73: issue: expression is always true [vcg-always-true] -(-ione) + ione + itwo == itwo, "22: good i adding" - ^^ expressions/foo.check:76: issue: expression is always true [vcg-always-true] -(-done) + done + dtwo == dtwo, "23: good d adding" - ^^ expressions/foo.check:80: issue: expression is always true [vcg-always-true] -ione * itwo * ione * itwo == itwo + itwo, "24: good i*" - ^^ expressions/foo.check:84: issue: expression is always true [vcg-always-true] -done * dtwo * done * dtwo == dtwo + dtwo, "25: good d*" - ^^ expressions/foo.check:87: issue: expression is always true [vcg-always-true] -10 / itwo / itwo == itwo, "26: good i/" - ^^ expressions/foo.check:90: issue: expression is always true [vcg-always-true] -10.0 / dtwo / dtwo == 2.5, "27: good d/" - ^^ expressions/foo.check:93: issue: expression is always true [vcg-always-true] -10 % 5 == 0, "28: good % (1/12)" - ^^ expressions/foo.check:96: issue: expression is always true [vcg-always-true] -11 % 5 == 1, "28: good % (2/12)" - ^^ expressions/foo.check:97: issue: expression is always true [vcg-always-true] -14 % 5 == 4, "28: good % (3/12)" - ^^ expressions/foo.check:98: issue: expression is always true [vcg-always-true] -(-10) % 5 == 0, "28: good % (4/12)" - ^^ expressions/foo.check:99: issue: expression is always true [vcg-always-true] -(-11) % 5 == -1, "28: good % (5/12)" - ^^ expressions/foo.check:100: issue: expression is always true [vcg-always-true] -(-14) % 5 == -4, "28: good % (6/12)" - ^^ expressions/foo.check:101: issue: expression is always true [vcg-always-true] -10 % (-5) == 0, "28: good % (7/12)" - ^^ expressions/foo.check:102: issue: expression is always true [vcg-always-true] -11 % (-5) == 1, "28: good % (8/12)" - ^^ expressions/foo.check:103: issue: expression is always true [vcg-always-true] -14 % (-5) == 4, "28: good % (9/12)" - ^^ expressions/foo.check:104: issue: expression is always true [vcg-always-true] -(-10) % (-5) == 0, "28: good % (10/12)" - ^^ expressions/foo.check:105: issue: expression is always true [vcg-always-true] -(-11) % (-5) == -1, "28: good % (11/12)" - ^^ expressions/foo.check:106: issue: expression is always true [vcg-always-true] -(-14) % (-5) == -4, "28: good % (12/12)" - ^^ expressions/foo.check:107: issue: expression is always true [vcg-always-true] -itwo ** (2 + 1) == 8, "29: good iexp" - ^^ expressions/foo.check:113: issue: expression is always true [vcg-always-true] -dtwo ** (2 + 1) == 8.0, "30: good dexp" - ^^ expressions/foo.check:116: issue: expression is always true [vcg-always-true] -not nay, "31: good lnot" -^^^ expressions/foo.check:119: issue: expression is always true [vcg-always-true] -abs (ione - itwo) == ione, "32: good iabs" - ^^ expressions/foo.check:122: issue: expression is always true [vcg-always-true] -abs (done - dtwo) == done, "33: good dabs" - ^^ expressions/foo.check:125: issue: expression is always true [vcg-always-true] -(if yay then ione else itwo) == ione, "34: good ifexpr" - ^^ expressions/foo.check:128: issue: expression is always true [vcg-always-true] -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 01: bad and -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 02: bad or -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 03: bad xor -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 04: bad implies -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 05: bad i< -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 06: bad d< -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 07: bad i<= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 08: bad d<= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 09: bad i> -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 10: bad d> -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 11: bad i>= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 12: bad d>= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 13: bad i== -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 14: bad d== -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 15: bad i!= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 16: bad d!= -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 17: bad range iin -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 18: bad range din -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 19: bad range not iin -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 20: bad range not din -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 21: bad substring -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 22: bad i adding (1/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 22: bad i adding (2/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 23: bad d adding (1/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 23: bad d adding (2/2) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 24: bad i* -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 25: bad d* -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 26: bad i/ -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 27: bad d/ -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (1/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (2/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (3/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 28: bad % (4/4) -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 29: bad iexp -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 30: bad dexp -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 31: bad lnot -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 32: bad iabs -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 33: bad dabs -T Test { - ^^^^ expressions/foo.trlc:3: check warning: 34: bad ifexpr -Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 85 warning(s) diff --git a/tests-system/expressions/foo.check b/tests-system/rbt-expression/foo.rsl similarity index 96% rename from tests-system/expressions/foo.check rename to tests-system/rbt-expression/foo.rsl index acbf5af9..421603aa 100644 --- a/tests-system/expressions/foo.check +++ b/tests-system/rbt-expression/foo.rsl @@ -1,5 +1,16 @@ package Foo +type T { + ione Integer + itwo Integer + done Decimal + dtwo Decimal + yay Boolean + nay Boolean + foo String + foobar String +} + checks T { ione == 1, fatal "bad setup" itwo == 2, fatal "bad setup" diff --git a/tests-system/expressions/foo.trlc b/tests-system/rbt-expression/foo.trlc similarity index 100% rename from tests-system/expressions/foo.trlc rename to tests-system/rbt-expression/foo.trlc diff --git a/tests-system/rbt-expression/output b/tests-system/rbt-expression/output new file mode 100644 index 00000000..8353e03c --- /dev/null +++ b/tests-system/rbt-expression/output @@ -0,0 +1,169 @@ +yay and yay and yay, "01: good and" + ^^^ rbt-expression/foo.rsl:24: issue: expression is always true [vcg-always-true] +nay or yay or nay, "02: or" + ^^ rbt-expression/foo.rsl:27: issue: expression is always true [vcg-always-true] +nay xor yay, "03: good xor" + ^^^ rbt-expression/foo.rsl:30: issue: expression is always true [vcg-always-true] +yay implies yay, "04: good implies" + ^^^^^^^ rbt-expression/foo.rsl:33: issue: expression is always true [vcg-always-true] +ione < itwo, "05: good i<" + ^ rbt-expression/foo.rsl:36: issue: expression is always true [vcg-always-true] +done < dtwo, "06: good d<" + ^ rbt-expression/foo.rsl:39: issue: expression is always true [vcg-always-true] +ione <= ione, "07: good i<=" + ^^ rbt-expression/foo.rsl:42: issue: expression is always true [vcg-always-true] +done <= done, "08: good d<=" + ^^ rbt-expression/foo.rsl:45: issue: expression is always true [vcg-always-true] +itwo > ione, "09: good i>" + ^ rbt-expression/foo.rsl:48: issue: expression is always true [vcg-always-true] +dtwo > done, "10: good d>" + ^ rbt-expression/foo.rsl:51: issue: expression is always true [vcg-always-true] +itwo >= ione, "11: good i>=" + ^^ rbt-expression/foo.rsl:54: issue: expression is always true [vcg-always-true] +dtwo >= done, "12: good d>=" + ^^ rbt-expression/foo.rsl:57: issue: expression is always true [vcg-always-true] +ione == ione, "13: good i==" + ^^ rbt-expression/foo.rsl:60: issue: expression is always true [vcg-always-true] +done == done, "14: good d==" + ^^ rbt-expression/foo.rsl:63: issue: expression is always true [vcg-always-true] +ione != itwo, "15: good i!=" + ^^ rbt-expression/foo.rsl:66: issue: expression is always true [vcg-always-true] +done != dtwo, "16: good d!=" + ^^ rbt-expression/foo.rsl:69: issue: expression is always true [vcg-always-true] +ione in 0 .. 10, "17: good range iin" + ^^ rbt-expression/foo.rsl:72: issue: expression is always true [vcg-always-true] +done in 0.0 .. 10.0, "18: good range din" + ^^ rbt-expression/foo.rsl:75: issue: expression is always true [vcg-always-true] +ione not in 5 .. 10, "19: good range not iin" + ^^^ rbt-expression/foo.rsl:78: issue: expression is always true [vcg-always-true] +done not in 5.0 .. 10.0, "20: good range not din" + ^^^ rbt-expression/foo.rsl:81: issue: expression is always true [vcg-always-true] +foo in foobar, "21: good substring" + ^^ rbt-expression/foo.rsl:84: issue: expression is always true [vcg-always-true] +(-ione) + ione + itwo == itwo, "22: good i adding" + ^^ rbt-expression/foo.rsl:87: issue: expression is always true [vcg-always-true] +(-done) + done + dtwo == dtwo, "23: good d adding" + ^^ rbt-expression/foo.rsl:91: issue: expression is always true [vcg-always-true] +ione * itwo * ione * itwo == itwo + itwo, "24: good i*" + ^^ rbt-expression/foo.rsl:95: issue: expression is always true [vcg-always-true] +done * dtwo * done * dtwo == dtwo + dtwo, "25: good d*" + ^^ rbt-expression/foo.rsl:98: issue: expression is always true [vcg-always-true] +10 / itwo / itwo == itwo, "26: good i/" + ^^ rbt-expression/foo.rsl:101: issue: expression is always true [vcg-always-true] +10.0 / dtwo / dtwo == 2.5, "27: good d/" + ^^ rbt-expression/foo.rsl:104: issue: expression is always true [vcg-always-true] +10 % 5 == 0, "28: good % (1/12)" + ^^ rbt-expression/foo.rsl:107: issue: expression is always true [vcg-always-true] +11 % 5 == 1, "28: good % (2/12)" + ^^ rbt-expression/foo.rsl:108: issue: expression is always true [vcg-always-true] +14 % 5 == 4, "28: good % (3/12)" + ^^ rbt-expression/foo.rsl:109: issue: expression is always true [vcg-always-true] +(-10) % 5 == 0, "28: good % (4/12)" + ^^ rbt-expression/foo.rsl:110: issue: expression is always true [vcg-always-true] +(-11) % 5 == -1, "28: good % (5/12)" + ^^ rbt-expression/foo.rsl:111: issue: expression is always true [vcg-always-true] +(-14) % 5 == -4, "28: good % (6/12)" + ^^ rbt-expression/foo.rsl:112: issue: expression is always true [vcg-always-true] +10 % (-5) == 0, "28: good % (7/12)" + ^^ rbt-expression/foo.rsl:113: issue: expression is always true [vcg-always-true] +11 % (-5) == 1, "28: good % (8/12)" + ^^ rbt-expression/foo.rsl:114: issue: expression is always true [vcg-always-true] +14 % (-5) == 4, "28: good % (9/12)" + ^^ rbt-expression/foo.rsl:115: issue: expression is always true [vcg-always-true] +(-10) % (-5) == 0, "28: good % (10/12)" + ^^ rbt-expression/foo.rsl:116: issue: expression is always true [vcg-always-true] +(-11) % (-5) == -1, "28: good % (11/12)" + ^^ rbt-expression/foo.rsl:117: issue: expression is always true [vcg-always-true] +(-14) % (-5) == -4, "28: good % (12/12)" + ^^ rbt-expression/foo.rsl:118: issue: expression is always true [vcg-always-true] +itwo ** (2 + 1) == 8, "29: good iexp" + ^^ rbt-expression/foo.rsl:124: issue: expression is always true [vcg-always-true] +dtwo ** (2 + 1) == 8.0, "30: good dexp" + ^^ rbt-expression/foo.rsl:127: issue: expression is always true [vcg-always-true] +not nay, "31: good lnot" +^^^ rbt-expression/foo.rsl:130: issue: expression is always true [vcg-always-true] +abs (ione - itwo) == ione, "32: good iabs" + ^^ rbt-expression/foo.rsl:133: issue: expression is always true [vcg-always-true] +abs (done - dtwo) == done, "33: good dabs" + ^^ rbt-expression/foo.rsl:136: issue: expression is always true [vcg-always-true] +(if yay then ione else itwo) == ione, "34: good ifexpr" + ^^ rbt-expression/foo.rsl:139: issue: expression is always true [vcg-always-true] +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 01: bad and +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 02: bad or +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 03: bad xor +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 04: bad implies +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 05: bad i< +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 06: bad d< +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 07: bad i<= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 08: bad d<= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 09: bad i> +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 10: bad d> +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 11: bad i>= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 12: bad d>= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 13: bad i== +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 14: bad d== +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 15: bad i!= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 16: bad d!= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 17: bad range iin +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 18: bad range din +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 19: bad range not iin +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 20: bad range not din +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 21: bad substring +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 22: bad i adding (1/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 22: bad i adding (2/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 23: bad d adding (1/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 23: bad d adding (2/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 24: bad i* +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 25: bad d* +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 26: bad i/ +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 27: bad d/ +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (1/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (2/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (3/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (4/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 29: bad iexp +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 30: bad dexp +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 31: bad lnot +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 32: bad iabs +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 33: bad dabs +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 34: bad ifexpr +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 84 warning(s) diff --git a/tests-system/rbt-expression/output.brief b/tests-system/rbt-expression/output.brief new file mode 100644 index 00000000..d26c5879 --- /dev/null +++ b/tests-system/rbt-expression/output.brief @@ -0,0 +1,39 @@ +rbt-expression/foo.trlc:3:3: trlc check warning: 01: bad and +rbt-expression/foo.trlc:3:3: trlc check warning: 02: bad or +rbt-expression/foo.trlc:3:3: trlc check warning: 03: bad xor +rbt-expression/foo.trlc:3:3: trlc check warning: 04: bad implies +rbt-expression/foo.trlc:3:3: trlc check warning: 05: bad i< +rbt-expression/foo.trlc:3:3: trlc check warning: 06: bad d< +rbt-expression/foo.trlc:3:3: trlc check warning: 07: bad i<= +rbt-expression/foo.trlc:3:3: trlc check warning: 08: bad d<= +rbt-expression/foo.trlc:3:3: trlc check warning: 09: bad i> +rbt-expression/foo.trlc:3:3: trlc check warning: 10: bad d> +rbt-expression/foo.trlc:3:3: trlc check warning: 11: bad i>= +rbt-expression/foo.trlc:3:3: trlc check warning: 12: bad d>= +rbt-expression/foo.trlc:3:3: trlc check warning: 13: bad i== +rbt-expression/foo.trlc:3:3: trlc check warning: 14: bad d== +rbt-expression/foo.trlc:3:3: trlc check warning: 15: bad i!= +rbt-expression/foo.trlc:3:3: trlc check warning: 16: bad d!= +rbt-expression/foo.trlc:3:3: trlc check warning: 17: bad range iin +rbt-expression/foo.trlc:3:3: trlc check warning: 18: bad range din +rbt-expression/foo.trlc:3:3: trlc check warning: 19: bad range not iin +rbt-expression/foo.trlc:3:3: trlc check warning: 20: bad range not din +rbt-expression/foo.trlc:3:3: trlc check warning: 21: bad substring +rbt-expression/foo.trlc:3:3: trlc check warning: 22: bad i adding (1/2) +rbt-expression/foo.trlc:3:3: trlc check warning: 22: bad i adding (2/2) +rbt-expression/foo.trlc:3:3: trlc check warning: 23: bad d adding (1/2) +rbt-expression/foo.trlc:3:3: trlc check warning: 23: bad d adding (2/2) +rbt-expression/foo.trlc:3:3: trlc check warning: 24: bad i* +rbt-expression/foo.trlc:3:3: trlc check warning: 25: bad d* +rbt-expression/foo.trlc:3:3: trlc check warning: 26: bad i/ +rbt-expression/foo.trlc:3:3: trlc check warning: 27: bad d/ +rbt-expression/foo.trlc:3:3: trlc check warning: 28: bad % (1/4) +rbt-expression/foo.trlc:3:3: trlc check warning: 28: bad % (2/4) +rbt-expression/foo.trlc:3:3: trlc check warning: 28: bad % (3/4) +rbt-expression/foo.trlc:3:3: trlc check warning: 28: bad % (4/4) +rbt-expression/foo.trlc:3:3: trlc check warning: 29: bad iexp +rbt-expression/foo.trlc:3:3: trlc check warning: 30: bad dexp +rbt-expression/foo.trlc:3:3: trlc check warning: 31: bad lnot +rbt-expression/foo.trlc:3:3: trlc check warning: 32: bad iabs +rbt-expression/foo.trlc:3:3: trlc check warning: 33: bad dabs +rbt-expression/foo.trlc:3:3: trlc check warning: 34: bad ifexpr diff --git a/tests-system/rbt-expression/output.json b/tests-system/rbt-expression/output.json new file mode 100644 index 00000000..071ddfcf --- /dev/null +++ b/tests-system/rbt-expression/output.json @@ -0,0 +1,91 @@ +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 01: bad and +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 02: bad or +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 03: bad xor +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 04: bad implies +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 05: bad i< +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 06: bad d< +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 07: bad i<= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 08: bad d<= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 09: bad i> +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 10: bad d> +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 11: bad i>= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 12: bad d>= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 13: bad i== +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 14: bad d== +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 15: bad i!= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 16: bad d!= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 17: bad range iin +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 18: bad range din +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 19: bad range not iin +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 20: bad range not din +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 21: bad substring +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 22: bad i adding (1/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 22: bad i adding (2/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 23: bad d adding (1/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 23: bad d adding (2/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 24: bad i* +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 25: bad d* +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 26: bad i/ +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 27: bad d/ +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (1/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (2/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (3/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (4/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 29: bad iexp +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 30: bad dexp +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 31: bad lnot +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 32: bad iabs +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 33: bad dabs +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 34: bad ifexpr +{ + "Test": { + "done": 1.0, + "dtwo": 2.0, + "foo": "foo", + "foobar": "foobar", + "ione": 1, + "itwo": 2, + "nay": false, + "yay": true + } +} +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 39 warning(s) diff --git a/tests-system/rbt-expression/output.smtlib b/tests-system/rbt-expression/output.smtlib new file mode 100644 index 00000000..8353e03c --- /dev/null +++ b/tests-system/rbt-expression/output.smtlib @@ -0,0 +1,169 @@ +yay and yay and yay, "01: good and" + ^^^ rbt-expression/foo.rsl:24: issue: expression is always true [vcg-always-true] +nay or yay or nay, "02: or" + ^^ rbt-expression/foo.rsl:27: issue: expression is always true [vcg-always-true] +nay xor yay, "03: good xor" + ^^^ rbt-expression/foo.rsl:30: issue: expression is always true [vcg-always-true] +yay implies yay, "04: good implies" + ^^^^^^^ rbt-expression/foo.rsl:33: issue: expression is always true [vcg-always-true] +ione < itwo, "05: good i<" + ^ rbt-expression/foo.rsl:36: issue: expression is always true [vcg-always-true] +done < dtwo, "06: good d<" + ^ rbt-expression/foo.rsl:39: issue: expression is always true [vcg-always-true] +ione <= ione, "07: good i<=" + ^^ rbt-expression/foo.rsl:42: issue: expression is always true [vcg-always-true] +done <= done, "08: good d<=" + ^^ rbt-expression/foo.rsl:45: issue: expression is always true [vcg-always-true] +itwo > ione, "09: good i>" + ^ rbt-expression/foo.rsl:48: issue: expression is always true [vcg-always-true] +dtwo > done, "10: good d>" + ^ rbt-expression/foo.rsl:51: issue: expression is always true [vcg-always-true] +itwo >= ione, "11: good i>=" + ^^ rbt-expression/foo.rsl:54: issue: expression is always true [vcg-always-true] +dtwo >= done, "12: good d>=" + ^^ rbt-expression/foo.rsl:57: issue: expression is always true [vcg-always-true] +ione == ione, "13: good i==" + ^^ rbt-expression/foo.rsl:60: issue: expression is always true [vcg-always-true] +done == done, "14: good d==" + ^^ rbt-expression/foo.rsl:63: issue: expression is always true [vcg-always-true] +ione != itwo, "15: good i!=" + ^^ rbt-expression/foo.rsl:66: issue: expression is always true [vcg-always-true] +done != dtwo, "16: good d!=" + ^^ rbt-expression/foo.rsl:69: issue: expression is always true [vcg-always-true] +ione in 0 .. 10, "17: good range iin" + ^^ rbt-expression/foo.rsl:72: issue: expression is always true [vcg-always-true] +done in 0.0 .. 10.0, "18: good range din" + ^^ rbt-expression/foo.rsl:75: issue: expression is always true [vcg-always-true] +ione not in 5 .. 10, "19: good range not iin" + ^^^ rbt-expression/foo.rsl:78: issue: expression is always true [vcg-always-true] +done not in 5.0 .. 10.0, "20: good range not din" + ^^^ rbt-expression/foo.rsl:81: issue: expression is always true [vcg-always-true] +foo in foobar, "21: good substring" + ^^ rbt-expression/foo.rsl:84: issue: expression is always true [vcg-always-true] +(-ione) + ione + itwo == itwo, "22: good i adding" + ^^ rbt-expression/foo.rsl:87: issue: expression is always true [vcg-always-true] +(-done) + done + dtwo == dtwo, "23: good d adding" + ^^ rbt-expression/foo.rsl:91: issue: expression is always true [vcg-always-true] +ione * itwo * ione * itwo == itwo + itwo, "24: good i*" + ^^ rbt-expression/foo.rsl:95: issue: expression is always true [vcg-always-true] +done * dtwo * done * dtwo == dtwo + dtwo, "25: good d*" + ^^ rbt-expression/foo.rsl:98: issue: expression is always true [vcg-always-true] +10 / itwo / itwo == itwo, "26: good i/" + ^^ rbt-expression/foo.rsl:101: issue: expression is always true [vcg-always-true] +10.0 / dtwo / dtwo == 2.5, "27: good d/" + ^^ rbt-expression/foo.rsl:104: issue: expression is always true [vcg-always-true] +10 % 5 == 0, "28: good % (1/12)" + ^^ rbt-expression/foo.rsl:107: issue: expression is always true [vcg-always-true] +11 % 5 == 1, "28: good % (2/12)" + ^^ rbt-expression/foo.rsl:108: issue: expression is always true [vcg-always-true] +14 % 5 == 4, "28: good % (3/12)" + ^^ rbt-expression/foo.rsl:109: issue: expression is always true [vcg-always-true] +(-10) % 5 == 0, "28: good % (4/12)" + ^^ rbt-expression/foo.rsl:110: issue: expression is always true [vcg-always-true] +(-11) % 5 == -1, "28: good % (5/12)" + ^^ rbt-expression/foo.rsl:111: issue: expression is always true [vcg-always-true] +(-14) % 5 == -4, "28: good % (6/12)" + ^^ rbt-expression/foo.rsl:112: issue: expression is always true [vcg-always-true] +10 % (-5) == 0, "28: good % (7/12)" + ^^ rbt-expression/foo.rsl:113: issue: expression is always true [vcg-always-true] +11 % (-5) == 1, "28: good % (8/12)" + ^^ rbt-expression/foo.rsl:114: issue: expression is always true [vcg-always-true] +14 % (-5) == 4, "28: good % (9/12)" + ^^ rbt-expression/foo.rsl:115: issue: expression is always true [vcg-always-true] +(-10) % (-5) == 0, "28: good % (10/12)" + ^^ rbt-expression/foo.rsl:116: issue: expression is always true [vcg-always-true] +(-11) % (-5) == -1, "28: good % (11/12)" + ^^ rbt-expression/foo.rsl:117: issue: expression is always true [vcg-always-true] +(-14) % (-5) == -4, "28: good % (12/12)" + ^^ rbt-expression/foo.rsl:118: issue: expression is always true [vcg-always-true] +itwo ** (2 + 1) == 8, "29: good iexp" + ^^ rbt-expression/foo.rsl:124: issue: expression is always true [vcg-always-true] +dtwo ** (2 + 1) == 8.0, "30: good dexp" + ^^ rbt-expression/foo.rsl:127: issue: expression is always true [vcg-always-true] +not nay, "31: good lnot" +^^^ rbt-expression/foo.rsl:130: issue: expression is always true [vcg-always-true] +abs (ione - itwo) == ione, "32: good iabs" + ^^ rbt-expression/foo.rsl:133: issue: expression is always true [vcg-always-true] +abs (done - dtwo) == done, "33: good dabs" + ^^ rbt-expression/foo.rsl:136: issue: expression is always true [vcg-always-true] +(if yay then ione else itwo) == ione, "34: good ifexpr" + ^^ rbt-expression/foo.rsl:139: issue: expression is always true [vcg-always-true] +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 01: bad and +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 02: bad or +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 03: bad xor +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 04: bad implies +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 05: bad i< +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 06: bad d< +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 07: bad i<= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 08: bad d<= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 09: bad i> +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 10: bad d> +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 11: bad i>= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 12: bad d>= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 13: bad i== +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 14: bad d== +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 15: bad i!= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 16: bad d!= +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 17: bad range iin +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 18: bad range din +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 19: bad range not iin +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 20: bad range not din +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 21: bad substring +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 22: bad i adding (1/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 22: bad i adding (2/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 23: bad d adding (1/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 23: bad d adding (2/2) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 24: bad i* +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 25: bad d* +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 26: bad i/ +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 27: bad d/ +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (1/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (2/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (3/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 28: bad % (4/4) +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 29: bad iexp +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 30: bad dexp +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 31: bad lnot +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 32: bad iabs +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 33: bad dabs +T Test { + ^^^^ rbt-expression/foo.trlc:3: check warning: 34: bad ifexpr +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 84 warning(s) diff --git a/tests-system/rbt-expression/tracing b/tests-system/rbt-expression/tracing new file mode 100644 index 00000000..6edec6ca --- /dev/null +++ b/tests-system/rbt-expression/tracing @@ -0,0 +1,5 @@ +LRM.Relation +LRM.Simple_Expression +LRM.Term +LRM.Factor +LRM.Primary diff --git a/trlc/parser.py b/trlc/parser.py index 1defed0e..ab806733 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -616,6 +616,7 @@ def parse_record_declaration(self): return record def parse_expression(self, scope): + # lobster-trace: LRM.Expression assert isinstance(scope, ast.Scope) n_lhs = self.parse_relation(scope) @@ -673,6 +674,7 @@ def parse_expression(self, scope): return n_lhs def parse_relation(self, scope): + # lobster-trace: LRM.Relation assert isinstance(scope, ast.Scope) relop_mapping = {"==" : ast.Binary_Operator.COMP_EQ, "!=" : ast.Binary_Operator.COMP_NEQ, @@ -757,6 +759,7 @@ def parse_relation(self, scope): return n_lhs def parse_simple_expression(self, scope): + # lobster-trace: LRM.Simple_Expression assert isinstance(scope, ast.Scope) un_add_map = {"+" : ast.Unary_Operator.PLUS, "-" : ast.Unary_Operator.MINUS} @@ -812,6 +815,7 @@ def parse_simple_expression(self, scope): return n_lhs def parse_term(self, scope): + # lobster-trace: LRM.Term assert isinstance(scope, ast.Scope) mul_map = {"*" : ast.Binary_Operator.TIMES, "/" : ast.Binary_Operator.DIVIDE, @@ -835,6 +839,7 @@ def parse_term(self, scope): return n_lhs def parse_factor(self, scope): + # lobster-trace: LRM.Factor assert isinstance(scope, ast.Scope) if self.peek_kw("not"): @@ -879,6 +884,7 @@ def parse_factor(self, scope): return n_lhs def parse_primary(self, scope): + # lobster-trace: LRM.Primary assert isinstance(scope, ast.Scope) if self.peek("INTEGER"): From 7d6d26ec0b6423389ca9b49f24e14defd277dd3d Mon Sep 17 00:00:00 2001 From: christophkloeffel Date: Mon, 23 Oct 2023 12:42:41 +0200 Subject: [PATCH 2/2] enhances tracing --- language-reference-manual/lrm.trlc | 1 - .../example.rsl | 0 tests-system/rbt-unary-minus-parsing/output | 3 +++ .../output.brief | 0 .../output.json | 0 .../rbt-unary-minus-parsing/output.smtlib | 3 +++ tests-system/unary-ops-1/output | 3 --- tests-system/unary-ops-1/output.smtlib | 3 --- trlc/ast.py | 16 ++++++++++++++-- trlc/parser.py | 4 ++++ 10 files changed, 24 insertions(+), 9 deletions(-) rename tests-system/{unary-ops-1 => rbt-unary-minus-parsing}/example.rsl (100%) create mode 100644 tests-system/rbt-unary-minus-parsing/output rename tests-system/{unary-ops-1 => rbt-unary-minus-parsing}/output.brief (100%) rename tests-system/{unary-ops-1 => rbt-unary-minus-parsing}/output.json (100%) create mode 100644 tests-system/rbt-unary-minus-parsing/output.smtlib delete mode 100644 tests-system/unary-ops-1/output delete mode 100644 tests-system/unary-ops-1/output.smtlib diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index d399dfb5..290888be 100644 --- a/language-reference-manual/lrm.trlc +++ b/language-reference-manual/lrm.trlc @@ -1070,7 +1070,6 @@ section "Expressions" { is recommended that a linter warns whenever a unary minus is encountered that has a non-trivial `term` or `factor` as its operand.''' - untraced_reason = "Non-normative recommendation" } Example Expression_Examples { diff --git a/tests-system/unary-ops-1/example.rsl b/tests-system/rbt-unary-minus-parsing/example.rsl similarity index 100% rename from tests-system/unary-ops-1/example.rsl rename to tests-system/rbt-unary-minus-parsing/example.rsl diff --git a/tests-system/rbt-unary-minus-parsing/output b/tests-system/rbt-unary-minus-parsing/output new file mode 100644 index 00000000..bdbe57a4 --- /dev/null +++ b/tests-system/rbt-unary-minus-parsing/output @@ -0,0 +1,3 @@ +-a * b > 0, "potato" +^ rbt-unary-minus-parsing/example.rsl:9: issue: expression means -(a * b), place explicit brackets to clarify intent [unary_minus_precedence] +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s) diff --git a/tests-system/unary-ops-1/output.brief b/tests-system/rbt-unary-minus-parsing/output.brief similarity index 100% rename from tests-system/unary-ops-1/output.brief rename to tests-system/rbt-unary-minus-parsing/output.brief diff --git a/tests-system/unary-ops-1/output.json b/tests-system/rbt-unary-minus-parsing/output.json similarity index 100% rename from tests-system/unary-ops-1/output.json rename to tests-system/rbt-unary-minus-parsing/output.json diff --git a/tests-system/rbt-unary-minus-parsing/output.smtlib b/tests-system/rbt-unary-minus-parsing/output.smtlib new file mode 100644 index 00000000..bdbe57a4 --- /dev/null +++ b/tests-system/rbt-unary-minus-parsing/output.smtlib @@ -0,0 +1,3 @@ +-a * b > 0, "potato" +^ rbt-unary-minus-parsing/example.rsl:9: issue: expression means -(a * b), place explicit brackets to clarify intent [unary_minus_precedence] +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s) diff --git a/tests-system/unary-ops-1/output b/tests-system/unary-ops-1/output deleted file mode 100644 index d478f463..00000000 --- a/tests-system/unary-ops-1/output +++ /dev/null @@ -1,3 +0,0 @@ --a * b > 0, "potato" -^ unary-ops-1/example.rsl:9: issue: expression means -(a * b), place explicit brackets to clarify intent [unary_minus_precedence] -Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s) diff --git a/tests-system/unary-ops-1/output.smtlib b/tests-system/unary-ops-1/output.smtlib deleted file mode 100644 index d478f463..00000000 --- a/tests-system/unary-ops-1/output.smtlib +++ /dev/null @@ -1,3 +0,0 @@ --a * b > 0, "potato" -^ unary-ops-1/example.rsl:9: issue: expression means -(a * b), place explicit brackets to clarify intent [unary_minus_precedence] -Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s) diff --git a/trlc/ast.py b/trlc/ast.py index 858fc0a1..f9dd7adf 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -591,6 +591,7 @@ def to_python_object(self): class Null_Literal(Literal): + # lobster-trace: LRM.Primary """The null literal This can appear in check expressions:: @@ -603,14 +604,12 @@ class Null_Literal(Literal): """ def __init__(self, token): - # lobster-exclude: Constructor only declares variables assert isinstance(token, Token) assert token.kind == "KEYWORD" assert token.value == "null" super().__init__(token.location, None) def dump(self, indent=0): # pragma: no cover - # lobster-exclude: Debugging feature self.write_indent(indent, "Null Literal") def to_string(self): @@ -630,6 +629,7 @@ def can_be_null(self): class Integer_Literal(Literal): # lobster-trace: LRM.Integer_Values + # lobster-trace: LRM.Primary """Integer literals Note that these are always positive. A negative integer is @@ -676,6 +676,7 @@ def can_be_null(self): class Decimal_Literal(Literal): # lobster-trace: LRM.Decimal_Values + # lobster-trace: LRM.Primary """Decimal literals Note that these are always positive. A negative decimal is @@ -723,6 +724,7 @@ def can_be_null(self): class String_Literal(Literal): # lobster-trace: LRM.String_Values # lobster-trace: LRM.Markup_String_Values + # lobster-trace: LRM.Primary """String literals Note the value of the string does not include the quotation marks, @@ -778,6 +780,7 @@ def can_be_null(self): class Boolean_Literal(Literal): # lobster-trace: LRM.Boolean_Values + # lobster-trace: LRM.Primary """Boolean values :attribute value: the boolean value @@ -1166,6 +1169,9 @@ class Unary_Expression(Expression): """ def __init__(self, mh, location, typ, operator, n_operand): + # lobster-trace: LRM.Simple_Expression + # lobster-trace: LRM.Relation + # lobster-trace: LRM.Factor super().__init__(location, typ) assert isinstance(mh, Message_Handler) assert isinstance(operator, Unary_Operator) @@ -1329,6 +1335,11 @@ class Binary_Expression(Expression): """ def __init__(self, mh, location, typ, operator, n_lhs, n_rhs): + # lobster-trace: LRM.Expression + # lobster-trace: LRM.Relation + # lobster-trace: LRM.Simple_Expression + # lobster-trace: LRM.Term + # lobster-trace: LRM.Factor super().__init__(location, typ) assert isinstance(mh, Message_Handler) assert isinstance(operator, Binary_Operator) @@ -1731,6 +1742,7 @@ class Range_Test(Expression): """ def __init__(self, mh, location, typ, n_lhs, n_lower, n_upper): + # lobster-trace: LRM.Relation super().__init__(location, typ) assert isinstance(mh, Message_Handler) assert isinstance(n_lhs, Expression) diff --git a/trlc/parser.py b/trlc/parser.py index ab806733..9162c2f6 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -675,6 +675,7 @@ def parse_expression(self, scope): def parse_relation(self, scope): # lobster-trace: LRM.Relation + # lobster-trace: LRM.Operators assert isinstance(scope, ast.Scope) relop_mapping = {"==" : ast.Binary_Operator.COMP_EQ, "!=" : ast.Binary_Operator.COMP_NEQ, @@ -760,6 +761,8 @@ def parse_relation(self, scope): def parse_simple_expression(self, scope): # lobster-trace: LRM.Simple_Expression + # lobster-trace: LRM.Operators + # lobster-trace: LRM.Unary_Minus_Parsing assert isinstance(scope, ast.Scope) un_add_map = {"+" : ast.Unary_Operator.PLUS, "-" : ast.Unary_Operator.MINUS} @@ -816,6 +819,7 @@ def parse_simple_expression(self, scope): def parse_term(self, scope): # lobster-trace: LRM.Term + # lobster-trace: LRM.Operators assert isinstance(scope, ast.Scope) mul_map = {"*" : ast.Binary_Operator.TIMES, "/" : ast.Binary_Operator.DIVIDE,