blob: d68758254c89e2d63f8057924f95523f8828db72 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
Chalice Test Suite
==================
Contents
--------
- examples: Various examples how Chalice can be used to verify concurrent
programs. These tests represent (the core of) real problems and are therefore
well suited for performance and comparison tests (e.g. with other tools).
- general-tests: Regression tests for various aspects of Chalice.
- regressions: Regression tests for fixed bugs to ensure they do not occur
again.
- permission-model: Regression tests specifically for the permission model of
Chalice.
- refinements: Regression tests for the refinement extension.
- test-scripts: Some batch scripts that can be used to execute the tests in an
easy and automated way. More information below.
Test Scripts
------------
In the directory test-scripts are various scripts to allow the execution of the
tests in different ways. There are launchers in the test directories (e.g. in
examples or permission-model) to access them.
Commands (sorted by relevance):
- runalltests.bat: Executes all tests in all test folders.
- test.bat <file> [-params]: Execute a test and output the result of the
verification. Note: <file> must not include the file extension.
- reg_test.bat <file> [-params]: Execute a tests as a regression test, i.e., run
the test and compare the verification result with the reference output stored
in <file.output.txt>. Also shows the differences if any.
- reg_test_all.bat: Execute all tests as regression tests in the current
directory.
- generete_reference.bat <file> [-params]: Generate the reference output.
- generate_reference_all.bat: Generate reference files for all tests in the
current directory.
- getboogieoutput.bat: File used internally by generete_reference.bat.
To provide additional parameters to Chalice when verifying the tests (e.g., to
test the autoMagic feature, see tests/examples/RockBand-automagic.chalice), one
can start the Chalice source file with the line
"// chalice-parameter=<list of space-separated parameters>"
Note: For the refinement tests, there is a bash script test.sh.
|
