Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Added a sanity check to lit configuration so tests won't run | Dan Liew | 2014-05-10 |
| | | | | if solver executables are missing. | ||
* | Enabled "linear type checking" lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | Enabled symdiff lit test. | Dan Liew | 2014-05-07 |
| | |||
* | Enable snapshot test. This test is unusual in that it doesn't | Dan Liew | 2014-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. | Dan Liew | 2014-05-07 |
| | |||
* | Enabled "Extract loops benchmarks" lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | Enabled the "Stratified inlining benchmarks" lit tests. | Dan Liew | 2014-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" ↵ | Dan Liew | 2014-05-07 |
| | | | | lit tests. | ||
* | Enabled generalizedarray lit test. | Dan Liew | 2014-05-07 |
| | |||
* | Enabled datatypes lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | Enabled prover lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | Enable codeexpr lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | Enabled lit loop unrolling test | Dan Liew | 2014-05-07 |
| | |||
* | Enabled smoke lit test. | Dan Liew | 2014-05-07 |
| | |||
* | Enabled bitvector lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | Enabled "Benchmarks for error messages" lit tests. | Dan Liew | 2014-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.bpl | Dan Liew | 2014-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. | Dan Liew | 2014-05-07 |
| | |||
* | Enable "SLAM example" lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | Enable "abstract domain of intervals" lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | Enable Linear inequality lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | For lit test infrastructure, disable running tests in | Dan Liew | 2014-05-07 |
| | | | | | | | | AbsHoudini/ test17/ z3api/ because the alltests.txt claims they are "Postponed" | ||
* | Enable the Constant propagation tests as lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | Enabled "Verify Boogie 2" lit tests. Note the following tests fail | Dan Liew | 2014-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. | Dan Liew | 2014-05-07 |
| | |||
* | Enable the VCVariety.BlockNested tests as lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | Enabled VC Generation lit tests. | Dan Liew | 2014-05-07 |
| | |||
* | For lit tests running on Windows pass /W flag to the fc tool | Dan Liew | 2014-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/ directory | Dan Liew | 2014-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 pass | Dan Liew | 2014-05-05 |
| | | | | yet due to a bug in -useBaseNameForFileName. | ||
* | Converted textbook tests to lit tests. | Dan Liew | 2014-04-08 |
| | |||
* | Add lit.local.cfg that instructs not to run any tests in this | Dan Liew | 2014-05-05 |
| | | | | | | | directory or its subdirectories. The test in this directory is pointless because we will run it later on anyway! When we migrate to lit this test directory should be removed | ||
* | Pass -useBaseNameForFileName option to Boogie when running tests. | Dan Liew | 2014-04-06 |
| | | | | | | | | | This is needed because the expected test output contains just the basename of the .bpl files in error messages but lit passes an absolute path to Boogie so without this option error messages would contain absolute paths which would cause the tests to fail. Now all the houdini tests pass when driven by lit. | ||
* | Enable houdini lit tests. Note some still fail due to Boogie | Dan Liew | 2014-05-05 |
| | | | | outputing absolute paths to .bpl files in error messages | ||
* | Added basic lit configuration file for running tests. | Dan Liew | 2014-04-06 |
| | |||
* | minor fix | qadeer | 2014-05-05 |
| | |||
* | example for variable introduction added | qadeer | 2014-05-04 |
| | |||
* | second checkpoint | qadeer | 2014-05-04 |
| | |||
* | checkpoint | qadeer | 2014-05-03 |
| | |||
* | updated the mover checks | qadeer | 2014-04-25 |
| | |||
* | Add support for assumption variables. | wuestholz | 2014-04-21 |
| | |||
* | added another sample | qadeer | 2014-04-20 |
| | |||
* | added simulation relation computation to yield type checking | qadeer | 2014-04-20 |
| | | | | updated the type check to incorporate {:terminates} annotation | ||
* | added the framing for the refinement check | qadeer | 2014-04-16 |
| | |||
* | Merge | qadeer | 2014-04-16 |
|\ | |||
* | | added variable hiding | qadeer | 2014-04-16 |
| | | | | | | | | added annotation on an atomic action about the phases in which it exists | ||
| * | disabled quantifier merging, except when no triggers are provided (as ↵ | Unknown | 2014-03-03 |
|/ | | | | discussed with Rustan) | ||
* | Fixed abstract interpretation for reals | Rustan Leino | 2014-04-13 |
| | |||
* | Fixed bug in abstract interpretation over reals | Rustan Leino | 2014-04-08 |
| | |||
* | Changed all lambda-expression rewriting to be done as a pre-processing step ↵ | Rustan Leino | 2014-02-28 |
| | | | | | | before real verification. Fixed treatment of lambda-expression attributes. |