| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Remove a few other old test infrastructure files. They |  Dan Liew | 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 |  qadeer | 2013-12-07 |
| | | |||
| * | Added test cases for symdiff (z3multipleErrors flag) |  Unknown | 2013-07-30 |
| | | |||
| * | Added a feature for verifying several program snapshots (incl. result ↵ | wuestholz | 2013-06-02 |
| | | | | | caching and prioritization). | ||
| * | Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵ | Rustan Leino | 2013-03-05 |
| | | | | | Codeplex repositories. | ||
| * | Disengaged Dafny tests |  Rustan Leino | 2012-11-20 |
| | | |||
| * | Added Abstract Houdini: an implementation of Houdini based on abstract domains. |  Unknown | 2012-11-05 |
| | | | | | Currently only predicate-abstraction domain is supported. | ||
| * | include Test/datatypes |  Unknown | 2012-10-22 |
| | | |||
| * | removed lazy inlining |  qadeer | 2012-04-28 |
| | | |||
| * | Boogie: temporarily disabled the "datatypes" test cases, until a null ↵ | Unknown | 2012-03-12 |
| | | | | | dereference error in the Boogie code gets resolved | ||
| * | updated Boogie strings so that they can refer to \" (and more) | qadeer | 2012-03-12 |
| | | | | | fixed BCT :value | ||
| * | Disable datatypes test until Z3 is updated. |  Mike Barnett | 2012-01-05 |
| | | |||
| * | added a test for generalized array theory | qadeer | 2011-12-30 |
| | | |||
| * | added the datatypes test | qadeer | 2011-12-29 |
| | | |||
| * | Added Dafny solutions to the VSTTE 2012 program verification competition | Rustan Leino | 2011-11-15 |
| | | |||
| * | Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only) |  Unknown | 2011-10-19 |
| | | |||
| * | added houdini to regression | qadeer | 2011-10-17 |
| | | | | | changed houdini so that the initial worklist is created by queueing downstream Sccs first | ||
| * | Dafny: added Snapshotable Trees example | Rustan Leino | 2011-09-11 |
| | | |||
| * | Add tests for -z3multipleErrors from Shuvendu. | MichalMoskal | 2011-02-23 |
| | | |||
| * | Boogie: | rustanleino | 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 | akashlal | 2010-09-04 |
| | | |||
| * | Dafny: Added Dafny solutions to the VSComp 2010 problems | rustanleino | 2010-09-01 |
| | | |||
| * | Boogie: Added boolean code expressions (sans well-formedness checks on the ↵ | rustanleino | 2010-08-10 |
| | | | | | input). | ||
| * | Boogie: Added a new simple regression test, "sanity", which runs a single ↵ | tabarbe | 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 ↵ | akashlal | 2010-07-07 |
| | | | | | /stratifiedInline:1. | ||
| * | Boogie: | rustanleino | 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 | qadeer | 2010-05-28 |
| | | |||
| * | Dafny: | rustanleino | 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) | qadeer | 2010-02-12 |
| | | |||
| * | Start (some parsing and resolution) of adding algebraic datatypes to Dafny. | rustanleino | 2009-11-08 |
| | | | | | Included VSI-Benchmarks in standard tests. | ||
| * | Initial set of files. | mikebarnett | 2009-07-15 |
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |