summaryrefslogtreecommitdiff
path: root/Test
Commit message (Expand)AuthorAge
* Dafny: don't allow ghost expressions in print statementsGravatar Rustan Leino2012-01-03
* added a test for generalized array theoryGravatar qadeer2011-12-30
* added the datatypes testGravatar qadeer2011-12-29
* fixed problems with datatypesGravatar qadeer2011-12-29
* Dafny: Fixed a bug in the pretty printer.Gravatar wuestholz2011-12-26
* Dafny: Extended the support for attributes on method/constructor calls.Gravatar wuestholz2011-12-23
* Dafny: Added support for attributes on method/constructor calls.Gravatar wuestholz2011-12-21
* forgot to check it inGravatar qadeer2011-12-21
* Dafny: for a datatype with just one constructor, don't check (but do assume) ...Gravatar Rustan Leino2011-12-19
* fixed a completeness problem in houdini with inliningGravatar qadeer2011-12-18
* Dafny: Made sure that error locations refer to the Dafny program, even if the...Gravatar wuestholz2011-12-15
* Dafny: Added support for attributes on various specification constructs (asse...Gravatar wuestholz2011-12-07
* Dafny: implemented thresholds for the new interval domain (/infer:j)Gravatar Rustan Leino2011-12-12
* Boogie: Changed Expr.Not to keep swap arguments rather change direction of op...Gravatar Rustan Leino2011-12-12
* Dafny: fix bug in translation of (the splitting of) if-then-else expressions ...Gravatar Rustan Leino2011-12-10
* MergeGravatar Rustan Leino2011-12-07
|\
* \ MergeGravatar Rustan Leino2011-12-07
|\ \
| * \ MergeGravatar Michal Moskal2011-12-07
| |\ \
| * | | Make it work with mingwGravatar Michal Moskal2011-12-07
| | * | Dafny: Added a separate script to run all Dafny tests.Gravatar wuestholz2011-12-07
* | | | MergeGravatar Rustan Leino2011-12-07
|\ \ \ \ | | |/ / | |/| |
| * | | Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable well...Gravatar wuestholz2011-12-07
* | | | Dafny tests: Disabled SnapshotableTrees.dfy for now while performance issues ...Gravatar Rustan Leino2011-12-07
* | | | MergeGravatar Rustan Leino2011-12-06
|\| | |
| * | | first check inGravatar qadeer2011-12-05
* | | | MergeGravatar Rustan Leino2011-12-05
|\| | |
* | | | Boogie: Added new abstract interpretation harness, which uses native Boogie E...Gravatar Rustan Leino2011-12-05
| * | | further fixes to houdiniGravatar qadeer2011-12-05
| |/ /
| * | Updated the 'Answer' file for test2.Gravatar wuestholz2011-12-02
| * | Boogie: Fixed a crash due to old expressions in lambda expressions that were ...Gravatar wuestholz2011-12-02
|/ /
* | added some more statistics to houdiniGravatar qadeer2011-11-24
* | fixed bug in the inlineDepth option for houdiniGravatar qadeer2011-11-23
| * MergeGravatar Rustan Leino2011-11-22
| |\ | |/ |/|
* | Dafny: call C# compiler directly from inside Dafny, and optionally produce a ...Gravatar Rustan Leino2011-11-22
| * Dafny: Added "type" declaration (syntax: "type X;"), which introduces an arbi...Gravatar Rustan Leino2011-11-21
* | changed the semantics of requires and ensures for inlined proceduresGravatar qadeer2011-11-17
|/
* /contractInfer always prints the computed assignment nowGravatar qadeer2011-11-16
* MergeGravatar Rustan Leino2011-11-15
|\
* | Added Dafny solutions to the VSTTE 2012 program verification competitionGravatar Rustan Leino2011-11-15
* | Dafny: added let expressions (syntax: "var x := E0; E1")Gravatar Rustan Leino2011-11-14
| * added the option /inlineDepth:n. This option defaults to -1. If the user prov...Gravatar qadeer2011-11-13
* | Dafny: implemented the wellformedness check that datatype destructors are onl...Gravatar Rustan Leino2011-11-11
|/
* Many, many bug fixes related to generics and some other random problems.Gravatar Mike Barnett2011-11-10
* Dafny: allow assert/assume expressions in more placesGravatar Rustan Leino2011-11-09
* Dafny: added assert/assume expressionsGravatar Rustan Leino2011-11-09
* Dafny: fixed part of a type-inference issue with datatypes and the < operator...Gravatar Rustan Leino2011-11-09
* Dafny: fixed bug in reads checking of array-to-sequence conversionsGravatar Rustan Leino2011-11-08
* Dafny: Cleaned up proof of RevConcat in test caseGravatar Rustan Leino2011-11-08
* Dafny: in test suite (Rippling.dfy), replaced an inline lemma with a call to ...Gravatar Rustan Leino2011-11-04
* Added some Dafny and Boogie test cases, including Turing's factorial program,...Gravatar Rustan Leino2011-11-03