summaryrefslogtreecommitdiff
path: root/Test/dafny0/ResolutionErrors.dfy
Commit message (Expand)AuthorAge
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Fixed bug #32 dafny.codeplex.com.Gravatar Rustan Leino2014-04-15
* Changed an error from a verification error to a syntactic (resolution) errorGravatar Rustan Leino2014-04-04
* Added "modify" statement.Gravatar Rustan Leino2014-04-03
* Fixed problem with propagating allocation information about array elements.Gravatar Rustan Leino2014-03-20
* Added ghost let expressions.Gravatar Rustan Leino2014-01-05
* Allow calls to side-effect-free ghost methods from expressionsGravatar Rustan Leino2013-08-06
* Set up call-graph to keep track of edges between functions and methods. (To ...Gravatar Rustan Leino2013-08-04
* Introduced keywords "lemma" (like a "ghost method", but not allowed to have a...Gravatar Rustan Leino2013-08-02
* Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, ...Gravatar Rustan Leino2013-04-01
* Disallow allocations in ghost contextsGravatar Rustan Leino2013-03-06
* Added side-effects and control-flow checks in hints.Gravatar Nadia Polikarpova2013-03-05
* Report error if type of a quantified variable cannot be inferredGravatar Rustan Leino2013-02-11
* Translate let-such-that expressionsGravatar Rustan Leino2013-01-22
* fixed and improved scheme for inferring type parametersGravatar Rustan Leino2012-10-19
* improved and fixed compilation and resolution of assign-such-that statementsGravatar Rustan Leino2012-10-05
* Support default (which, here, means nameless) class-instance constructorsGravatar Rustan Leino2012-10-05
* Bugfix in the translation of calc statements (oops), added more resolution an...Gravatar Nadia Polikarpova2012-09-21
* Added tests for parsing and resolution of calc statementsGravatar Nadia Polikarpova2012-09-21
* Dafny: allow various forms of leaving off type arguments in declarationsGravatar Rustan Leino2012-02-16
* Dafny: don't allow ghost expressions in print statementsGravatar Rustan Leino2012-01-03
* Dafny: implemented the wellformedness check that datatype destructors are onl...Gravatar Rustan Leino2011-11-11
* Dafny: fix resolution crash (using multi-dimensional arrays in loop alternative)Gravatar Rustan Leino2011-08-03
* Dafny: added implicit datatype query fields and datatype destructor fieldsGravatar Rustan Leino2011-06-05
* Dafny: added constructorsGravatar Rustan Leino2011-05-28
* Dafny: added chaining operatorsGravatar Rustan Leino2011-05-27
* Dafny:Gravatar Rustan Leino2011-05-26
* Dafny: retired the "call" keywordGravatar Rustan Leino2011-05-26
* Dafny: allow class names to be used when referring to static functions (and, ...Gravatar Rustan Leino2011-05-21
* Cleaner version of ghost loop termination example.Gravatar Unknown2011-05-13
* Dafny: fixed bugs in resolution of multi-dimensional arraysGravatar Rustan Leino2011-05-12
* Dafny: forbid "decreases *" on ghost loopsGravatar Rustan Leino2011-05-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-19 10:32:29 +0000