Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Remove a few other old test infrastructure files. They | 2014-05-28 | |
| | | | | | probably aren't very useful anymore now that the old test infrastructure is gone. | ||
* | fixed a bug regarding invocation of modsetanalysis w.r.t. OG desugaring | 2013-12-07 | |
| | |||
* | Added test cases for symdiff (z3multipleErrors flag) | 2013-07-30 | |
| | |||
* | Added a feature for verifying several program snapshots (incl. result ↵ | 2013-06-02 | |
| | | | | caching and prioritization). | ||
* | Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵ | 2013-03-05 | |
| | | | | Codeplex repositories. | ||
* | Disengaged Dafny tests | 2012-11-20 | |
| | |||
* | Added Abstract Houdini: an implementation of Houdini based on abstract domains. | 2012-11-05 | |
| | | | | Currently only predicate-abstraction domain is supported. | ||
* | include Test/datatypes | 2012-10-22 | |
| | |||
* | removed lazy inlining | 2012-04-28 | |
| | |||
* | Boogie: temporarily disabled the "datatypes" test cases, until a null ↵ | 2012-03-12 | |
| | | | | dereference error in the Boogie code gets resolved | ||
* | updated Boogie strings so that they can refer to \" (and more) | 2012-03-12 | |
| | | | | fixed BCT :value | ||
* | Disable datatypes test until Z3 is updated. | 2012-01-05 | |
| | |||
* | added a test for generalized array theory | 2011-12-30 | |
| | |||
* | added the datatypes test | 2011-12-29 | |
| | |||
* | Added Dafny solutions to the VSTTE 2012 program verification competition | 2011-11-15 | |
| | |||
* | Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only) | 2011-10-19 | |
| | |||
* | added houdini to regression | 2011-10-17 | |
| | | | | changed houdini so that the initial worklist is created by queueing downstream Sccs first | ||
* | Dafny: added Snapshotable Trees example | 2011-09-11 | |
| | |||
* | Add tests for -z3multipleErrors from Shuvendu. | 2011-02-23 | |
| | |||
* | Boogie: | 2010-09-24 | |
| | | | | | * Added Test/textbook/DivMod.bpl, which embodies a conversion between C's div/mod operators and SMT Lib's div/mod operators. * Added a rudimentary printing of variables for captured states. It doesn't attempt to print everything at this time, and it doesn't work when variables get unique-ified by @@-suffixes. A more complete implementation will be added at a later time. | ||
* | Added tests for extractloops | 2010-09-04 | |
| | |||
* | Dafny: Added Dafny solutions to the VSComp 2010 problems | 2010-09-01 | |
| | |||
* | Boogie: Added boolean code expressions (sans well-formedness checks on the ↵ | 2010-08-10 | |
| | | | | input). | ||
* | Boogie: Added a new simple regression test, "sanity", which runs a single ↵ | 2010-07-29 | |
| | | | | test for Boogie and a single test for Dafny, just to check for grievous runtime errors in the code. (In my porting, I work with code that, in some cases, is not tested until the 3rd or 4th regression test. These 2 test files should make use of that more obscure code and alert me to my errors quickly, rather than making me wait through a full regression cycle.) | ||
* | Boogie: Added stratified inlining. It is enabled using the flag ↵ | 2010-07-07 | |
| | | | | /stratifiedInline:1. | ||
* | Boogie: | 2010-06-08 | |
| | | | | | | | | | * Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it). * Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it). Dafny: * Split off some tests from Test/dafny0 into Test/dafny1. * Added Test/dafny1/UltraFilter.dfy. | ||
* | added lazyinline to the regressions | 2010-05-28 | |
| | |||
* | Dafny: | 2010-05-21 | |
| | | | | | | | * Added arrays * Beefed up set axiomatization to know more things about set displays * Added a simple heuristic that can infer some simple decreases clauses for loops * Added Dafny solutions to a couple of VACID benchmarks | ||
* | (no commit message) | 2010-02-12 | |
| | |||
* | Start (some parsing and resolution) of adding algebraic datatypes to Dafny. | 2009-11-08 | |
| | | | | Included VSI-Benchmarks in standard tests. | ||
* | Initial set of files. | 2009-07-15 | |