summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension
Commit message (Collapse)AuthorAge
* Fixed range bug that was causing extension to sometimes crashGravatar Bryan Parno2014-10-27
|
* Ensure that no file is processed twice, even if one command-line file is ↵Gravatar Bryan Parno2014-10-27
| | | | included by another command-line file.
* MergeGravatar leino2014-10-20
|\
* | Added types "char" and "string" (the latter being a synonym for "seq<char>").Gravatar leino2014-10-20
| | | | | | | | | | | | Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings. Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions. Fixed lack of operator resolution in custom attributes.
| * DafnyExtension: Fixed minor issue in the menu.Gravatar wuestholz2014-10-19
|/
* MergeGravatar leino2014-09-29
|\
* | Shorter wait-for-idle time in the Dafny IDEGravatar leino2014-09-29
| |
| * DafnyExtension: Made it not log the pretty-printed program.Gravatar wuestholz2014-09-28
| |
| * DafnyExtension: minor change due to change in BoogieGravatar wuestholz2014-09-28
| |
| * Did more refactoring.Gravatar wuestholz2014-09-23
| |
| * Did more refactoring.Gravatar wuestholz2014-09-23
| |
| * DafnyExtension: minor changeGravatar wuestholz2014-09-22
|/
* Various resolution fixes and improvementsGravatar leino2014-08-26
| | | | | Added IsGoodHeap antecedent in (exists heap ...) in newtype Is axioms. Added IDE tool tips in newtype constraints.
* Changed syntax of derived types to "newtype"Gravatar leino2014-08-21
| | | | Added parsing of constraints (beyond parsing is yet to come)
* Forget the extra copy of DafnyRuntime.cs that gets copied into DafnyExtensionGravatar Rustan Leino2014-08-12
|
* MergeGravatar Dan Rosén2014-08-11
|\
* | Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter
| * MergeGravatar leino2014-08-02
| |\
| * | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in ↵Gravatar leino2014-08-02
|/ / | | | | | | the resolver and translator
| * added trait feature:Gravatar Reza Ahmadi2014-07-18
|/ | | | | | -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods
* Fixed build break from recent changeGravatar leino2014-07-15
|
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-09
|
* Build VS Extension for both VS 2012 and VS 2013.Gravatar Rustan Leino2014-07-08
| | | | Currently builds only in VS 2012. To build in VS 2013, change MinimumVisualStudioVersion from 11.0 to 12.0 in these two .csproj files.
* MergeGravatar Dan Rosén2014-07-07
|\
| * DafnyExtension: Worked on adding support for Visual Studio 2013.Gravatar wuestholz2014-07-02
| |
| * Dispose DafnyTokenTaggerGravatar Rustan Leino2014-07-01
| |
| * Color nested comments correctly in the Dafny IDEGravatar Rustan Leino2014-07-01
| |
| * Minor change due to change in BoogieGravatar wuestholz2014-06-28
| |
| * DafnyExtension: Made it possible to activate the more advanced verification ↵Gravatar wuestholz2014-06-23
| | | | | | | | result caching in Boogie (experimental for now).
* | DafnyExtension: Minor change to deal with a change in the Boogie ↵Gravatar wuestholz2014-06-20
| | | | | | | | command-line options
| * DafnyExtension: Minor change to deal with a change in the Boogie ↵Gravatar wuestholz2014-06-20
| | | | | | | | command-line options
* | Fixed issues with absolute file names in the expected output for the lit tests.Gravatar wuestholz2014-06-04
| |
| * Fixed issues with absolute file names in the expected output for the lit tests.Gravatar wuestholz2014-06-04
|/
* DafnyExtension: Made it display the compilation output in the VS output pane.Gravatar wuestholz2014-04-21
|
* DafnyExtension: Added some support for logging program snapshots that are ↵Gravatar wuestholz2014-04-21
| | | | sent to the verifier.
* Run-time real supportGravatar Rustan Leino2014-04-13
|
* Added "modify" statement.Gravatar Rustan Leino2014-04-03
| | | | In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
* DafnyExtension: Fixed a concurrency issue.Gravatar wuestholz2014-04-03
|
* Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss ↵Gravatar Rustan Leino2014-03-17
| | | | to VarDeclStmt.Locals
* Fixed build-break typoGravatar Rustan Leino2014-02-23
|
* Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵Gravatar Rustan Leino2014-02-23
| | | | -> "prefix lemma")
* Syntax highlighting for realsGravatar Rustan Leino2014-02-13
|
* Fixed bug in DafnyExtension (hover text computation would crash if ↵Gravatar Rustan Leino2014-02-06
| | | | | | Translator had not been run). Fixed duplicate hover text information for Lines of calc statements.
* Mark auto-generated expressions (in "decreases" clauses) and don't use these ↵Gravatar Rustan Leino2014-02-04
| | | | when figuring out hover text.
* Version 1.8.0.10115 release candidateGravatar Rustan Leino2014-01-15
|
* Manually adjusted mergeGravatar Rustan Leino2014-01-08
|
* One more file to go with the previous check-in (DafnyRuntime.cs apparently ↵Gravatar Rustan Leino2014-01-06
| | | | gets copied)
* DafnyExtension: Reduce the default number of Z3 instances by one.Gravatar wuestholz2013-12-26
|
* Compute default decreases clauses in Resolver instead of in the Translator.Gravatar Rustan Leino2013-12-19
| | | | Make this information available as AdditionalInformation, that is, as hover text in the IDE.