summaryrefslogtreecommitdiff
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)
* MergeGravatar Dan Liew2014-05-27
|\
* | 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.
| * MergeGravatar Ally Donaldson2014-05-27
| |\ | |/ |/|
| * Undid accidental commitGravatar Ally Donaldson2014-05-27
| |
* | Implemented an additional type check for assumption variables.Gravatar wuestholz2014-05-27
| |
* | Added more tests (snapshots).Gravatar wuestholz2014-05-27
| |
| * MergeGravatar Ally Donaldson2014-05-27
| |
| * Added key check to uniformity analysisGravatar Ally Donaldson2014-05-27
|/
* Merge duality changesGravatar Ken McMillan2014-05-26
|\
| * Conjecture printing for duality and child user time tracking.Gravatar Ken McMillan2014-05-26
| |
* | 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
* | Made the Boogie driver return an exit code.Gravatar wuestholz2014-05-19
| |
* | keep some stats for debuggingGravatar akashlal2014-05-15
| |
* | Delete '_admin' directory.Gravatar wuestholz2014-05-13
| |
* | Simplify Z3 executable discovery.Gravatar wuestholz2014-05-12
| |
* | 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.
* | Added stack boundingGravatar akashlal2014-05-10
| |
* | 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
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 05:30:49 +0000