summaryrefslogtreecommitdiff
path: root/Test
Commit message (Expand)AuthorAge
* Enable snapshot test. This test is unusual in that it doesn'tGravatar Dan Liew2014-05-07
* 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
* Added "STORM benchmarks for testing correctness of live variable analysis" li...Gravatar Dan Liew2014-05-07
* 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
* Enabled the inline lit tests. In order to support expansion2.bplGravatar Dan Liew2014-05-07
* 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
* 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
* 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
* Enabled lit tests for test1/ directoryGravatar Dan Liew2014-05-06
* Enabled most of the name resolution lit tests. They don't all passGravatar Dan Liew2014-05-05
* Converted textbook tests to lit tests.Gravatar Dan Liew2014-04-08
* Add lit.local.cfg that instructs not to run any tests in thisGravatar Dan Liew2014-05-05
* Pass -useBaseNameForFileName option to Boogie when running tests.Gravatar Dan Liew2014-04-06
* Enable houdini lit tests. Note some still fail due to BoogieGravatar Dan Liew2014-05-05
* Added basic lit configuration file for running tests.Gravatar Dan Liew2014-04-06
* minor fixGravatar qadeer2014-05-05
* example for variable introduction addedGravatar qadeer2014-05-04
* second checkpointGravatar qadeer2014-05-04
* checkpointGravatar qadeer2014-05-03
* updated the mover checksGravatar qadeer2014-04-25
* Add support for assumption variables.Gravatar wuestholz2014-04-21
* added another sampleGravatar qadeer2014-04-20
* added simulation relation computation to yield type checkingGravatar qadeer2014-04-20
* added the framing for the refinement checkGravatar qadeer2014-04-16
* MergeGravatar qadeer2014-04-16
|\
* | added variable hidingGravatar qadeer2014-04-16
| * disabled quantifier merging, except when no triggers are provided (as discuss...Gravatar Unknown2014-03-03
|/
* Fixed abstract interpretation for realsGravatar Rustan Leino2014-04-13
* Fixed bug in abstract interpretation over realsGravatar Rustan Leino2014-04-08
* Changed all lambda-expression rewriting to be done as a pre-processing step b...Gravatar Rustan Leino2014-02-28
* added ReadOnlyStandardVisitorGravatar qadeer2014-02-24
* fixed a bug in desugaring of linear variablesGravatar qadeer2014-02-20
* forgot to update the Answer file earlierGravatar qadeer2014-02-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 17:04:22 +0000