summaryrefslogtreecommitdiff
path: root/Test
Commit message (Expand)AuthorAge
* Dafny: Added if-then-else expressions (replacing and extending the previous b...Gravatar rustanleino2010-02-04
* Fixed the implementation of inlining to deal with inlining depth properly.Gravatar qadeer2010-01-30
* Added experimental feature /DoomDebug. Can be test using Test/doomed/doomdebu...Gravatar schaef2010-01-28
* Dafny: updated to reflect Boogie's new parsing of function argumentsGravatar rustanleino2010-01-07
* Doomed checking now uses the counterexample trace to minimize the number of t...Gravatar schaef2009-12-18
* Allow ":" in addition to "returns" in function definitions. Make the pretty-p...Gravatar MichalMoskal2009-12-17
* Add makefile for running tests, allows "make -j4" to utilize multiple cores.Gravatar MichalMoskal2009-12-17
* Remove vcc1 testcase that never worked with Boogie2 and is testing obsolete b...Gravatar MichalMoskal2009-12-17
* * Added decreases clauses to functionsGravatar rustanleino2009-11-24
* Added resolution and translation of algebraic datatypes and (in function bodi...Gravatar rustanleino2009-11-20
* (no commit message)Gravatar schaef2009-11-20
* Fixed bug in inlining (procedure *definitions* had been traversed by Standard...Gravatar rustanleino2009-11-19
* doomed stuff: minor bug fixes / improved output / more test casesGravatar schaef2009-11-19
* modified the doom checking. It is now able to report only the relevant statem...Gravatar schaef2009-11-18
* Swapped previous file (Datatypes.bpl) for the correct test file (Datatypes.dfy).Gravatar rustanleino2009-11-14
* Start (some parsing and resolution) of adding algebraic datatypes to Dafny.Gravatar rustanleino2009-11-08
* Added a sequence update expression in Dafny.Gravatar rustanleino2009-11-06
* Redesigned the encoding of Dafny generics, including the built-in types set a...Gravatar rustanleino2009-11-06
* The Dafny call statement now automatically declares left-hand sides as local ...Gravatar rustanleino2009-11-05
* Introduced operator !in in Dafny. An expression "x !in S" is equivalent to "...Gravatar rustanleino2009-11-05
* Added loop invariants to make VSI-Benchmarks/b8.dfy verify. (Still to do: un...Gravatar rustanleino2009-11-04
* vc:doomed does not use the console anymore to report resultsGravatar schaef2009-11-02
* Initial version of VSI Benchmarks 1 - 8Gravatar RMonahan2009-10-30
* Fixed bugs in inlining, and added a test case.Gravatar rustanleino2009-10-14
* Fixed some bugs in the generation of bitvector input for Z3.Gravatar rustanleino2009-09-29
* Updated Answer files, in synch with my recent edits 31961.Gravatar rustanleino2009-08-16
* Removed Output files. These are created on a local machine when the tests ar...Gravatar rustanleino2009-08-07
* Fixed problem where nullary function with definition had caused a crash.Gravatar rustanleino2009-08-07
* Removed a temporary file that is created by the test script.Gravatar rustanleino2009-08-06
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 05:31:00 +0000