Dafny:

* Big change:  Add type and allocatedness information everywhere in the Boogie translation.  This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program.  On the downside, it also requires discharging more antecedents in order to use some axioms.  Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case).

* Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms).  (Internally, this uses the new canCall mechanism.)

* Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type.

* More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal")

* Add axioms about idempotence of set union and intersection

* The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one

* In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase

* Fixed error in translation of while(*)

5 files changed, 6 insertions, 4 deletions

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 82490ae7..cc3d6fb2 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -37,7 +37,7 @@
         )) . font-lock-builtin-face)

    `(,(dafny-regexp-opt '(

         "assert" "assume" "break" "call" "then" "else" "havoc" "if" "label" "return" "while" "print"

-        "old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use"

+        "old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "allocated" "use"

         "match" "case" "false" "true" "null")) . font-lock-keyword-face)

    `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "int" "object" "set" "seq")) . font-lock-type-face)

    )

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 48841c43..26d4f45a 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -27,7 +27,7 @@ namespace Demo
           "in", "forall", "exists",

           "seq", "set", "array", "array2", "array3",

           "match", "case",

-          "fresh", "old"

+          "fresh", "allocated", "old"

           );

 

         StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);

@@ -335,6 +335,7 @@ namespace Demo
           | "match"

           | "case"

           | "fresh"

+          | "allocated"

           | "old"

           | ident

           | "}"

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index a9254621..a4d67f0b 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -233,6 +233,7 @@ namespace DafnyLanguage
             } else {

               switch (s) {

                 #region keywords

+                case "allocated":

                 case "array":

                 case "assert":

                 case "assume":

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index e82ed0dc..11af30d4 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -11,7 +11,7 @@
       method,returns,module,imports,in,

       requires,modifies,ensures,reads,decreases,free,

       % expressions

-      match,case,false,true,null,old,fresh,this,

+      match,case,false,true,null,old,fresh,allocated,this,

       % statements

       assert,assume,print,new,havoc,call,if,then,else,while,invariant,break,label,return,foreach,

       },

diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index df2666c3..5c492a31 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -13,7 +13,7 @@ syntax keyword dafnyStatement havoc assume assert return call new print break la
 syntax keyword dafnyKeyword var ghost returns null static this refines replaces by
 syntax keyword dafnyType int bool seq set object array array2 array3
 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant 
-syntax keyword dafnyOperator forall exists old fresh
+syntax keyword dafnyOperator forall exists old fresh allocated
 syntax keyword dafnyBoolean true false
   
 syntax region dafnyString start=/"/ skip=/\\"/ end=/"/