Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Changed "dummy" checksums to "stable" and added more tests for the ↵ | wuestholz | 2014-07-03 |
| | | | | verification result caching. | ||
* | Added support for verifying Dafny program snapshots from the command-line. | wuestholz | 2014-07-01 |
| | |||
* | Added tuples and tuple types. Syntax is the expected one, namely parentheses ↵ | Rustan Leino | 2014-06-27 |
| | | | | around a comma-delimited list of expressions or types. Unit and the unit type are denoted (). | ||
* | Make syntax of "match" expressions and "match" statements the same -- curly ↵ | Rustan Leino | 2014-06-24 |
| | | | | braces around the cases are now supported for both and are optional for both | ||
* | Invert LHS sub-expressions in forall assignment statements, which gives the ↵ | Rustan Leino | 2014-06-24 |
| | | | | opportunity to designate a good trigger. | ||
* | Specialized Lit function for int and real (leaving all other cases ↵ | Rustan Leino | 2014-06-10 |
| | | | | | | polymorphic). This reduces the number of int<->U conversions that Boogie adds, which avoids a looping problem in Z3. (Regrettably, the test suite seems to have become rather unstable. Sometimes everything verifies and sometimes there is some looping forever.) | ||
* | Fixed issues with absolute file names in the expected output for the lit tests. | wuestholz | 2014-06-04 |
| | |||
* | Added support for 'dirty' forall statements. | chmaria | 2014-06-03 |
| | | | | | | | | | | | One can now write forall statements without bodies (but with ensures clauses) as follows: forall s | s in S ensures s < 0; where S is set<int>. The ensures clauses are assumed but not checked. | ||
* | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
| | |||
* | Fixed bug in resolution, where type proxies involved in equality tests did ↵ | Rustan Leino | 2014-05-07 |
| | | | | | | not get assigned. (Issue #35) Fixed Main detection--a method "Main" with type parameters cannot be a program entry point. | ||
* | Fixed some bugs where various attributes were not properly visited during ↵ | Rustan Leino | 2014-05-05 |
| | | | | type checking. | ||
* | DafnyExtension: Made it display the compilation output in the VS output pane. | wuestholz | 2014-04-21 |
| | |||
* | Add support for assumption variables. | wuestholz | 2014-04-21 |
| | |||
* | Fixed bug #33. | Rustan Leino | 2014-04-19 |
| | |||
* | Members included from different files are now internally marked with an ↵ | Rustan Leino | 2014-04-19 |
| | | | | | | | IncludeToken; the previous scheme of using {:verify false} is no longer used. This makes "include" work with refinement features. Filenames of included files used in error messages are now what the user wrote, rather than absolute paths (which not only don't look so good, but are also problematic in comparing test output on different machines). Added dafny0/Includee.dfy to the test suite as well -- might as well include it, too, to get checked. | ||
* | Fixed bug #32 dafny.codeplex.com. | Rustan Leino | 2014-04-15 |
| | |||
* | Compile reals | Rustan Leino | 2014-04-13 |
| | |||
* | Allow reals in decreases clauses | Rustan Leino | 2014-04-08 |
| | |||
* | Merge | Rustan Leino | 2014-04-04 |
|\ | |||
* | | Fixed refinement of modify statements | Rustan Leino | 2014-04-04 |
| | | |||
| * | Partial support for slicing a sequence using lengths, rather than indices. | Bryan Parno | 2014-04-04 |
|/ | | | | Will get cleaner once we have tuple support. | ||
* | Merge | Rustan Leino | 2014-04-04 |
|\ | |||
* | | Also include lower set bounds (bounding a set from below) in witness guesses ↵ | Rustan Leino | 2014-04-04 |
| | | | | | | | | for assign/let such-that. | ||
* | | Support the transition from "modify Frame;" to "modify Frame { Body }" by ↵ | Rustan Leino | 2014-04-04 |
| | | | | | | | | refinement. | ||
* | | Changed an error from a verification error to a syntactic (resolution) error | Rustan Leino | 2014-04-04 |
| | | |||
* | | Added "modify Frame { Body }" statement. | Rustan Leino | 2014-04-04 |
| | | |||
* | | Added "modify" statement. | Rustan Leino | 2014-04-03 |
| | | | | | | | | In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field. | ||
| * | Basic support for datatype-update syntatic sugar | Bryan Parno | 2014-04-03 |
|/ | |||
* | Merge | Rustan Leino | 2014-03-24 |
|\ | |||
* | | Reduced noise in BVD display of temporary variables of the translation | Rustan Leino | 2014-03-24 |
| | | |||
| * | Auto-set type arguments of built-in collection types, just like for ↵ | Rustan Leino | 2014-03-21 |
|/ | | | | user-defined types. | ||
* | Fixed problem with propagating allocation information about array elements. | Rustan Leino | 2014-03-20 |
| | | | | Improved situation with (reducing bogosity of) type checking of "object". | ||
* | Propagate literals through equality operations. | Nada Amin | 2014-03-19 |
| | |||
* | Merge | Rustan Leino | 2014-03-17 |
|\ | |||
* | | Fixed resolution bug where "var x := x" was allowed. | Rustan Leino | 2014-03-17 |
| | | |||
* | | Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss ↵ | Rustan Leino | 2014-03-17 |
| | | | | | | | | to VarDeclStmt.Locals | ||
* | | AST refactoring: | Rustan Leino | 2014-03-17 |
| | | | | | | | | | | Changed VarDecl to no longer inherit from Statement. Removed ConcreteSyntaxStatement and changed VarDeclStmt's superclass be Statement. | ||
| * | Improve computations, in particular compositionality. Isolated useless ↵ | Nada Amin | 2014-03-12 |
| | | | | | | | | literals around if-then-else as a surprising source of practical hanging. | ||
| * | change computation weight to 3. Tests still pass. | Nada Amin | 2014-03-11 |
|/ | |||
* | Added further assistance in coming up with decreases clauses in SCCs with ↵ | Rustan Leino | 2014-02-24 |
| | | | | co-recursive calls. | ||
* | Unfinished code -- please forgive (I'm switching machines and will fix shortly) | Rustan Leino | 2014-02-24 |
| | |||
* | Refactored code for dealing with SCCs in the call graph. | Rustan Leino | 2014-02-24 |
| | | | | Fixed bug. | ||
* | Fixed bugs in co-call checks | Rustan Leino | 2014-02-23 |
| | |||
* | Fixed some checking of recursive method/copredicate calls | Rustan Leino | 2014-02-23 |
| | |||
* | Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵ | Rustan Leino | 2014-02-23 |
| | | | | -> "prefix lemma") | ||
* | Allow unary minus on reals | Rustan Leino | 2014-02-13 |
| | |||
* | Fixed crash in parser | Rustan Leino | 2014-02-13 |
| | |||
* | Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for ↵ | Rustan Leino | 2014-02-13 |
| | | | | | | literals. Added axiom to better handle DtAlloc/GenericAlloc correspondence (which improves handling of computations). | ||
* | Preliminary support for reals in Dafny specs. No compiler suport yet. | Bryan Parno | 2014-02-10 |
| | |||
* | Fixed bug in DafnyExtension (hover text computation would crash if ↵ | Rustan Leino | 2014-02-06 |
| | | | | | | Translator had not been run). Fixed duplicate hover text information for Lines of calc statements. |