diffblue-cbmc/regression
Michael Tautschnig d7a91ad94c
Merge pull request #4015 from allredj/smt2_strings_tests
SMT2 strings tests
2019-02-01 08:29:36 +00:00
..
acceleration Remove blank lines from regression test specs 2017-04-07 15:20:11 +01:00
ansi-c Move regression tests of the C front-end to a suitable folder, again 2019-01-10 18:32:24 +00:00
array-refinement merge fixes 2017-04-03 16:57:59 +01:00
array-refinement-with-incr merge fixes 2017-04-03 16:57:59 +01:00
cbmc Fix test matching missing property description 2019-01-31 15:29:14 +00:00
cbmc-concurrency Skip phi assignment if one of the merged states has an uninitialised object 2018-12-19 17:03:06 +00:00
cbmc-cover Add constraints for bounded quantification 2019-01-30 11:14:23 +00:00
cbmc-cpp move to C++ tests from regression/cbmc to regression/cbmc-cpp 2018-09-19 15:45:21 +01:00
cbmc-from-CVS Process array_equal the same way as array_{replace,copy} 2018-02-23 07:03:37 +00:00
cbmc-incr merge fixes 2017-04-03 16:57:59 +01:00
cbmc-incr-oneloop Remove blank lines from regression test specs 2017-04-07 15:20:11 +01:00
cbmc-library When to_integer returns true, the result must not be used 2019-01-30 16:28:12 +00:00
cbmc-with-incr Generalize ID_malloc to ID_allocate with optional zero-init 2017-11-06 17:11:21 +00:00
contracts Fix test matching missing property description 2019-01-31 15:29:14 +00:00
cpp C++ bool is at least one byte wide 2018-10-29 17:04:26 +00:00
cpp-from-CVS second pass cpplint fixes in regression/cpp-from-CVS 2017-04-10 17:16:06 +01:00
cpp-linter Escape braces in regression test regexes 2018-09-17 11:39:49 +01:00
fault-localization Move implementation of failed-tests-printer.pl into test.pl 2017-11-02 12:18:15 +00:00
goto-analyzer Remove blank line from test.desc file 2019-01-04 11:07:59 +00:00
goto-analyzer-taint Move Java regression tests 2018-05-20 23:00:12 +01:00
goto-cc-cbmc cbmc test no longer uses --cover 2018-08-03 11:44:12 +01:00
goto-cc-goto-analyzer Convert returned numbers to the appropriate symbolic exit codes and correct a few cases. 2017-12-05 11:17:25 +00:00
goto-cl Include goto-cl regression tests in test sequence 2019-01-10 18:32:22 +00:00
goto-diff bump goto binary version 2018-08-10 18:12:18 +01:00
goto-gcc Move regression tests of the C front-end to a suitable folder, again 2019-01-10 18:32:24 +00:00
goto-harness Add goto-harness regression test 2019-01-25 18:55:41 +00:00
goto-instrument Do not sneak an ID_identifier entry into END_FUNCTION 2019-01-27 15:37:56 +00:00
goto-instrument-typedef Fix base_name of return' symbol to match its name 2019-01-28 15:07:57 +00:00
goto-instrument-wmm-core merge fixes 2017-04-03 16:57:59 +01:00
invariants switch representation of bit-vectors to hex 2018-11-05 13:25:27 +00:00
k-induction merge fixes 2017-04-03 16:57:59 +01:00
smt2_solver smt2 id_map: Do not use nil_typet to detect map insert 2019-01-27 16:01:22 +00:00
smt2_strings Add FUTURE tests for SMT2 string operations 2019-01-31 17:28:04 +00:00
strings Fix perl regular expressioons in regression test descriptions 2018-05-17 17:35:21 +01:00
systemc Name resolution may require further template instantiation 2018-07-07 13:30:50 +01:00
test-script Fix tests with missing EXIT or SIGNAL tests 2018-03-23 11:37:53 +00:00
.gitignore Adding simple regression for struct function 2017-03-10 15:46:08 +00:00
CMakeLists.txt Add smt2_strings test suite directory 2019-01-31 17:28:01 +00:00
Makefile Add smt2_strings test suite directory 2019-01-31 17:28:01 +00:00
goto-instrument-wmm-full.tgz moved goto-instrument-wmm-full tests into a tarball 2016-01-17 16:18:15 +00:00
test.pl Variable in test.desc file can be also separated by ':' 2019-01-22 15:50:26 +00:00