summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
* Convert the AbsHoudini tests to lit tests. They weren't being run by the oldGravatar Dan Liew2014-05-27
| | | | | | | | | | | | | | infrastructure so I have not bothered to update the Answer file. These tests are still disabled by the lit.local.cfg file in the AbsHoudini folder because the following tests fail or weren't even being run previously (these are left unresolved because I do not know how these tests are meant to be run) UNRESOLVED: Boogie :: AbsHoudini/f1.bpl (1 of 32) UNRESOLVED: Boogie :: AbsHoudini/imp1.bpl (7 of 32) UNRESOLVED: Boogie :: AbsHoudini/int1.bpl (8 of 32) UNRESOLVED: Boogie :: AbsHoudini/multi.bpl (9 of 32) FAIL: Boogie :: AbsHoudini/quant3.bpl (22 of 32) FAIL: Boogie :: AbsHoudini/quant5.bpl (28 of 32)
* Added simple python implementation of diff to replace using theGravatar Dan Liew2014-05-27
| | | | | ``fc`` tool on windows because it is buggy when tests are run concurrently.
* Implemented an additional type check for assumption variables.Gravatar wuestholz2014-05-27
|
* Added more tests (snapshots).Gravatar wuestholz2014-05-27
|
* Set the following tests to expected failure under lit. Having theseGravatar Dan Liew2014-05-19
| | | | | | | | | | | | | | | reported is unnecessary noise right now. Someone needs to fix these tests but I'm not the author. Boogie :: og/DeviceCacheSimplified.bpl Boogie :: og/DeviceCacheWithBuffer.bpl Boogie :: og/async.bpl Boogie :: og/houd1.bpl Boogie :: og/lock-introduced.bpl Boogie :: og/termination.bpl Boogie :: og/treiber-stack.bpl Boogie :: test21/Maps2.bpl Boogie :: test21/test3_AddMethod_conv.bpl
* Remove solver executable check under windows at the requestGravatar Dan Liew2014-05-12
| | | | | of Valentin Wüstholz because under Windows Boogie looks in other locations for Z3.
* Converted test0/Arrays1.bpl test to OutputCheck style test.Gravatar Dan Liew2014-05-12
|
* Convert houd12.bpl into a OutputCheck style test and also passGravatar Dan Liew2014-05-12
| | | | --dump-file-to-check flag to OutputCheck by default to ease debugging
* Added some documentation on the new testing infrastructureGravatar Dan Liew2014-05-11
|
* Remove old testing script. Probably not much use anyway, the executableGravatar Dan Liew2014-05-11
| | | | bit wasn't set on it.
* Added script for cleaning up temporary files created by both the litGravatar Dan Liew2014-05-11
| | | | | | | and legacy (batch file) testing infrastructures. This unfortunately is required if switching between infrastructures because both systems create a file named "Output". However for lit it is a directory and for the legacy system this is a simple text file.
* Prevent lit tests from running on OSX/Linux if mono is not inGravatar Dan Liew2014-05-11
| | | | the user's PATH
* Remove some legacy test infrastructure for OSX/LinuxGravatar Dan Liew2014-05-11
|
* Remove old python testing scriptsGravatar Dan Liew2014-05-11
|
* Made lit tests slightly less fragile under OSX/Linux by passing flags to ignoreGravatar Dan Liew2014-05-11
| | | | DOS line endings and whitespace to diff tool.
* Enable as many "og" lit tests. Several fail because they weren'tGravatar Dan Liew2014-05-11
| | | | | | | | | | | | being executed previously! Boogie :: og/DeviceCacheSimplified.bpl Boogie :: og/DeviceCacheWithBuffer.bpl Boogie :: og/async.bpl Boogie :: og/houd1.bpl Boogie :: og/lock-introduced.bpl Boogie :: og/termination.bpl Boogie :: og/treiber-stack.bpl
* Prevent running doomed tests. They weren't being runGravatar Dan Liew2014-05-10
| | | | by the old testing infrastructure.
* Remove old copy of lit. It's too old to work with our current configurationGravatar Dan Liew2014-05-10
|
* Unbreak the tests in test2 for batch file testing infrastructureGravatar Dan Liew2014-05-10
|
* Added a sanity check to lit configuration so tests won't runGravatar Dan Liew2014-05-10
| | | | if solver executables are missing.
* Enabled "linear type checking" lit tests.Gravatar Dan Liew2014-05-07
|
* Enabled symdiff lit test.Gravatar Dan Liew2014-05-07
|
* Enable snapshot test. This test is unusual in that it doesn'tGravatar Dan Liew2014-05-07
| | | | | | use .bpl files in the directory directy on the command line. So instead will tell lit to look for *.snapshot files and provide one that runs the commands we want in the right directory.
* Enabled "HAVOC-generated bpl files" lit tests.Gravatar Dan Liew2014-05-07
|
* Enabled "Extract loops benchmarks" lit tests.Gravatar Dan Liew2014-05-07
|
* Enabled the "Stratified inlining benchmarks" lit tests.Gravatar Dan Liew2014-05-07
| | | | | | | | | | The following tests will probably fail for newer versions of Z3 (e.g. 4.3) stratifiedinline/bar10.bpl stratifiedinline/bar7.bpl stratifiedinline/bar8.bpl stratifiedinline/bar9.bpl
* Added "STORM benchmarks for testing correctness of live variable analysis" ↵Gravatar Dan Liew2014-05-07
| | | | lit tests.
* Enabled generalizedarray lit test.Gravatar Dan Liew2014-05-07
|
* Enabled datatypes lit tests.Gravatar Dan Liew2014-05-07
|
* Enabled prover lit tests.Gravatar Dan Liew2014-05-07
|
* Enable codeexpr lit tests.Gravatar Dan Liew2014-05-07
|
* Enabled lit loop unrolling testGravatar Dan Liew2014-05-07
|
* Enabled smoke lit test.Gravatar Dan Liew2014-05-07
|
* Enabled bitvector lit tests.Gravatar Dan Liew2014-05-07
|
* Enabled "Benchmarks for error messages" lit tests.Gravatar Dan Liew2014-05-07
| | | | | | The test15/CaptureState.bpl test fails on Linux using (Z3 4.2) due to additional (but not meaningful) parentheses in the outputted model.
* Enabled the inline lit tests. In order to support expansion2.bplGravatar Dan Liew2014-05-07
| | | | | | we now require the OutputCheck tool. The lit.site.cfg file has been taught to require that this tool is in the user's PATH before testing starts.
* Enable "error messages for failing asserts vs. loop invariants" lit tests.Gravatar Dan Liew2014-05-07
|
* Enable "SLAM example" lit tests.Gravatar Dan Liew2014-05-07
|
* Enable "abstract domain of intervals" lit tests.Gravatar Dan Liew2014-05-07
|
* Enable Linear inequality lit tests.Gravatar Dan Liew2014-05-07
|
* For lit test infrastructure, disable running tests inGravatar Dan Liew2014-05-07
| | | | | | | | AbsHoudini/ test17/ z3api/ because the alltests.txt claims they are "Postponed"
* Enable the Constant propagation tests as lit tests.Gravatar Dan Liew2014-05-07
|
* Enabled "Verify Boogie 2" lit tests. Note the following tests failGravatar Dan Liew2014-05-07
| | | | | | | | because they were never properly tested in the the old testing infrastructure. test21/Maps2.bpl test21/test3_AddMethod_conv.bpl
* Enabled tests for types introduced in Boogie2 as lit tests.Gravatar Dan Liew2014-05-07
|
* Enable the VCVariety.BlockNested tests as lit tests.Gravatar Dan Liew2014-05-07
|
* Enabled VC Generation lit tests.Gravatar Dan Liew2014-05-07
|
* For lit tests running on Windows pass /W flag to the fc toolGravatar Dan Liew2014-05-06
| | | | | | | so that all whitespace (including mismatching line endings due to DOS vs UNIX) are ignored. This fixes the test1/Arrays.bpl test under Windows. It's quite suprising this issue didn't come up earlier.
* Enabled lit tests for test1/ directoryGravatar Dan Liew2014-05-06
| | | | Bizarely Array.bpl does not pass on Windows. This will be fixed soon.
* Enabled most of the name resolution lit tests. They don't all passGravatar Dan Liew2014-05-05
| | | | yet due to a bug in -useBaseNameForFileName.
* Converted textbook tests to lit tests.Gravatar Dan Liew2014-04-08
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 02:11:52 +0000