Echtzeitsysteme/tchecker
1
0
Fork 0
mirror of https://github.com/Echtzeitsysteme/tchecker.git synced 2024-05-20 20:00:44 +00:00
Code Issues Packages Projects Releases Wiki Activity
tchecker/test
History
alzeha c195fdd53b
fixed multiple bugs (#6) 
fixed multiple bugs
2024-05-17 16:12:12 +02:00
..
algos Updated DBM output as expressions to conform to TChecker 2023-07-12 12:21:00 +02:00
bugfixes Improved memory management in declarations 2023-12-24 16:14:34 +01:00
covreach chg: start Gitlab CI configuration 2020-11-17 15:38:17 +01:00
explore chg: start Gitlab CI configuration 2020-11-17 15:38:17 +01:00
simple-nr Fixed test cases 2023-06-23 00:01:49 +02:00
tck-compare fixed multiple bugs (#6) 2024-05-17 16:12:12 +02:00
testutils Improved memory management in declarations 2023-12-24 16:14:34 +01:00
unit-tests Intermediate (#3) 2024-05-14 18:18:14 +02:00
CMakeLists.txt added first version of vcg 2024-05-14 18:18:14 +02:00
README.md new test suites 2019-10-25 11:20:19 +02:00
save-results.sh new test suites 2019-10-25 11:20:19 +02:00
tck-compare.sh added first version of vcg 2024-05-14 18:18:14 +02:00
tck-reach.sh Added memory max rss stat 2023-04-17 09:26:21 +02:00
test-driver.sh chg: memcheck tests fail if grep finds valgrind messages in error files 2021-07-20 13:35:09 +02:00
TestUtils.cmake Made commande line options rational 2023-03-20 16:36:34 +01:00

README.md

Test suites for TChecker project

Sub-directories contain specific test suites except testutils which contains a small library used to factorize some code between compiled tests. Each test suite can be disabled using a cmake option (see description below).

  • bugfixes contains non-regression test for reported bugs (see Issues tab on Github). This testsuite is disabled using the option -DTCK_ENABLE_BUGFIXES_TESTS=OFF.
  • covreach executes non-regression test on tchecker covreach; input tests come from the examples directory. This testsuite is disabled using the option -DTCK_ENABLE_COVREACH_TESTS=OFF.
  • explore executes non-regression test on tchecker explore; input tests come from the examples directory. This testsuite is disabled using the option -DTCK_ENABLE_EXPLORE_TESTS=OFF.
  • simple-nr contains more simple non-regression tests. This testsuite is disabled using the option -DTCK_ENABLE_SIMPLE_NR_TESTS=OFF.
  • unit-tests contains Catch2-based unit-tests for the native code. This testsuite is disabled using the option -DTCK_ENABLE_UNITTESTS=OFF.