diff --git a/CHANGELOG.md b/CHANGELOG.md index ac027c50..8a87e775 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -30,6 +30,15 @@ generated in the following situations: * New minor version release due to minor API changes and major command-line changes. +* When using `--verify` you can now also specify a + [CVC5](https://github.com/cvc5/cvc5) executable using + `--use-cvc5-binary`. This allows you to use the `--verify` option on + platforms where there is no CVC5 PyPI package (i.e. Windows). + +* The [PyVCG](https://pypi.org/project/PyVCG) is now required on all + platforms. The optional dependency is now + [CVC5](https://pypi.org/project/cvc5) instead. + * Remove the `--lint` option. Lint messages are now enabled by default, and `.trlc` files are processed as well. Instead there is a `--no-lint` option which turns off the extra warnings. diff --git a/documentation/TUTORIAL-CI.md b/documentation/TUTORIAL-CI.md index 4240eb31..e338dd7f 100644 --- a/documentation/TUTORIAL-CI.md +++ b/documentation/TUTORIAL-CI.md @@ -43,8 +43,8 @@ The components of this regular expression are: The TRLC tools also come with a static analysis mode that performs additional checks. To enable this use `--verify`, and it requires the -optional dependency [PyVCG](https://pypi.org/project/PyVCG/). It is -strongly suggested to turn this on in CI. +optional dependency [CVC5](https://pypi.org/project/cvc5/) (GNU/Linux +only). It is strongly suggested to turn this on in CI. The TRLC tool goes beyond what the language definition requires and produces additional messages that may be helpful. For example it warns diff --git a/documentation/TUTORIAL-INSTALL.md b/documentation/TUTORIAL-INSTALL.md index 602a8a74..c990a3ed 100644 --- a/documentation/TUTORIAL-INSTALL.md +++ b/documentation/TUTORIAL-INSTALL.md @@ -10,15 +10,9 @@ The easiest way to install the tools is through PyPI: $ pip3 install --user trlc ``` -There are currently no required dependencies, all you need is a -moderatly recent Python 3.9. - -If you are on Linux however, you may want to also install PyVCG as -this enables some advanced features for getting better error messages. - -``` -$ pip3 install --user PyVCG -``` +There are currently one required dependencies (PyVCG which should be +installed automatically), all you need is a moderatly recent Python +3.8 / 3.9 / 3.10 / 3.11. Don't forget to adjust your `PATH` so that `.local/bin` (or the equivalent on Windows) is on it; so that the `trlc` executable can be diff --git a/documentation/TUTORIAL-LINT.md b/documentation/TUTORIAL-LINT.md index 6b7d618e..35040242 100644 --- a/documentation/TUTORIAL-LINT.md +++ b/documentation/TUTORIAL-LINT.md @@ -5,20 +5,24 @@ This is part of the [TRLC Tutorial](TUTORIAL.md). ## Using the linter The TRLC tools come with a static analysis tool that can diagnose some -potential issues with `.rsl` files before they are deployed and used. +potential issues with `.rsl` files before they are deployed and +used. This is enabled by default, but you can turn these off with the +`--no-lint` option. -To do this simply use the `--lint` feature: +To enable more detailed checks you can also use the `--verify` +feature, but please note that this is only available on Linux, and +requires you to have installed the optional dependency +[CVC5](https://pypi.org/project/cvc5). ```bash -$ trlc --lint DIRECTORIES_OR_FILES +$ trlc --verify DIRECTORIES_OR_FILES ``` -To enable more detailed checks you can also use the `--lint --verify` -feature, but please note that this is only available on Linux and OSX, -and requires you to have installed the optional dependency -[PyVCG](https://pypi.org/project/PyVCG). + +If you are on Windows or Linux, you can also download the CVC5 +executables and ask TRLC to use them directly: ```bash -$ trlc --lint --verify DIRECTORIES_OR_FILES +$ trlc --verify --use-cvc5-binary=path/to/cvc5.exe DIRECTORIES_OR_FILES ``` ## Sanity checks @@ -50,7 +54,7 @@ contexts: * division by zero * array out of bounds -The `--lint --verify` feature can also find cases where the check +The `--verify` feature can also find cases where the check could be improved to guard against such as problem. For example: ```trlc @@ -66,7 +70,7 @@ checks T { When running the verifier we can see: ```plain -$ trlc.py --lint --verify trivial.rsl +$ trlc.py --verify trivial.rsl x > 0, "please make this positive", x ^ trivial.rsl:8: warning: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: @@ -98,16 +102,16 @@ checks T { When running the verifier now we no longer get a complaint: ```plain -$ trlc.py --lint --verify trivial.rsl +$ trlc.py --verify trivial.rsl Verified 1 model(s) and 0 check(s) and found no issues ``` ### Caveat -Please keep in mind two limitations with the `--lint --verify` +Please keep in mind two limitations with the `--verify` feature: -* It currently does not work on Windows +* It is harder to use and much slower on Windows * Under some circumstances the counter-examples generated are impossible to achieve, due to how the underlying technology (SMT Solvers) works. The current limitations are documented in the diff --git a/requirements.txt b/requirements.txt index 092dea3e..581a566e 100644 --- a/requirements.txt +++ b/requirements.txt @@ -2,5 +2,4 @@ pycodestyle>=2.10 pylint>=2.17 coverage>=7.2 sphinx>=7.0 -pyvcg==1.0.5 -cvc5==1.0.8 +pyvcg[api]==1.0.6 diff --git a/setup.py b/setup.py index 9dfb7044..66f604e1 100644 --- a/setup.py +++ b/setup.py @@ -33,8 +33,10 @@ required_packages = [] python_required = ">=3.8, <4" if "--plat-name" in sys.argv or "-p" in sys.argv: - required_packages.append("PyVCG==1.0.5") + required_packages.append("PyVCG[api]==1.0.6") python_required = ">=3.8, <3.12" +else: + required_packages.append("PyVCG==1.0.6") setuptools.setup( name="trlc", diff --git a/tests-system/Makefile b/tests-system/Makefile index f6bd3e35..cb8d7573 100644 --- a/tests-system/Makefile +++ b/tests-system/Makefile @@ -2,6 +2,7 @@ RAW_TARGETS=$(filter-out bulk, $(subst ./,,$(shell find . -mindepth 1 -maxdepth TARGETS=\ $(addsuffix /output, $(RAW_TARGETS)) \ + $(addsuffix /output.smtlib, $(RAW_TARGETS)) \ $(addsuffix /output.brief, $(RAW_TARGETS)) \ $(addsuffix /output.json, $(RAW_TARGETS)) @@ -16,6 +17,13 @@ all: $(TARGETS) bulk/output bulk/output.brief bulk/output.json ../trlc.py --verify $(file < $(dir $@)options) \ $(dir $@) > $@ +%/output.smtlib: + -@coverage run -p --rcfile=../coverage.cfg --branch \ + --data-file ../.coverage \ + ../trlc.py --verify --use-cvc5-binary=cvc5 \ + $(file < $(dir $@)options) \ + $(dir $@) > $@ + %/output.brief: -@coverage run -p --rcfile=../coverage.cfg --branch \ --data-file ../.coverage \ diff --git a/tests-system/array-length/output.smtlib b/tests-system/array-length/output.smtlib new file mode 100644 index 00000000..65382358 --- /dev/null +++ b/tests-system/array-length/output.smtlib @@ -0,0 +1,5 @@ +values = ["one", "two", "three"] + ^^^^^^^ array-length/foo.trlc:4: error: this array requires at most 2 elements (3 provided) +values = ["one"] + ^ array-length/foo.trlc:8: error: this array requires at least 2 elements (only 1 provided) +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 error(s) diff --git a/tests-system/array-membership-1/output.smtlib b/tests-system/array-membership-1/output.smtlib new file mode 100644 index 00000000..11aea098 --- /dev/null +++ b/tests-system/array-membership-1/output.smtlib @@ -0,0 +1,13 @@ +arr = [40, 41, 42, 43, 44, 45] + ^ array-membership-1/foo.trlc:10: check warning: 42 is not in array +arr = [40, 41, 42, 43, 44, 45] + ^ array-membership-1/foo.trlc:10: check warning: 42 is in array +arr = [1, 2, 3] + ^ array-membership-1/foo.trlc:22: check warning: 42 is not in array +arr = [1, 2, 3] + ^ array-membership-1/foo.trlc:22: check warning: 42 is in array +arr = [] + ^ array-membership-1/foo.trlc:34: check warning: 42 is not in array +arr = [] + ^ array-membership-1/foo.trlc:34: check warning: 42 is in array +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 6 warning(s) diff --git a/tests-system/array-membership-2/output.smtlib b/tests-system/array-membership-2/output.smtlib new file mode 100644 index 00000000..8b3eeddb --- /dev/null +++ b/tests-system/array-membership-2/output.smtlib @@ -0,0 +1,3 @@ +ival in arr, warning "potato" +^^^^ array-membership-2/foo.rsl:9: error: expected expression of type Builtin_String, got Builtin_Integer instead +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/array-membership-3/output.smtlib b/tests-system/array-membership-3/output.smtlib new file mode 100644 index 00000000..f62a66cb --- /dev/null +++ b/tests-system/array-membership-3/output.smtlib @@ -0,0 +1,3 @@ +kitten in arr, warning "does not reference kitten" +^^^^^^ array-membership-3/foo.rsl:10: error: unknown symbol kitten +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/arrays-1/output.smtlib b/tests-system/arrays-1/output.smtlib new file mode 100644 index 00000000..ae54c418 --- /dev/null +++ b/tests-system/arrays-1/output.smtlib @@ -0,0 +1,3 @@ +arr = [1, 2, 3] + ^ arrays-1/example.trlc:8: check error: potato +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/arrays-2/output.smtlib b/tests-system/arrays-2/output.smtlib new file mode 100644 index 00000000..e684ba22 --- /dev/null +++ b/tests-system/arrays-2/output.smtlib @@ -0,0 +1,3 @@ +arr[0] == len(arr), "potato", arr +^^^ arrays-2/example.rsl:8: error: expression 'arr' has type Integer, which is not an array +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/base-types/output.smtlib b/tests-system/base-types/output.smtlib new file mode 100644 index 00000000..c8a31315 --- /dev/null +++ b/tests-system/base-types/output.smtlib @@ -0,0 +1,5 @@ +checks MyType { + ^^^^^^ base-types/checks.check:4: issue: move this check block into bar.rsl:1 [deprecated_feature] +int_nok = 24 + ^^ base-types/instances.trlc:10: check error: int must be 42 +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/bazel-dirs/output.smtlib b/tests-system/bazel-dirs/output.smtlib new file mode 100644 index 00000000..cbd1060f --- /dev/null +++ b/tests-system/bazel-dirs/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found no issues diff --git a/tests-system/builtin-1/output.smtlib b/tests-system/builtin-1/output.smtlib new file mode 100644 index 00000000..0517203e --- /dev/null +++ b/tests-system/builtin-1/output.smtlib @@ -0,0 +1,3 @@ +len = 2 + ^ builtin-1/example.trlc:10: check warning: potato +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) diff --git a/tests-system/builtin-2/output.smtlib b/tests-system/builtin-2/output.smtlib new file mode 100644 index 00000000..3b5c542b --- /dev/null +++ b/tests-system/builtin-2/output.smtlib @@ -0,0 +1,3 @@ +len == trlc:len(str), warning "potato", len + ^^^^^^^^ builtin-2/legacy.rsl:9: issue: please use function len instead [deprecated_feature] +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s) diff --git a/tests-system/check-wo-type/output.smtlib b/tests-system/check-wo-type/output.smtlib new file mode 100644 index 00000000..60f595a8 --- /dev/null +++ b/tests-system/check-wo-type/output.smtlib @@ -0,0 +1,3 @@ +checks { + ^ check-wo-type/checks.check:3: error: expected identifier, encountered opening brace '{' instead +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/checks-1/output.smtlib b/tests-system/checks-1/output.smtlib new file mode 100644 index 00000000..8324c90f --- /dev/null +++ b/tests-system/checks-1/output.smtlib @@ -0,0 +1,14 @@ +checks T { + ^ checks-1/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature] +a < b, "a must be less than b" + ^ checks-1/foo.check:4: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | a = 0 + | /* b is null */ + | } +T Test_1 { + ^^^^^^ checks-1/foo.trlc:3: error: rhs of check a < b (foo.check:4) must not be null +T Test_2 { + ^^^^^^ checks-1/foo.trlc:7: check error: a must be less than b +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 2 warning(s) and 2 error(s) diff --git a/tests-system/checks-2/output.smtlib b/tests-system/checks-2/output.smtlib new file mode 100644 index 00000000..a111faba --- /dev/null +++ b/tests-system/checks-2/output.smtlib @@ -0,0 +1,7 @@ +checks T { + ^ checks-2/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature] +T Test_1 { + ^^^^^^ checks-2/foo.trlc:3: check error: please define b +a = 5 + ^ checks-2/foo.trlc:8: check error: a must be less than b +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 2 error(s) diff --git a/tests-system/checks-3/output.smtlib b/tests-system/checks-3/output.smtlib new file mode 100644 index 00000000..9ae8f5ba --- /dev/null +++ b/tests-system/checks-3/output.smtlib @@ -0,0 +1,5 @@ +checks T { + ^ checks-3/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature] +a = 5 + ^ checks-3/foo.trlc:8: check error: a must be less than b +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/checks-4/output.smtlib b/tests-system/checks-4/output.smtlib new file mode 100644 index 00000000..a5761cf7 --- /dev/null +++ b/tests-system/checks-4/output.smtlib @@ -0,0 +1,14 @@ +checks T { + ^ checks-4/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature] +(forall v in values => v != foo), "value cannot be same as value of foo", values + ^^^^^^ checks-4/foo.check:4: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | /* foo is null */ + | /* values is null */ + | } +T Test_1 { + ^^^^^^ checks-4/foo.trlc:3: error: values in quantified expression (forall v in values => v != foo) (foo.check:4) must not be null +values = ["x", "kitten", "z"] + ^ checks-4/foo.trlc:9: check error: value cannot be same as value of foo +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 2 warning(s) and 2 error(s) diff --git a/tests-system/checks-5/output.smtlib b/tests-system/checks-5/output.smtlib new file mode 100644 index 00000000..eaef5cd3 --- /dev/null +++ b/tests-system/checks-5/output.smtlib @@ -0,0 +1,6 @@ +Requirement Potato { + ^^^^^^ checks-5/foo.trlc:3: check error: linkage incorrect + | You must either link this requirement to other requirements + | using the derived_from attribute, or you need to set + | top_level to true. +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/checks-6/output.smtlib b/tests-system/checks-6/output.smtlib new file mode 100644 index 00000000..4151546a --- /dev/null +++ b/tests-system/checks-6/output.smtlib @@ -0,0 +1,5 @@ +true, """this + ^^^^^^^ checks-6/foo.rsl:6: error: error message must not contain a newline +true, """this +^^^^ checks-6/foo.rsl:6: issue: expression is always true [vcg-always-true] +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/combined-rsl-file-1/output.smtlib b/tests-system/combined-rsl-file-1/output.smtlib new file mode 100644 index 00000000..4bba2a8c --- /dev/null +++ b/tests-system/combined-rsl-file-1/output.smtlib @@ -0,0 +1,3 @@ +T foo { + ^^^ combined-rsl-file-1/example.trlc:3: check error: potato +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/combined-rsl-file-2/output.smtlib b/tests-system/combined-rsl-file-2/output.smtlib new file mode 100644 index 00000000..7d2abf13 --- /dev/null +++ b/tests-system/combined-rsl-file-2/output.smtlib @@ -0,0 +1,2 @@ +package Example + ^^^^^^^ combined-rsl-file-2/b.rsl:1: error: duplicate definition, previous definition at a.rsl:1 diff --git a/tests-system/comments-1/output.smtlib b/tests-system/comments-1/output.smtlib new file mode 100644 index 00000000..6106aec3 --- /dev/null +++ b/tests-system/comments-1/output.smtlib @@ -0,0 +1 @@ +Processed 0 model(s), 0 check(s) and 1 requirement file(s) and found no issues diff --git a/tests-system/comments-2/output.smtlib b/tests-system/comments-2/output.smtlib new file mode 100644 index 00000000..cbd1060f --- /dev/null +++ b/tests-system/comments-2/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found no issues diff --git a/tests-system/cross-refs-in-errors/output.smtlib b/tests-system/cross-refs-in-errors/output.smtlib new file mode 100644 index 00000000..42dbac58 --- /dev/null +++ b/tests-system/cross-refs-in-errors/output.smtlib @@ -0,0 +1,2 @@ +package Foo + ^^^ cross-refs-in-errors/potato/foo.rsl:1: error: duplicate definition, previous definition at kitten/bar.rsl:1 diff --git a/tests-system/cyclic-inheritance/output.smtlib b/tests-system/cyclic-inheritance/output.smtlib new file mode 100644 index 00000000..72b7070f --- /dev/null +++ b/tests-system/cyclic-inheritance/output.smtlib @@ -0,0 +1,5 @@ +type MyType2 extends MyType3 { + ^^^^^^^ cyclic-inheritance/bar.rsl:5: error: unknown symbol MyType3 +type MyType3 extends MyType2 { + ^^^^^^^ cyclic-inheritance/bar.rsl:9: error: unknown symbol MyType2 +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 2 error(s) diff --git a/tests-system/cyclic-packages/output.smtlib b/tests-system/cyclic-packages/output.smtlib new file mode 100644 index 00000000..d9636196 --- /dev/null +++ b/tests-system/cyclic-packages/output.smtlib @@ -0,0 +1,5 @@ +> Bar depends on Baz +> Baz depends on Bork +> Bork depends on Bar +cyclic-packages/bar.rsl: error: circular inheritence +Processed 4 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/decimal-1/output.smtlib b/tests-system/decimal-1/output.smtlib new file mode 100644 index 00000000..c60917e6 --- /dev/null +++ b/tests-system/decimal-1/output.smtlib @@ -0,0 +1,7 @@ +D = 5.0 + ^^^ decimal-1/foo.trlc:9: check warning: D is not less that I +D = -5.0 + ^ decimal-1/foo.trlc:14: check warning: D is not less that I +D = -5.0 + ^ decimal-1/foo.trlc:14: check warning: D is not positive +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s) diff --git a/tests-system/decimal-2/output.smtlib b/tests-system/decimal-2/output.smtlib new file mode 100644 index 00000000..f5558a61 --- /dev/null +++ b/tests-system/decimal-2/output.smtlib @@ -0,0 +1,3 @@ +D in 0 .. 10, warning "potato", D + ^ decimal-2/foo.rsl:8: error: expected expression of type Decimal, got Integer instead +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/decimal-3/output.smtlib b/tests-system/decimal-3/output.smtlib new file mode 100644 index 00000000..f70a7b95 --- /dev/null +++ b/tests-system/decimal-3/output.smtlib @@ -0,0 +1,3 @@ +D in 0.0 .. 10, warning "potato", D + ^^ decimal-3/foo.rsl:8: error: expected expression of type Decimal, got Integer instead +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/decimal-4/output.smtlib b/tests-system/decimal-4/output.smtlib new file mode 100644 index 00000000..cbd1060f --- /dev/null +++ b/tests-system/decimal-4/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found no issues diff --git a/tests-system/decimal-5/output.smtlib b/tests-system/decimal-5/output.smtlib new file mode 100644 index 00000000..cbd1060f --- /dev/null +++ b/tests-system/decimal-5/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found no issues diff --git a/tests-system/decimal-6/output.smtlib b/tests-system/decimal-6/output.smtlib new file mode 100644 index 00000000..f3b84478 --- /dev/null +++ b/tests-system/decimal-6/output.smtlib @@ -0,0 +1,3 @@ +0.0 + D + D + D == 3.0 * D, warning "rounding error", D + ^^ decimal-6/foo.rsl:8: issue: expression is always true [vcg-always-true] +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) diff --git a/tests-system/decimal-7/output.smtlib b/tests-system/decimal-7/output.smtlib new file mode 100644 index 00000000..4f8ec559 --- /dev/null +++ b/tests-system/decimal-7/output.smtlib @@ -0,0 +1,3 @@ +D ** 2 >= 0.0, warning "potato", D + ^^ decimal-7/foo.rsl:8: issue: expression is always true [vcg-always-true] +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s) diff --git a/tests-system/decimal-8/output.smtlib b/tests-system/decimal-8/output.smtlib new file mode 100644 index 00000000..4b7b1703 --- /dev/null +++ b/tests-system/decimal-8/output.smtlib @@ -0,0 +1,3 @@ +D == I, warning "not equal", D + ^^ decimal-8/foo.rsl:9: error: type mismatch: Decimal and Integer do not match +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/delayed-references-1/output.smtlib b/tests-system/delayed-references-1/output.smtlib new file mode 100644 index 00000000..72aa97d2 --- /dev/null +++ b/tests-system/delayed-references-1/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 2 requirement file(s) and found no issues diff --git a/tests-system/derived-type-ref/output.smtlib b/tests-system/derived-type-ref/output.smtlib new file mode 100644 index 00000000..e88761ff --- /dev/null +++ b/tests-system/derived-type-ref/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found no issues diff --git a/tests-system/duplicate-imports/output.smtlib b/tests-system/duplicate-imports/output.smtlib new file mode 100644 index 00000000..30b1e9a5 --- /dev/null +++ b/tests-system/duplicate-imports/output.smtlib @@ -0,0 +1,3 @@ +import Foo + ^^^ duplicate-imports/bar.trlc:4: warning: duplicate import of package Foo +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) diff --git a/tests-system/duplicate-late-packages/output.smtlib b/tests-system/duplicate-late-packages/output.smtlib new file mode 100644 index 00000000..c839b5bb --- /dev/null +++ b/tests-system/duplicate-late-packages/output.smtlib @@ -0,0 +1,3 @@ +package Foo + ^^^ duplicate-late-packages/foo.trlc:1: warning: duplicate late declaration of package Foo, previous declaration in bar.trlc:1; consider adding an rsl file declaring the package +Processed 0 model(s), 0 check(s) and 3 requirement file(s) and found 1 warning(s) diff --git a/tests-system/empty-attributes/output.smtlib b/tests-system/empty-attributes/output.smtlib new file mode 100644 index 00000000..6f2e6403 --- /dev/null +++ b/tests-system/empty-attributes/output.smtlib @@ -0,0 +1,5 @@ +checks BaseRequirement { + ^^^^^^^^^^^^^^^ empty-attributes/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] +bar.BaseRequirement SomeThing { + ^^^^^^^^^ empty-attributes/instances.trlc:4: check error: Asil must be set +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/empty-files/output.smtlib b/tests-system/empty-files/output.smtlib new file mode 100644 index 00000000..36858edb --- /dev/null +++ b/tests-system/empty-files/output.smtlib @@ -0,0 +1,2 @@ +empty-files/foo.trlc:1:1: error: expected keyword package, encountered end-of-file instead +Processed 0 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/enum-null/output.smtlib b/tests-system/enum-null/output.smtlib new file mode 100644 index 00000000..41c702c8 --- /dev/null +++ b/tests-system/enum-null/output.smtlib @@ -0,0 +1,5 @@ +checks MyType { + ^^^^^^ enum-null/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] +bar.MyType SomeThing { + ^^^^^^^^^ enum-null/instances.trlc:4: check error: Status must be not null +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/enum-ok/output.smtlib b/tests-system/enum-ok/output.smtlib new file mode 100644 index 00000000..5077c602 --- /dev/null +++ b/tests-system/enum-ok/output.smtlib @@ -0,0 +1,3 @@ +checks MyType { + ^^^^^^ enum-ok/checks.check:4: 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) diff --git a/tests-system/enum/output.smtlib b/tests-system/enum/output.smtlib new file mode 100644 index 00000000..f8cd0755 --- /dev/null +++ b/tests-system/enum/output.smtlib @@ -0,0 +1,7 @@ +checks MyType { + ^^^^^^ enum/checks.check:2: issue: move this check block into bar.rsl:1 [deprecated_feature] +status != null , "Internal error when evaluating enum value" + ^^ enum/checks.check:4: issue: expression is always true [vcg-always-true] +bar.MyType SomeThing { + ^^^^^^^^^ enum/instances.trlc:4: check error: Status must be NEW +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 2 warning(s) and 1 error(s) diff --git a/tests-system/error-in-check/output.smtlib b/tests-system/error-in-check/output.smtlib new file mode 100644 index 00000000..8b363dac --- /dev/null +++ b/tests-system/error-in-check/output.smtlib @@ -0,0 +1,3 @@ +startsXwith(name, "Q"), error "name must start with Q", name +^^^^^^^^^^^ error-in-check/checks.check:4: error: unknown symbol startsXwith, did you mean startswith? +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/expressions/output.smtlib b/tests-system/expressions/output.smtlib new file mode 100644 index 00000000..304cb072 --- /dev/null +++ b/tests-system/expressions/output.smtlib @@ -0,0 +1,171 @@ +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/file-encoding-not-utf8/output.smtlib b/tests-system/file-encoding-not-utf8/output.smtlib new file mode 100644 index 00000000..fc04f0ee --- /dev/null +++ b/tests-system/file-encoding-not-utf8/output.smtlib @@ -0,0 +1 @@ +file-encoding-not-utf8/test.rsl: error: 'utf-8' codec can't decode byte 0xff in position 0: invalid start byte diff --git a/tests-system/freezing-1/output.smtlib b/tests-system/freezing-1/output.smtlib new file mode 100644 index 00000000..680a74e2 --- /dev/null +++ b/tests-system/freezing-1/output.smtlib @@ -0,0 +1,3 @@ +freeze n = -2 + ^ freezing-1/foo.rsl:16: check warning: n should be positive +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) diff --git a/tests-system/freezing-2/output.smtlib b/tests-system/freezing-2/output.smtlib new file mode 100644 index 00000000..0af40511 --- /dev/null +++ b/tests-system/freezing-2/output.smtlib @@ -0,0 +1,3 @@ +freeze a = 3 + ^ freezing-2/foo.rsl:6: error: duplicate freezing of a, previously frozen at foo.rsl:5 +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/freezing-3/output.smtlib b/tests-system/freezing-3/output.smtlib new file mode 100644 index 00000000..1b036a73 --- /dev/null +++ b/tests-system/freezing-3/output.smtlib @@ -0,0 +1,3 @@ +n = 42 +^ freezing-3/foo.trlc:4: error: cannot overwrite frozen component n +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/if_expressions/output.smtlib b/tests-system/if_expressions/output.smtlib new file mode 100644 index 00000000..cdffde7c --- /dev/null +++ b/tests-system/if_expressions/output.smtlib @@ -0,0 +1,7 @@ +checks T { + ^ if_expressions/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature] +T test_01 { + ^^^^^^^ if_expressions/foo.trlc:3: check error: potato +T test_01 { + ^^^^^^^ if_expressions/foo.trlc:3: check error: kitten +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 2 error(s) diff --git a/tests-system/inheritance-2/output.smtlib b/tests-system/inheritance-2/output.smtlib new file mode 100644 index 00000000..b047d47d --- /dev/null +++ b/tests-system/inheritance-2/output.smtlib @@ -0,0 +1,5 @@ +checks MyType { + ^^^^^^ inheritance-2/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] +name = "Qbert" + ^^^^^^^ inheritance-2/instances.trlc:4: check error: name must have specific length +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/inheritance/output.smtlib b/tests-system/inheritance/output.smtlib new file mode 100644 index 00000000..651fbcf4 --- /dev/null +++ b/tests-system/inheritance/output.smtlib @@ -0,0 +1,5 @@ +checks Type2 { + ^^^^^ inheritance/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] +name = "Qbert" + ^^^^^^^ inheritance/instances.trlc:4: check error: name must have specific length +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/int-literals-1/output.smtlib b/tests-system/int-literals-1/output.smtlib new file mode 100644 index 00000000..e88761ff --- /dev/null +++ b/tests-system/int-literals-1/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found no issues diff --git a/tests-system/int-literals-2/output.smtlib b/tests-system/int-literals-2/output.smtlib new file mode 100644 index 00000000..e3af1b09 --- /dev/null +++ b/tests-system/int-literals-2/output.smtlib @@ -0,0 +1,3 @@ +T test1 { v = 5.5.5 } + ^ int-literals-2/foo.trlc:3: error: decimal point is not allowed here +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/int-literals-3/output.smtlib b/tests-system/int-literals-3/output.smtlib new file mode 100644 index 00000000..2044d9e6 --- /dev/null +++ b/tests-system/int-literals-3/output.smtlib @@ -0,0 +1,3 @@ +T test1 { v = 5_ } + ^ int-literals-3/foo.trlc:3: error: base 10 digit is required here +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/int-literals-4/output.smtlib b/tests-system/int-literals-4/output.smtlib new file mode 100644 index 00000000..b84dd5fa --- /dev/null +++ b/tests-system/int-literals-4/output.smtlib @@ -0,0 +1,3 @@ +T test1 { v = 0x10.3 } + ^ int-literals-4/foo.trlc:3: error: base 16 integer may not contain a decimal point +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/int-literals-5/output.smtlib b/tests-system/int-literals-5/output.smtlib new file mode 100644 index 00000000..c1160629 --- /dev/null +++ b/tests-system/int-literals-5/output.smtlib @@ -0,0 +1,3 @@ +T test1 { v = 0bf00 } + ^ int-literals-5/foo.trlc:3: error: f is not a valid base 2 digit +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/int-literals-6/output.smtlib b/tests-system/int-literals-6/output.smtlib new file mode 100644 index 00000000..acec9aeb --- /dev/null +++ b/tests-system/int-literals-6/output.smtlib @@ -0,0 +1,5 @@ +T test1 { v = 3__3 } + ^ int-literals-6/foo.trlc:3: error: base 10 digit is required here +T test1 { v = 3__3 } + ^ int-literals-6/foo.trlc:3: error: unexpected character '_' +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 error(s) diff --git a/tests-system/int-literals-7/output.smtlib b/tests-system/int-literals-7/output.smtlib new file mode 100644 index 00000000..ce23ae3d --- /dev/null +++ b/tests-system/int-literals-7/output.smtlib @@ -0,0 +1,5 @@ +T test1 { v = 0x_3 } + ^ int-literals-7/foo.trlc:3: error: base 16 digit is required here +T test1 { v = 0x_3 } + ^ int-literals-7/foo.trlc:3: error: unexpected character '_' +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 error(s) diff --git a/tests-system/int-literals-8/output.smtlib b/tests-system/int-literals-8/output.smtlib new file mode 100644 index 00000000..ea7dc5a5 --- /dev/null +++ b/tests-system/int-literals-8/output.smtlib @@ -0,0 +1,3 @@ +T test1 { v = 0x + ^^ int-literals-8/foo.trlc:5: error: unfinished base 16 integer +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/late-packages-1/output.smtlib b/tests-system/late-packages-1/output.smtlib new file mode 100644 index 00000000..8da2d9f1 --- /dev/null +++ b/tests-system/late-packages-1/output.smtlib @@ -0,0 +1,3 @@ +package a + ^ late-packages-1/b.trlc:1: warning: duplicate late declaration of package a, previous declaration in a.trlc:1; consider adding an rsl file declaring the package +Processed 1 model(s), 0 check(s) and 2 requirement file(s) and found 1 warning(s) diff --git a/tests-system/late-packages-2/output.smtlib b/tests-system/late-packages-2/output.smtlib new file mode 100644 index 00000000..834ac5d6 --- /dev/null +++ b/tests-system/late-packages-2/output.smtlib @@ -0,0 +1 @@ +Processed 0 model(s), 0 check(s) and 2 requirement file(s) and found no issues diff --git a/tests-system/lint-ambiguous-literals/output.smtlib b/tests-system/lint-ambiguous-literals/output.smtlib new file mode 100644 index 00000000..2ee94d18 --- /dev/null +++ b/tests-system/lint-ambiguous-literals/output.smtlib @@ -0,0 +1,9 @@ +separator x + ^ lint-ambiguous-literals/foo.rsl:11: issue: x separator after integer component creates ambiguities [separator_based_literal_ambiguity] + | For example 0x"potato" would be a lexer error + | instead of the tuple segment 0 x "potato". +separator x + ^ lint-ambiguous-literals/foo.rsl:5: issue: x separator after integer component creates ambiguities [separator_based_literal_ambiguity] + | For example 0x100 would be a base 16 literal + | instead of the tuple segment 0 x 100. +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 2 warning(s) diff --git a/tests-system/lint-null/output.smtlib b/tests-system/lint-null/output.smtlib new file mode 100644 index 00000000..cbd1060f --- /dev/null +++ b/tests-system/lint-null/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found no issues diff --git a/tests-system/lint-record-refs/output.smtlib b/tests-system/lint-record-refs/output.smtlib new file mode 100644 index 00000000..ea7e3025 --- /dev/null +++ b/tests-system/lint-record-refs/output.smtlib @@ -0,0 +1,41 @@ +x, "potato" +^ lint-record-refs/test1.rsl:11: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| top_level = true +| /* derived_from is null */ +| /* x is null */ +| } +a != b implies x, "potato" + ^ lint-record-refs/test2.rsl:10: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | a = T_instance_1 + | b = T_instance_0 + | /* x is null */ + | } +a == b implies x, "potato" + ^ lint-record-refs/test2.rsl:11: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | a = T_instance_0 + | b = T_instance_0 + | /* x is null */ + | } +a != b implies x, "potato" + ^ lint-record-refs/test3.rsl:11: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | a = Other.T_instance_1 + | b = Other.T_instance_0 + | /* x is null */ + | } +a == b implies x, "potato" + ^ lint-record-refs/test3.rsl:12: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | a = Other.T_instance_0 + | b = Other.T_instance_0 + | /* x is null */ + | } +Processed 4 model(s), 0 check(s) and 0 requirement file(s) and found 5 warning(s) diff --git a/tests-system/lint-vcg-arrays/output.smtlib b/tests-system/lint-vcg-arrays/output.smtlib new file mode 100644 index 00000000..5543522b --- /dev/null +++ b/tests-system/lint-vcg-arrays/output.smtlib @@ -0,0 +1,24 @@ +x, "potato" +^ lint-vcg-arrays/test1.rsl:13: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| arr1 = [] +| arr2 = [Colour.Blue, Colour.Blue, Colour.Blue] +| arr3 = ["", "", ""] +| /* x is null */ +| } +arr1[x] > 0, "potato" + ^ lint-vcg-arrays/test2.rsl:11: issue: array index could be less than 0 [vcg-array-index] + | example record_type triggering error: + | T bad_potato { + | arr1 = [-2, 42, 666] + | x = -1 + | } +arr1[x] > 0, "potato" + ^ lint-vcg-arrays/test2.rsl:11: issue: array index could be larger than len(arr1) [vcg-array-index] + | example record_type triggering error: + | T bad_potato { + | arr1 = [-1, 42, 666] + | x = 3 + | } +Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 3 warning(s) diff --git a/tests-system/lint-vcg-basic/output.smtlib b/tests-system/lint-vcg-basic/output.smtlib new file mode 100644 index 00000000..666d3f1e --- /dev/null +++ b/tests-system/lint-vcg-basic/output.smtlib @@ -0,0 +1,55 @@ +y != null implies x > 1, warning "potato" + ^ lint-vcg-basic/test1.rsl:11: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T1 bad_potato { + | /* x is null */ + | y = 0 + | z = 0 + | } +x != 0, warning "potato" + ^^ lint-vcg-basic/test2.rsl:9: issue: expression is always true [vcg-always-true] +x, "potato" +^ lint-vcg-basic/test3.rsl:9: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T3 bad_potato { +| /* x is null */ +| y = false +| } +x, "wibble" +^ lint-vcg-basic/test4.rsl:16: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T4 bad_potato { +| a = Colour.Green +| b = Colour.Red +| c = Colour.Blue +| d = Colour.Blue +| /* x is null */ +| } +x, "wibble" +^ lint-vcg-basic/test4.rsl:23: issue: expression is always true [vcg-always-true] +a == b / (c + d * 2), "potato" + ^ lint-vcg-basic/test5.rsl:12: issue: divisor could be 0 [vcg-div-by-zero] + | example record_type triggering error: + | T bad_potato { + | a = 0 + | b = 0 + | c = 10 + | d = -5 + | } +a == b % (c + d * 2), "potato" + ^ lint-vcg-basic/test6.rsl:13: issue: divisor could be 0 [vcg-div-by-zero] + | example record_type triggering error: + | T bad_potato { + | a = 0 + | b = -1 + | c = 10 + | d = -5 + | } +13 % ((-a) % b + 7) > 0, "potato" + ^ lint-vcg-basic/test7.rsl:11: issue: divisor could be 0 [vcg-div-by-zero] + | example record_type triggering error: + | T bad_potato { + | a = 19 + | b = 12 + | } +Processed 7 model(s), 0 check(s) and 0 requirement file(s) and found 8 warning(s) diff --git a/tests-system/lint-vcg-connectives/output.smtlib b/tests-system/lint-vcg-connectives/output.smtlib new file mode 100644 index 00000000..e8182795 --- /dev/null +++ b/tests-system/lint-vcg-connectives/output.smtlib @@ -0,0 +1,16 @@ +c, "wibble" +^ lint-vcg-connectives/test1.rsl:11: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| x = 10 +| /* c is null */ +| } +y == -5 implies c, "wibble" + ^ lint-vcg-connectives/test2.rsl:11: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | x = 1 + | y = -5 + | /* c is null */ + | } +Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 2 warning(s) diff --git a/tests-system/lint-vcg-decimal/output.smtlib b/tests-system/lint-vcg-decimal/output.smtlib new file mode 100644 index 00000000..c4e06379 --- /dev/null +++ b/tests-system/lint-vcg-decimal/output.smtlib @@ -0,0 +1,21 @@ +x, "potato" +^ lint-vcg-decimal/test1.rsl:12: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| a = -1.0 +| b = 0.0 +| /* x is null */ +| } +1.0 / (a + (1.0 / 3.0)) > 0.0, fatal "potato" + ^ lint-vcg-decimal/test2.rsl:8: issue: divisor could be 0.0 [vcg-div-by-zero] + | example record_type triggering error: + | T bad_potato { + | a = -1 / 3 + | } +1.0 / (a - 58.50823) > 0.0, "potato" + ^ lint-vcg-decimal/test3.rsl:8: issue: divisor could be 0.0 [vcg-div-by-zero] + | example record_type triggering error: + | T bad_potato { + | a = 58.50823 + | } +Processed 3 model(s), 0 check(s) and 0 requirement file(s) and found 3 warning(s) diff --git a/tests-system/lint-vcg-empty-enum/output.smtlib b/tests-system/lint-vcg-empty-enum/output.smtlib new file mode 100644 index 00000000..fc7309bf --- /dev/null +++ b/tests-system/lint-vcg-empty-enum/output.smtlib @@ -0,0 +1,3 @@ +enum E {} + ^ lint-vcg-empty-enum/foo.rsl:3: error: empty enumerations are not permitted +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/lint-vcg-frozen/output.smtlib b/tests-system/lint-vcg-frozen/output.smtlib new file mode 100644 index 00000000..cbd1060f --- /dev/null +++ b/tests-system/lint-vcg-frozen/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found no issues diff --git a/tests-system/lint-vcg-int-real/output.smtlib b/tests-system/lint-vcg-int-real/output.smtlib new file mode 100644 index 00000000..0e9cdebd --- /dev/null +++ b/tests-system/lint-vcg-int-real/output.smtlib @@ -0,0 +1,18 @@ +x, "potato" +^ lint-vcg-int-real/test1.rsl:14: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| num = 157 +| den = 50 +| r = 3.14 +| /* x is null */ +| } +x, "potato" +^ lint-vcg-int-real/test2.rsl:12: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| i = -3 +| r = -3.14 +| /* x is null */ +| } +Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 2 warning(s) diff --git a/tests-system/lint-vcg-ite/output.smtlib b/tests-system/lint-vcg-ite/output.smtlib new file mode 100644 index 00000000..6790035b --- /dev/null +++ b/tests-system/lint-vcg-ite/output.smtlib @@ -0,0 +1,17 @@ +(if a > 0 then x + ^ lint-vcg-ite/test1.rsl:10: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | a = 1 + | /* x is null */ + | /* y is null */ + | } +elsif a < 0 then y + ^ lint-vcg-ite/test1.rsl:11: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | a = -1 + | /* x is null */ + | /* y is null */ + | } +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 2 warning(s) diff --git a/tests-system/lint-vcg-membership/output.smtlib b/tests-system/lint-vcg-membership/output.smtlib new file mode 100644 index 00000000..9d7c4fed --- /dev/null +++ b/tests-system/lint-vcg-membership/output.smtlib @@ -0,0 +1,10 @@ +c, "wibble" +^ lint-vcg-membership/test1.rsl:13: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| x = 0 +| y = -1 +| z = 0 +| /* c is null */ +| } +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s) diff --git a/tests-system/lint-vcg-power/output.smtlib b/tests-system/lint-vcg-power/output.smtlib new file mode 100644 index 00000000..7ad6e2f3 --- /dev/null +++ b/tests-system/lint-vcg-power/output.smtlib @@ -0,0 +1,17 @@ +c, "wibble" +^ lint-vcg-power/test1.rsl:12: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| x = -9 +| y = 81 +| /* c is null */ +| } +c, "wibble" +^ lint-vcg-power/test2.rsl:12: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| x = /* unable to generate precise value */ +| y = 30.0 +| /* c is null */ +| } +Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 2 warning(s) diff --git a/tests-system/lint-vcg-quant/output.smtlib b/tests-system/lint-vcg-quant/output.smtlib new file mode 100644 index 00000000..70e168cb --- /dev/null +++ b/tests-system/lint-vcg-quant/output.smtlib @@ -0,0 +1,20 @@ +c, "potato" +^ lint-vcg-quant/test1.rsl:10: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| arr = [1, 1, 1] +| /* c is null */ +| } +| /* note: counter-example is unreliable in this case */ +len(positives) > 0 implies 5 / positives[0] > 0, "potato" + ^ lint-vcg-quant/test3.rsl:19: issue: divisor could be 0 [vcg-div-by-zero] + | example record_type triggering error: + | T bad_potato { + | arr = [2] + | positives = [0] + | negatives = [] + | zeros = [] + | /* c is null */ + | } + | /* note: counter-example is unreliable in this case */ +Processed 3 model(s), 0 check(s) and 0 requirement file(s) and found 2 warning(s) diff --git a/tests-system/lint-vcg-strings/output.smtlib b/tests-system/lint-vcg-strings/output.smtlib new file mode 100644 index 00000000..036bfc34 --- /dev/null +++ b/tests-system/lint-vcg-strings/output.smtlib @@ -0,0 +1,7 @@ +y, "potato" +^ lint-vcg-strings/test1.rsl:15: issue: expression could be null [vcg-evaluation-of-null] +c, "potato" +^ lint-vcg-strings/test2.rsl:14: issue: expression could be null [vcg-evaluation-of-null] +c, warning "potato" +^ lint-vcg-strings/test3.rsl:11: issue: expression could be null [vcg-evaluation-of-null] +Processed 3 model(s), 0 check(s) and 0 requirement file(s) and found 3 warning(s) diff --git a/tests-system/lint-vcg-tuple/output.smtlib b/tests-system/lint-vcg-tuple/output.smtlib new file mode 100644 index 00000000..2ae4cd91 --- /dev/null +++ b/tests-system/lint-vcg-tuple/output.smtlib @@ -0,0 +1,31 @@ +c, "potato" +^ lint-vcg-tuple/test1.rsl:15: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| x = 1 +| y = 2 +| p = -1 +| q = -3 +| /* c is null */ +| } +then x.version > 5 + ^^^^^^^ lint-vcg-tuple/test2.rsl:10: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | x = 501 + | } +else x.version < 5), warning "potato" + ^^^^^^^ lint-vcg-tuple/test2.rsl:11: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | x = 1 + | } +c, "potato" +^ lint-vcg-tuple/test3.rsl:12: issue: expression could be null [vcg-evaluation-of-null] +| example record_type triggering error: +| T bad_potato { +| x = 1@1 +| y = 1 +| /* c is null */ +| } +Processed 5 model(s), 0 check(s) and 0 requirement file(s) and found 4 warning(s) diff --git a/tests-system/markup-1/output.smtlib b/tests-system/markup-1/output.smtlib new file mode 100644 index 00000000..e88761ff --- /dev/null +++ b/tests-system/markup-1/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found no issues diff --git a/tests-system/markup-2/output.smtlib b/tests-system/markup-2/output.smtlib new file mode 100644 index 00000000..bf8e4d67 --- /dev/null +++ b/tests-system/markup-2/output.smtlib @@ -0,0 +1,3 @@ +M = "see [[Baz.foo]]" + ^^^ markup-2/bar.trlc:18: error: package must be imported before use +Processed 2 model(s), 0 check(s) and 3 requirement file(s) and found 1 error(s) diff --git a/tests-system/markup-3/output.smtlib b/tests-system/markup-3/output.smtlib new file mode 100644 index 00000000..2ba9f916 --- /dev/null +++ b/tests-system/markup-3/output.smtlib @@ -0,0 +1,3 @@ +M = "[[Test_3]]" + ^^^^^^ markup-3/foo.trlc:8: error: unknown symbol Test_3, did you mean Test_2? +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/mult/output.smtlib b/tests-system/mult/output.smtlib new file mode 100644 index 00000000..31e6fc25 --- /dev/null +++ b/tests-system/mult/output.smtlib @@ -0,0 +1,15 @@ +checks MyType { + ^^^^^^ mult/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] +mult String [5..3] + ^ mult/bar.rsl:23: issue: upper bound must be at least 5 [impossible_array_types] +mult String [0..0] + ^ mult/bar.rsl:17: issue: this array makes no sense [impossible_array_types] +mult = [ "A", "B"] + ^ mult/instances.trlc:6: error: this array requires at least 5 elements (only 2 provided) +mult = [ "A", "B"] + ^ mult/instances.trlc:16: error: this array requires at least 5 elements (only 2 provided) +mult = [ "A", "B"] + ^ mult/instances.trlc:21: error: this array requires at least 3 elements (only 2 provided) +bar.MyType SomeThing { + ^^^^^^^^^ mult/instances.trlc:4: check error: mult must have 3 elements +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 3 warning(s) and 4 error(s) diff --git a/tests-system/multiple-check-expressions/output.smtlib b/tests-system/multiple-check-expressions/output.smtlib new file mode 100644 index 00000000..bde6c6f3 --- /dev/null +++ b/tests-system/multiple-check-expressions/output.smtlib @@ -0,0 +1,7 @@ +checks MyType { + ^^^^^^ multiple-check-expressions/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] +name = "Aberx" + ^^^^^^^ multiple-check-expressions/instances.trlc:5: check error: name must start with Q +name = "Aberx" + ^^^^^^^ multiple-check-expressions/instances.trlc:5: check error: name must end with t +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 2 error(s) diff --git a/tests-system/multiple-models/output.smtlib b/tests-system/multiple-models/output.smtlib new file mode 100644 index 00000000..ee7b5b6b --- /dev/null +++ b/tests-system/multiple-models/output.smtlib @@ -0,0 +1,11 @@ +checks T { + ^ multiple-models/bar.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] +checks T { + ^ multiple-models/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature] +Foo.T test1 { + ^^^^^ multiple-models/foo.trlc:4: check error: this is not a good name +Bar.T test2 { + ^^^^^ multiple-models/foo.trlc:8: check error: this is not a good name +Bar.T test2 { + ^^^^^ multiple-models/foo.trlc:8: check error: also not a good name +Processed 2 model(s), 2 check(s) and 3 requirement file(s) and found 2 warning(s) and 3 error(s) diff --git a/tests-system/name-shadowing-1/output.smtlib b/tests-system/name-shadowing-1/output.smtlib new file mode 100644 index 00000000..ae3b1e94 --- /dev/null +++ b/tests-system/name-shadowing-1/output.smtlib @@ -0,0 +1,3 @@ +T Foo {} + ^^^ name-shadowing-1/foo.trlc:3: error: duplicate definition, previous definition at foo.rsl:1 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/names_unique_globally/output.smtlib b/tests-system/names_unique_globally/output.smtlib new file mode 100644 index 00000000..5c2ec7b1 --- /dev/null +++ b/tests-system/names_unique_globally/output.smtlib @@ -0,0 +1,5 @@ +A.L L1 { + ^^ names_unique_globally/f1.trlc:4: error: required component l (see def.rsl:4) is not defined +A.L L1 { + ^^ names_unique_globally/f2.trlc:3: error: duplicate definition, previous definition at f1.trlc:4 +Processed 1 model(s), 0 check(s) and 2 requirement file(s) and found 2 error(s) diff --git a/tests-system/negative-values/output.smtlib b/tests-system/negative-values/output.smtlib new file mode 100644 index 00000000..2f2d6921 --- /dev/null +++ b/tests-system/negative-values/output.smtlib @@ -0,0 +1,7 @@ +val = -5 + ^ negative-values/foo.trlc:4: check warning: potato +val = 5 + ^ negative-values/foo.trlc:10: check warning: potato +val = +5 + ^ negative-values/foo.trlc:13: check warning: potato +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s) diff --git a/tests-system/null-expr-1/output.smtlib b/tests-system/null-expr-1/output.smtlib new file mode 100644 index 00000000..fa5b9a16 --- /dev/null +++ b/tests-system/null-expr-1/output.smtlib @@ -0,0 +1,3 @@ +null == null, "potato" + ^^ null-expr-1/test_01.rsl:9: issue: expression is always true [vcg-always-true] +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s) diff --git a/tests-system/null-value/output.smtlib b/tests-system/null-value/output.smtlib new file mode 100644 index 00000000..764387ba --- /dev/null +++ b/tests-system/null-value/output.smtlib @@ -0,0 +1,7 @@ +checks MyType { + ^^^^^^ null-value/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] +other != null , "Other must not be null", other + ^^ null-value/checks.check:4: issue: expression is always true [vcg-always-true] +bar.MyType SomeThing { + ^^^^^^^^^ null-value/instances.trlc:4: error: required component other (see bar.rsl:5) is not defined +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 2 warning(s) and 1 error(s) diff --git a/tests-system/preamble-1/output.smtlib b/tests-system/preamble-1/output.smtlib new file mode 100644 index 00000000..f6edc7bb --- /dev/null +++ b/tests-system/preamble-1/output.smtlib @@ -0,0 +1,6 @@ +import Potato +^^^^^^ preamble-1/bar.rsl:1: error: expected keyword package, encountered keyword import instead +import Baz + ^^^ preamble-1/baz.rsl:2: error: package Baz cannot import itself +type T {} +^^^^ preamble-1/foo.rsl:1: error: expected keyword package, encountered keyword type instead diff --git a/tests-system/quantifiers/output.smtlib b/tests-system/quantifiers/output.smtlib new file mode 100644 index 00000000..7275156d --- /dev/null +++ b/tests-system/quantifiers/output.smtlib @@ -0,0 +1,21 @@ +arr = [] + ^ quantifiers/foo.trlc:10: check warning: not everything is 42 +arr = [] + ^ quantifiers/foo.trlc:10: check warning: nothing is 42 +arr = [40, 41, 42, 43, 44] + ^ quantifiers/foo.trlc:22: check warning: not everything is 42 +arr = [40, 41, 42, 43, 44] + ^ quantifiers/foo.trlc:22: check warning: nothing is 42 +arr = [1, 2, 3] + ^ quantifiers/foo.trlc:34: check warning: not everything is 42 +arr = [1, 2, 3] + ^ quantifiers/foo.trlc:34: check warning: nothing is 42 +arr = [42, 0, 42] + ^ quantifiers/foo.trlc:46: check warning: not everything is 42 +arr = [42, 0, 42] + ^ quantifiers/foo.trlc:46: check warning: nothing is 42 +arr = [42, 42] + ^ quantifiers/foo.trlc:58: check warning: not everything is 42 +arr = [42, 42] + ^ quantifiers/foo.trlc:58: check warning: nothing is 42 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 10 warning(s) diff --git a/tests-system/recovery-1/output.smtlib b/tests-system/recovery-1/output.smtlib new file mode 100644 index 00000000..fe9006ca --- /dev/null +++ b/tests-system/recovery-1/output.smtlib @@ -0,0 +1,7 @@ +type Q { +^^^^ recovery-1/test_1.rsl:6: error: expected identifier, encountered keyword instead +i really <3 potato +^ recovery-1/test_1.trlc:12: error: unknown symbol i +kitten = 99 +^^^^^^ recovery-1/test_1.trlc:15: error: unknown symbol kitten +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 error(s) diff --git a/tests-system/redefined-attribute/output.smtlib b/tests-system/redefined-attribute/output.smtlib new file mode 100644 index 00000000..edd17d0a --- /dev/null +++ b/tests-system/redefined-attribute/output.smtlib @@ -0,0 +1,5 @@ +checks MyType { + ^^^^^^ redefined-attribute/checks.check:2: issue: move this check block into bar.rsl:1 [deprecated_feature] +name = "Xbert" // does start with Q + ^^^^^^^ redefined-attribute/instances.trlc:5: check error: name must start with Q +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/sections-1/output.smtlib b/tests-system/sections-1/output.smtlib new file mode 100644 index 00000000..e88761ff --- /dev/null +++ b/tests-system/sections-1/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found no issues diff --git a/tests-system/simple-info-warn-error/output.smtlib b/tests-system/simple-info-warn-error/output.smtlib new file mode 100644 index 00000000..404fd54f --- /dev/null +++ b/tests-system/simple-info-warn-error/output.smtlib @@ -0,0 +1,51 @@ +checks MyType { + ^^^^^^ simple-info-warn-error/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] +matches(name, "^D.*"), error "name must start with D", name + ^^^^ simple-info-warn-error/checks.check:4: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | MyType bad_potato { + | /* name is null */ + | } +matches(name, "^E.*"), error "name must start with E", name + ^^^^ simple-info-warn-error/checks.check:5: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | MyType bad_potato { + | /* name is null */ + | } +matches(name, "^W.*"), warning "name must start with W", name + ^^^^ simple-info-warn-error/checks.check:6: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | MyType bad_potato { + | /* name is null */ + | } +matches(name, "^I.*"), warning "name must start with I", name + ^^^^ simple-info-warn-error/checks.check:7: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | MyType bad_potato { + | /* name is null */ + | } +name = "Qbert" // does start with Q + ^^^^^^^ simple-info-warn-error/instances.trlc:5: check error: name must start with D +name = "Qbert" // does start with Q + ^^^^^^^ simple-info-warn-error/instances.trlc:5: check error: name must start with E +name = "Qbert" // does start with Q + ^^^^^^^ simple-info-warn-error/instances.trlc:5: check warning: name must start with W +name = "Qbert" // does start with Q + ^^^^^^^ simple-info-warn-error/instances.trlc:5: check warning: name must start with I +name = "Abert" + ^^^^^^^ simple-info-warn-error/instances.trlc:9: check error: name must start with D +name = "Abert" + ^^^^^^^ simple-info-warn-error/instances.trlc:9: check error: name must start with E +name = "Abert" + ^^^^^^^ simple-info-warn-error/instances.trlc:9: check warning: name must start with W +name = "Abert" + ^^^^^^^ simple-info-warn-error/instances.trlc:9: check warning: name must start with I +name = "BBert" + ^^^^^^^ simple-info-warn-error/instances.trlc:13: check error: name must start with D +name = "BBert" + ^^^^^^^ simple-info-warn-error/instances.trlc:13: check error: name must start with E +name = "BBert" + ^^^^^^^ simple-info-warn-error/instances.trlc:13: check warning: name must start with W +name = "BBert" + ^^^^^^^ simple-info-warn-error/instances.trlc:13: check warning: name must start with I +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 11 warning(s) and 6 error(s) diff --git a/tests-system/simple-instance-type-reference/output.smtlib b/tests-system/simple-instance-type-reference/output.smtlib new file mode 100644 index 00000000..e88761ff --- /dev/null +++ b/tests-system/simple-instance-type-reference/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found no issues diff --git a/tests-system/simple-more-than-one/output.smtlib b/tests-system/simple-more-than-one/output.smtlib new file mode 100644 index 00000000..e07aba3b --- /dev/null +++ b/tests-system/simple-more-than-one/output.smtlib @@ -0,0 +1,13 @@ +checks MyType { + ^^^^^^ simple-more-than-one/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] +matches(name, "^Q.*"), error "name must start with Q", name + ^^^^ simple-more-than-one/checks.check:4: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | MyType bad_potato { + | /* name is null */ + | } +name = "Abert" + ^^^^^^^ simple-more-than-one/instances.trlc:9: check error: name must start with Q +name = "BBert" + ^^^^^^^ simple-more-than-one/instances.trlc:13: check error: name must start with Q +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 2 warning(s) and 2 error(s) diff --git a/tests-system/simple/output.smtlib b/tests-system/simple/output.smtlib new file mode 100644 index 00000000..2caadc10 --- /dev/null +++ b/tests-system/simple/output.smtlib @@ -0,0 +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) diff --git a/tests-system/strings/output.smtlib b/tests-system/strings/output.smtlib new file mode 100644 index 00000000..1b80d9be --- /dev/null +++ b/tests-system/strings/output.smtlib @@ -0,0 +1,3 @@ +checks T { + ^ strings/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature] +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) diff --git a/tests-system/tuples-1/output.smtlib b/tests-system/tuples-1/output.smtlib new file mode 100644 index 00000000..4e3cca22 --- /dev/null +++ b/tests-system/tuples-1/output.smtlib @@ -0,0 +1,11 @@ +baseline >= 1.0, error "Baseline must be at least 1.0", baseline +^^^^^^^^ tuples-1/foo.rsl:46: issue: expression could be null [vcg-evaluation-of-null] + | example tuple_type triggering error: + | Doors_Item bad_potato { + | module_id = 0 + | item_id = 0 + | /* baseline is null */ + | } +cb_link = 12345 // Equivalent to 12345@null + ^^^^^ tuples-1/foo.trlc:12: check warning: Please link to a specific version +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 warning(s) diff --git a/tests-system/tuples-10/output.smtlib b/tests-system/tuples-10/output.smtlib new file mode 100644 index 00000000..2c1cc05b --- /dev/null +++ b/tests-system/tuples-10/output.smtlib @@ -0,0 +1,13 @@ +a T +^ tuples-10/foo.rsl:10: error: tuple type Q, which contains separators, may not contain another tuple with separators +x Q + ^ tuples-10/foo.rsl:16: error: unknown symbol Q +x = 1 @ 2 @ 3 @ 4 +^ tuples-10/foo.trlc:4: error: unknown symbol x +x = 1 @ 2 @ 3 +^ tuples-10/foo.trlc:8: error: unknown symbol x +x = 1 @ 2 +^ tuples-10/foo.trlc:12: error: unknown symbol x +x = 1 +^ tuples-10/foo.trlc:16: error: unknown symbol x +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 6 error(s) diff --git a/tests-system/tuples-11/output.smtlib b/tests-system/tuples-11/output.smtlib new file mode 100644 index 00000000..ae32f4f2 --- /dev/null +++ b/tests-system/tuples-11/output.smtlib @@ -0,0 +1,13 @@ +a T +^ tuples-11/foo.rsl:10: error: tuple type Q, which contains separators, may not contain another tuple with separators +x Q + ^ tuples-11/foo.rsl:16: error: unknown symbol Q +x = 1 +^ tuples-11/foo.trlc:4: error: unknown symbol x +x = 1 @ 1 +^ tuples-11/foo.trlc:8: error: unknown symbol x +x = 1 @ "foo" +^ tuples-11/foo.trlc:12: error: unknown symbol x +x = 1 @ 1 @ "foo" +^ tuples-11/foo.trlc:16: error: unknown symbol x +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 6 error(s) diff --git a/tests-system/tuples-2/output.smtlib b/tests-system/tuples-2/output.smtlib new file mode 100644 index 00000000..ef3111fc --- /dev/null +++ b/tests-system/tuples-2/output.smtlib @@ -0,0 +1,3 @@ +foo = 1 potato = potato // this is NOT ok + ^ tuples-2/foo.trlc:10: error: expected integer literal, encountered = instead +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/tuples-3/output.smtlib b/tests-system/tuples-3/output.smtlib new file mode 100644 index 00000000..e88761ff --- /dev/null +++ b/tests-system/tuples-3/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found no issues diff --git a/tests-system/tuples-4/output.smtlib b/tests-system/tuples-4/output.smtlib new file mode 100644 index 00000000..666baa1c --- /dev/null +++ b/tests-system/tuples-4/output.smtlib @@ -0,0 +1,12 @@ +f2 >= 0, warning "potato2", f2 +^^ tuples-4/foo.rsl:12: issue: expression could be null [vcg-evaluation-of-null] + | example tuple_type triggering error: + | T bad_potato { + | f1 = R1_instance_0 + | /* f2 is null */ + | } +t = potato + ^^^^^^ tuples-4/foo.trlc:6: error: lhs of check f2 >= 0 (foo.rsl:12) must not be null +t = potato@-42 + ^ tuples-4/foo.trlc:14: check warning: potato2 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 warning(s) and 1 error(s) diff --git a/tests-system/tuples-5/output.smtlib b/tests-system/tuples-5/output.smtlib new file mode 100644 index 00000000..f965453e --- /dev/null +++ b/tests-system/tuples-5/output.smtlib @@ -0,0 +1,3 @@ +t = potato@-42 + ^ tuples-5/foo.trlc:14: check warning: potato2 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) diff --git a/tests-system/tuples-6/output.smtlib b/tests-system/tuples-6/output.smtlib new file mode 100644 index 00000000..c92f0105 --- /dev/null +++ b/tests-system/tuples-6/output.smtlib @@ -0,0 +1,3 @@ +c = [(1, 0) verified true, + ^^^^ tuples-6/foo.trlc:10: check warning: potato +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) diff --git a/tests-system/tuples-7/output.smtlib b/tests-system/tuples-7/output.smtlib new file mode 100644 index 00000000..8054b6f5 --- /dev/null +++ b/tests-system/tuples-7/output.smtlib @@ -0,0 +1,3 @@ +z optional Integer + ^^^^^^^^ tuples-7/foo.rsl:6: error: optional only permitted in tuples with separators +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/tuples-8/output.smtlib b/tests-system/tuples-8/output.smtlib new file mode 100644 index 00000000..56d266a0 --- /dev/null +++ b/tests-system/tuples-8/output.smtlib @@ -0,0 +1,3 @@ +separator @ +^^^^^^^^^ tuples-8/foo.rsl:6: error: either all fields must be separated, or none +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/tuples-9/output.smtlib b/tests-system/tuples-9/output.smtlib new file mode 100644 index 00000000..0a4b975a --- /dev/null +++ b/tests-system/tuples-9/output.smtlib @@ -0,0 +1,3 @@ +cdr optional List + ^^^^ tuples-9/foo.rsl:6: error: unknown symbol List +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s) diff --git a/tests-system/tutorial-1/output.smtlib b/tests-system/tutorial-1/output.smtlib new file mode 100644 index 00000000..a87e4973 --- /dev/null +++ b/tests-system/tutorial-1/output.smtlib @@ -0,0 +1,3 @@ +Requirement fuel { + ^^^^ tutorial-1/car.trlc:13: error: required component critical (see model.rsl:5) is not defined +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/tutorial-2/output.smtlib b/tests-system/tutorial-2/output.smtlib new file mode 100644 index 00000000..01352ab3 --- /dev/null +++ b/tests-system/tutorial-2/output.smtlib @@ -0,0 +1,5 @@ +checks Requirement { + ^^^^^^^^^^^ tutorial-2/example.check:3: issue: move this check block into example.rsl:1 [deprecated_feature] +description = "potato" + ^^^^^^^^ tutorial-2/example.trlc:4: check warning: this is not very descriptive +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 2 warning(s) diff --git a/tests-system/type-qualifiers-1/output.smtlib b/tests-system/type-qualifiers-1/output.smtlib new file mode 100644 index 00000000..9c1f1b9f --- /dev/null +++ b/tests-system/type-qualifiers-1/output.smtlib @@ -0,0 +1,6 @@ +type T4 extends T3 { + ^^ type-qualifiers-1/foo.rsl:15: issue: consider clarifying that this record is final [clarify_final] + | Parent record Foo.T3 is final, making this record + | also final. Marking it explicitly as final + | clarifies this to casual readers. +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) diff --git a/tests-system/type-qualifiers-2/output.smtlib b/tests-system/type-qualifiers-2/output.smtlib new file mode 100644 index 00000000..7c6eec5e --- /dev/null +++ b/tests-system/type-qualifiers-2/output.smtlib @@ -0,0 +1,8 @@ +type T4 extends T3 { + ^^ type-qualifiers-2/foo.rsl:15: issue: consider clarifying that this record is final [clarify_final] + | Parent record Foo.T3 is final, making this record + | also final. Marking it explicitly as final + | clarifies this to casual readers. +T1 test_1 { +^^ type-qualifiers-2/foo.trlc:3: error: cannot declare object of abstract record type T1 +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/type-qualifiers-3/output.smtlib b/tests-system/type-qualifiers-3/output.smtlib new file mode 100644 index 00000000..46fde73a --- /dev/null +++ b/tests-system/type-qualifiers-3/output.smtlib @@ -0,0 +1,13 @@ +type T4 extends T3 { + ^^ type-qualifiers-3/foo.rsl:15: issue: consider clarifying that this record is final [clarify_final] + | Parent record Foo.T3 is final, making this record + | also final. Marking it explicitly as final + | clarifies this to casual readers. +type T5 extends T4 { + ^^ type-qualifiers-3/foo.rsl:19: issue: consider clarifying that this record is final [clarify_final] + | Parent record Foo.T4 is final, making this record + | also final. Marking it explicitly as final + | clarifies this to casual readers. +w Integer +^ type-qualifiers-3/foo.rsl:20: error: cannot declare new components in final record type +Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 2 warning(s) and 1 error(s) diff --git a/tests-system/type-qualifiers-4/output.smtlib b/tests-system/type-qualifiers-4/output.smtlib new file mode 100644 index 00000000..aef8c6e5 --- /dev/null +++ b/tests-system/type-qualifiers-4/output.smtlib @@ -0,0 +1,3 @@ +abstract type T2 {} + ^^ type-qualifiers-4/foo.rsl:5: issue: abstract type T2 does not have any extensions [abstract_leaf_types] +Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s) diff --git a/tests-system/typesystem-1/output.smtlib b/tests-system/typesystem-1/output.smtlib new file mode 100644 index 00000000..cb52a295 --- /dev/null +++ b/tests-system/typesystem-1/output.smtlib @@ -0,0 +1,3 @@ +name = 5 + ^ typesystem-1/instances.trlc:5: error: expected string literal, encountered integer literal instead +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/typesystem-2/output.smtlib b/tests-system/typesystem-2/output.smtlib new file mode 100644 index 00000000..87068f1a --- /dev/null +++ b/tests-system/typesystem-2/output.smtlib @@ -0,0 +1,7 @@ +i = 5.0 + ^^^ typesystem-2/foo.trlc:4: error: expected integer literal, encountered decimal literal instead +i = 5.2 + ^^^ typesystem-2/foo.trlc:8: error: expected integer literal, encountered decimal literal instead +d = 5 + ^ typesystem-2/foo.trlc:12: error: expected decimal literal, encountered integer literal instead +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 error(s) diff --git a/tests-system/typesystem-mismatch-enums/output.smtlib b/tests-system/typesystem-mismatch-enums/output.smtlib new file mode 100644 index 00000000..2296c34d --- /dev/null +++ b/tests-system/typesystem-mismatch-enums/output.smtlib @@ -0,0 +1,3 @@ +asil = bar.Status.DEPRECATED + ^^^^^^ typesystem-mismatch-enums/instances.trlc:6: error: expected ASIL +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/typesystem-ok/output.smtlib b/tests-system/typesystem-ok/output.smtlib new file mode 100644 index 00000000..e88761ff --- /dev/null +++ b/tests-system/typesystem-ok/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found no issues diff --git a/tests-system/unary-ops-1/output.smtlib b/tests-system/unary-ops-1/output.smtlib new file mode 100644 index 00000000..d478f463 --- /dev/null +++ b/tests-system/unary-ops-1/output.smtlib @@ -0,0 +1,3 @@ +-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/unicode/output.smtlib b/tests-system/unicode/output.smtlib new file mode 100644 index 00000000..f74b35f2 --- /dev/null +++ b/tests-system/unicode/output.smtlib @@ -0,0 +1,5 @@ +bar.MyType Übergrößenträger { + ^ unicode/instances.trlc:4: error: unexpected character 'Ü' +bar.MyType Übergrößenträger { + ^ unicode/instances.trlc:4: error: unexpected character 'ö' +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 error(s) diff --git a/tests-system/value-converter/output.smtlib b/tests-system/value-converter/output.smtlib new file mode 100644 index 00000000..e88761ff --- /dev/null +++ b/tests-system/value-converter/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found no issues diff --git a/tests-system/value-exact/output.smtlib b/tests-system/value-exact/output.smtlib new file mode 100644 index 00000000..61805bb1 --- /dev/null +++ b/tests-system/value-exact/output.smtlib @@ -0,0 +1,5 @@ +checks MyType { + ^^^^^^ value-exact/checks.check:4: issue: move this check block into bar.rsl:1 [deprecated_feature] +name = "xbert" // does start with Q + ^^^^^^^ value-exact/instances.trlc:5: check error: name must be 'Qbert' +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/visibility-1/output.smtlib b/tests-system/visibility-1/output.smtlib new file mode 100644 index 00000000..95faa136 --- /dev/null +++ b/tests-system/visibility-1/output.smtlib @@ -0,0 +1,3 @@ +Foo.T {} +^^^ visibility-1/bar.trlc:3: error: package must be imported before use +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/whitespace/output.smtlib b/tests-system/whitespace/output.smtlib new file mode 100644 index 00000000..6106aec3 --- /dev/null +++ b/tests-system/whitespace/output.smtlib @@ -0,0 +1 @@ +Processed 0 model(s), 0 check(s) and 1 requirement file(s) and found no issues diff --git a/tests-system/xbase-operators/output.smtlib b/tests-system/xbase-operators/output.smtlib new file mode 100644 index 00000000..d8ecf197 --- /dev/null +++ b/tests-system/xbase-operators/output.smtlib @@ -0,0 +1,5 @@ +checks MyType { + ^^^^^^ xbase-operators/checks.check:2: issue: move this check block into bar.rsl:1 [deprecated_feature] +name = "Qbert" // does start with Q + ^^^^^^^ xbase-operators/instances.trlc:5: check error: Must fail +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/xref-2/output.smtlib b/tests-system/xref-2/output.smtlib new file mode 100644 index 00000000..96b59571 --- /dev/null +++ b/tests-system/xref-2/output.smtlib @@ -0,0 +1,3 @@ +link != null implies link.status == bar.Status.NEW, "Must be linked to new" + ^^^^ xref-2/checks.check:4: error: expression 'link' has type MyType, which is not a tuple +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/xref-correct-lowercase/output.smtlib b/tests-system/xref-correct-lowercase/output.smtlib new file mode 100644 index 00000000..d8487509 --- /dev/null +++ b/tests-system/xref-correct-lowercase/output.smtlib @@ -0,0 +1,3 @@ +checks MyType { + ^^^^^^ xref-correct-lowercase/checks.check:2: 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) diff --git a/tests-system/xref-correct/output.smtlib b/tests-system/xref-correct/output.smtlib new file mode 100644 index 00000000..07ac9289 --- /dev/null +++ b/tests-system/xref-correct/output.smtlib @@ -0,0 +1,3 @@ +checks MyType { + ^^^^^^ xref-correct/checks.check:4: 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) diff --git a/tests-system/xref-expressions/output.smtlib b/tests-system/xref-expressions/output.smtlib new file mode 100644 index 00000000..72aa97d2 --- /dev/null +++ b/tests-system/xref-expressions/output.smtlib @@ -0,0 +1 @@ +Processed 1 model(s), 0 check(s) and 2 requirement file(s) and found no issues diff --git a/tests-system/xref-uniqueness-across-files/output.smtlib b/tests-system/xref-uniqueness-across-files/output.smtlib new file mode 100644 index 00000000..1db01541 --- /dev/null +++ b/tests-system/xref-uniqueness-across-files/output.smtlib @@ -0,0 +1,3 @@ +A.L L1 { + ^^ xref-uniqueness-across-files/f2.trlc:3: error: duplicate definition, previous definition at f1.trlc:4 +Processed 1 model(s), 0 check(s) and 2 requirement file(s) and found 1 error(s) diff --git a/tests-system/xref/output.smtlib b/tests-system/xref/output.smtlib new file mode 100644 index 00000000..df3a7510 --- /dev/null +++ b/tests-system/xref/output.smtlib @@ -0,0 +1,5 @@ +checks MyType { + ^^^^^^ xref/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature] +bar.MyType DeprecatedR { + ^^^^^^^^^^^ xref/instances.trlc:3: check error: Must be linked +Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/trlc/lint.py b/trlc/lint.py index 620ba599..39a9c5da 100644 --- a/trlc/lint.py +++ b/trlc/lint.py @@ -25,16 +25,18 @@ class Linter: # lobster-exclude: Not safety relevant - def __init__(self, mh, stab, verify_checks, debug_vcg): + def __init__(self, mh, stab, verify_checks, debug_vcg, cvc5_binary): assert isinstance(mh, Message_Handler) assert isinstance(stab, ast.Symbol_Table) assert isinstance(verify_checks, bool) assert isinstance(debug_vcg, bool) + assert isinstance(cvc5_binary, str) or cvc5_binary is None self.mh = mh self.stab = stab self.verify_checks = verify_checks self.debug_vcg = debug_vcg + self.cvc5_binary = cvc5_binary self.abstract_extensions = {} self.checked_types = set() @@ -134,7 +136,11 @@ def verify_tuple_type(self, n_tuple_type): # Verify checks if self.verify_checks: - vcg = VCG(self.mh, n_tuple_type, self.debug_vcg) + vcg = VCG(mh = self.mh, + n_ctyp = n_tuple_type, + debug = self.debug_vcg, + use_api = self.cvc5_binary is None, + cvc5_binary = self.cvc5_binary) vcg.analyze() def verify_record_type(self, n_record_type): @@ -155,7 +161,11 @@ def verify_record_type(self, n_record_type): # Verify checks if self.verify_checks: - vcg = VCG(self.mh, n_record_type, self.debug_vcg) + vcg = VCG(mh = self.mh, + n_ctyp = n_record_type, + debug = self.debug_vcg, + use_api = self.cvc5_binary is None, + cvc5_binary = self.cvc5_binary) vcg.analyze() def verify_array_type(self, n_typ): diff --git a/trlc/trlc.py b/trlc/trlc.py index eea3329c..699b5e91 100644 --- a/trlc/trlc.py +++ b/trlc/trlc.py @@ -23,6 +23,7 @@ import sys import json import argparse +import subprocess from fractions import Fraction from trlc import ast @@ -33,10 +34,10 @@ from trlc.version import TRLC_VERSION, BUGS_URL try: - from pyvcg import version - VCG_AVAILABLE = version.VERSION_TUPLE >= (1, 0, 4) + import cvc5 + VCG_API_AVAILABLE = True except ImportError: - VCG_AVAILABLE = False + VCG_API_AVAILABLE = False class Source_Manager: @@ -76,12 +77,14 @@ def __init__(self, mh, parse_trlc = True, verify_mode = False, debug_vcg = False, - error_recovery = True): + error_recovery = True, + cvc5_binary = None): assert isinstance(mh, Message_Handler) assert isinstance(lint_mode, bool) assert isinstance(parse_trlc, bool) assert isinstance(verify_mode, bool) assert isinstance(debug_vcg, bool) + assert isinstance(cvc5_binary, str) or cvc5_binary is None self.mh = mh self.mh.sm = self @@ -96,6 +99,7 @@ def __init__(self, mh, self.verify_mode = verify_mode self.debug_vcg = debug_vcg self.error_recovery = error_recovery + self.cvc5_binary = cvc5_binary self.exclude_patterns = [] self.common_root = None @@ -381,7 +385,8 @@ def perform_sanity_checks(self): linter = lint.Linter(mh = self.mh, stab = self.stab, verify_checks = self.verify_mode, - debug_vcg = self.debug_vcg) + debug_vcg = self.debug_vcg, + cvc5_binary = self.cvc5_binary) return linter.verify() def process(self): @@ -459,13 +464,18 @@ def main(): help=("Only process model and check files," " do not process trlc files.")) og_lint.add_argument("--verify", - default=False, - action="store_true", - help=("[EXPERIMENTAL] Attempt to statically" - " verify absence of errors in user defined" - " checks. Does not yet support all language" - " constructs. Requires PyVCG to be " - " installed.")) + default=False, + action="store_true", + help=("[EXPERIMENTAL] Attempt to statically" + " verify absence of errors in user defined" + " checks. Does not yet support all language" + " constructs. Requires PyVCG to be " + " installed.")) + og_lint.add_argument("--use-cvc5-binary", + default=None, + help=("[EXPERIMENTAL] Drive the given CVC5 solver" + " with SMTLIB2 input instead of using the" + " API.")) og_input = ap.add_argument_group("input options") og_input.add_argument("--include-bazel-dirs", @@ -531,8 +541,27 @@ def main(): metavar="DIR|FILE") options = ap.parse_args() - if options.verify and not VCG_AVAILABLE: - ap.error("The --verify option requires the optional dependency PyVCG") + if options.verify and not (options.use_cvc5_binary or + VCG_API_AVAILABLE): + ap.error("The --verify option requires the optional dependency" + " CVC5 or use of the --use-cvc5-binary option") + + if options.use_cvc5_binary: + if not options.verify: + ap.error("The --use-cvc5-binary requires the --verify option") + try: + result = subprocess.run([options.use_cvc5_binary, + "--version"], + check = True, + capture_output = True, + encoding = "UTF-8") + if not result.stdout.startswith("This is cvc5"): + ap.error("selected binary does not appear to be CVC5") + except OSError as err: + ap.error("cannot run %s: %s" % (options.use_cvc5_binary, + str(err))) + except subprocess.CalledProcessError: + ap.error("cannot run %s" % options.use_cvc5_binary) mh = Message_Handler(options.brief, not options.no_detailed_info) @@ -544,7 +573,8 @@ def main(): parse_trlc = not options.skip_trlc_files, verify_mode = options.verify, debug_vcg = options.debug_vcg, - error_recovery = not options.no_error_recovery) + error_recovery = not options.no_error_recovery, + cvc5_binary = options.use_cvc5_binary) if not options.include_bazel_dirs: sm.exclude_patterns.append(re.compile("^bazel-.*$")) diff --git a/trlc/vcg.py b/trlc/vcg.py index 5c2d654e..42f397ea 100644 --- a/trlc/vcg.py +++ b/trlc/vcg.py @@ -29,11 +29,17 @@ from pyvcg import graph from pyvcg import vcg from pyvcg.driver.file_smtlib import SMTLIB_Generator - from pyvcg.driver.cvc5_api import CVC5_Solver + from pyvcg.driver.cvc5_smtlib import CVC5_File_Solver VCG_AVAILABLE = True except ImportError: # pragma: no cover VCG_AVAILABLE = False +try: + from pyvcg.driver.cvc5_api import CVC5_Solver + CVC5_API_AVAILABLE = True +except ImportError: # pragma: no cover + CVC5_API_AVAILABLE = False + CVC5_OPTIONS = { "tlimit-per" : 2500, "seed" : 42, @@ -67,15 +73,19 @@ def __init__(self, node, message, kind, expect_unsat=True): class VCG: # lobster-exclude: Not safety relevant - def __init__(self, mh, n_ctyp, debug): + def __init__(self, mh, n_ctyp, debug, use_api=True, cvc5_binary=None): assert VCG_AVAILABLE assert isinstance(mh, Message_Handler) assert isinstance(n_ctyp, Composite_Type) assert isinstance(debug, bool) + assert isinstance(use_api, bool) + assert use_api or isinstance(cvc5_binary, str) - self.mh = mh - self.n_ctyp = n_ctyp - self.debug = debug + self.mh = mh + self.n_ctyp = n_ctyp + self.debug = debug + self.use_api = use_api + self.cvc5_bin = cvc5_binary self.vc_name = "trlc-%s-%s" % (n_ctyp.n_package.name, n_ctyp.name) @@ -363,9 +373,13 @@ def checks_on_composite_type(self, n_ctyp): vc["feedback"] in nok_validity_checks: continue - solver = CVC5_Solver() + if self.use_api: + solver = CVC5_Solver() + else: + solver = CVC5_File_Solver(self.cvc5_bin) for name, value in CVC5_OPTIONS.items(): - solver.solver.setOption(name, str(value)) + solver.set_solver_option(name, value) + status, values = vc["script"].solve_vc(solver) message = vc["feedback"].message