Merge

13 files changed, 41 insertions, 30 deletions

diff --git a/Util/Emacs/boogie-mode.el b/Util/Emacs/boogie-mode.el
index 5b60dcab..5763d695 100644
--- a/Util/Emacs/boogie-mode.el
+++ b/Util/Emacs/boogie-mode.el
@@ -36,9 +36,9 @@
         )) . font-lock-builtin-face)

    `(,(boogie-regexp-opt '(

         "assert" "assume" "break" "call" "then" "else" "havoc" "if" "goto" "return" "while"

-        "old" "forall" "exists" "lambda" "cast"

+        "old" "forall" "exists" "lambda" "cast" "div" "mod"

         "false" "true")) . font-lock-keyword-face)

-   `(,(boogie-regexp-opt '("bool" "int"

+   `(,(boogie-regexp-opt '("bool" "int" "real"

                              "bv0" "bv1" "bv2" "bv3" "bv4" "bv5" "bv6" "bv7" "bv8" "bv9"

                              "bv10" "bv11" "bv12" "bv13" "bv14" "bv15" "bv16" "bv17" "bv18" "bv19"

                              "bv20" "bv21" "bv22" "bv23" "bv24" "bv25" "bv26" "bv27" "bv28" "bv29"

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 4f437d23..1ba6186b 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -40,7 +40,7 @@
    `(,(dafny-regexp-opt '(

         "assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "yield"

         "while" "print" "where"

-        "old" "forall" "exists" "new" "parallel" "in" "this" "fresh"

+        "old" "forall" "exists" "new" "parallel" "calc" "in" "this" "fresh"

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

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

    )

diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs
index 02d14b93..fd7c561d 100644
--- a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs
+++ b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs
@@ -23,17 +23,17 @@ namespace Demo
           "bv30", "bv31", "bv32",

           "bv64",

           "call", "complete", "const",

+          "div",

           "else", "ensures", "exists", "extends",

           "false", "forall", "free", "function",

           "goto",

           "havoc",

           "if", "implementation", "int", "invariant",

           "lambda",

-          "modifies",

+          "mod", "modifies",

           "old",

           "procedure",

-          "requires",

-          "return", "returns",

+          "real", "requires", "return", "returns",

           "then", "true", "type",

           "unique",

           "var",

@@ -181,7 +181,7 @@ namespace Demo
         identList.Rule = MakePlusRule(identList, comma, ident);

         NewStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LParen + expressionList.Q() + RParen;

         NewArrStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LBracket + expressionList.Q() + RBracket;

-        BinOp.Rule = ToTerm("+") | "-" | "*" | "/" | "%" | "^" | "&" | "|"

+        BinOp.Rule = ToTerm("+") | "-" | "*" | "div" | "mod" | "^" | "&" | "|"

                     | "&&" | "||" | "==" | "!=" | greater | less

                     | ">=" | "<=" | "is"

                     | "=" | "+=" | "-="

@@ -270,8 +270,7 @@ namespace Demo
           "modifies" |

           "old" |

           "procedure" |

-          "requires" |

-          "return" | "returns" |

+          "real" | "requires" | "return" | "returns" |

           "then" | "true" | "type" |

           "unique" |

           "var" |

@@ -322,7 +321,7 @@ namespace Demo
           ;

 

         typeDecl.Rule

-          = (ToTerm("int") | "bool" | ident)

+          = (ToTerm("int") | "bool" | "real" | ident)

           ;

 

         fieldDecl.Rule

@@ -376,7 +375,7 @@ namespace Demo
         #region 5. Operators precedence

         RegisterOperators(1, "<==>");

         RegisterOperators(2, "+", "-");

-        RegisterOperators(3, "*", "/", "%", "!!");

+        RegisterOperators(3, "*", "div", "mod", "!!");

         RegisterOperators(4, Associativity.Right, "^");

         RegisterOperators(5, "||");

         RegisterOperators(6, "&&");

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 9d6f0882..ac1b755c 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -29,7 +29,7 @@ namespace Demo
           "in", "forall", "exists",

           "seq", "set", "map", "multiset", "array", "array2", "array3",

           "match", "case",

-          "fresh", "old", "choose", "where"

+          "fresh", "old", "choose", "where", "calc"

           );

 

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

@@ -292,6 +292,7 @@ namespace Demo
           | "return"

           | "yield"

           | "parallel"

+          | "calc"

           | "print"

           | "returns"

           | "yields"

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension.sln b/Util/VS2010/DafnyExtension/DafnyExtension.sln
index e7391254..fd450cc8 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension.sln
+++ b/Util/VS2010/DafnyExtension/DafnyExtension.sln
@@ -1,6 +1,6 @@
 

-Microsoft Visual Studio Solution File, Format Version 11.00

-# Visual Studio 2010

+Microsoft Visual Studio Solution File, Format Version 12.00

+# Visual Studio 2012

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyExtension", "DafnyExtension\DafnyExtension.csproj", "{6E9A5E14-0763-471C-A129-80A879D9E7BA}"

 EndProject

 Global

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index 9f22b887..39829bb0 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -231,9 +231,6 @@ namespace DafnyLanguage
       if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) {

         if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) {

           Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);

-        } else if (Bpl.CommandLineOptions.Clo.Ai.AnySet) {

-          // run one of the old domains

-          Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

         } else {

           // use /infer:j as the default

           Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true;

@@ -258,11 +255,7 @@ namespace DafnyLanguage
 

       ConditionGeneration vcgen = null;

       try {

-        if (Bpl.CommandLineOptions.Clo.vcVariety == Bpl.CommandLineOptions.VCVariety.Doomed) {

-          vcgen = new DCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);

-        } else {

-          vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);

-        }

+        vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);

       } catch (Bpl.ProverException) {

         return PipelineOutcome.FatalError;

       }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
index 66370dec..2580c396 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
@@ -1,5 +1,6 @@
 <?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

+  <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

     <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

@@ -14,6 +15,12 @@
     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <FileAlignment>512</FileAlignment>

     <GeneratePkgDefFile>false</GeneratePkgDefFile>

+    <MinimumVisualStudioVersion>11.0</MinimumVisualStudioVersion>

+    <FileUpgradeFlags>

+    </FileUpgradeFlags>

+    <UpgradeBackupLocation>

+    </UpgradeBackupLocation>

+    <OldToolsVersion>4.0</OldToolsVersion>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

     <DebugSymbols>true</DebugSymbols>

@@ -158,8 +165,13 @@
   <ItemGroup>

     <WCFMetadata Include="Service References\" />

   </ItemGroup>

+  <PropertyGroup>

+    <VisualStudioVersion Condition="'$(VisualStudioVersion)' == ''">10.0</VisualStudioVersion>

+    <VSToolsPath Condition="'$(VSToolsPath)' == ''">$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion)</VSToolsPath>

+  </PropertyGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

-  <Import Project="$(MSBuildExtensionsPath)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" />

+  <Import Project="$(VSToolsPath)\VSSDK\Microsoft.VsSDK.targets" Condition="'$(VSToolsPath)' != ''" />

+  <Import Project="$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" Condition="false" />

   <PropertyGroup>

     <PostBuildEvent>cd</PostBuildEvent>

     <PostBuildEvent>

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 22388704..2f295429 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -227,10 +227,12 @@ namespace DafnyLanguage
                 #region keywords

                 case "allocated":

                 case "array":

+                case "as":

                 case "assert":

                 case "assume":

                 case "bool":

                 case "break":

+                case "calc":

                 case "case":

                 case "choose":

                 case "class":

@@ -249,7 +251,7 @@ namespace DafnyLanguage
                 case "function":

                 case "ghost":

                 case "if":

-                case "imports":

+                case "import":

                 case "in":

                 case "int":

                 case "invariant":

@@ -265,6 +267,7 @@ namespace DafnyLanguage
                 case "null":

                 case "object":

                 case "old":

+                case "opened":

                 case "parallel":

                 case "predicate":

                 case "print":

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
index d822fbfc..ef5c1cf5 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
@@ -10,6 +10,9 @@
       <VisualStudio Version="10.0">

         <Edition>Pro</Edition>

       </VisualStudio>

+      <VisualStudio Version="11.0">

+        <Edition>Pro</Edition>

+      </VisualStudio>

     </SupportedProducts>

     <SupportedFrameworkRuntimeEdition MinVersion="4.0" MaxVersion="4.0" />

   </Identifier>

diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty
index 45eb050d..e67c61f4 100644
--- a/Util/latex/boogie.sty
+++ b/Util/latex/boogie.sty
@@ -19,7 +19,7 @@
 \usepackage{listings}

 

 \lstdefinelanguage{boogie}{

-  morekeywords={type,finite,bool,int,ref,%

+  morekeywords={type,bool,int,real,%

       bv0,bv1,bv2,bv3,bv4,bv5,bv6,bv7,bv8,bv9,%

       bv10,bv11,bv12,bv13,bv14,bv15,bv16,bv17,bv18,bv19,%

       bv20,bv21,bv22,bv23,bv24,bv25,bv26,bv27,bv28,bv29,%

@@ -34,7 +34,7 @@
       procedure,implementation,

       requires,modifies,ensures,free,

       % expressions

-      false,true,null,old,then,

+      false,true,null,old,then,div,mod,

       % statements

       assert,assume,havoc,call,if,else,while,invariant,break,return,goto,

       },

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 88f9c2a2..879b90cb 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -15,7 +15,7 @@
       match,case,false,true,null,old,fresh,choose,this,

       % statements

       assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,

-      parallel,where

+      parallel,where,calc

       },

   literate=%

     {:}{$\colon$}1

diff --git a/Util/vim/syntax/boogie.vim b/Util/vim/syntax/boogie.vim
index 667a2b8c..6af66279 100644
--- a/Util/vim/syntax/boogie.vim
+++ b/Util/vim/syntax/boogie.vim
@@ -13,9 +13,9 @@ set cpo&vim
 
 
 " type
-syn keyword bplType			bool int
+syn keyword bplType			bool int real
 " repeat / condition / label
-syn keyword bplExpr			forall exists cast returns lambda
+syn keyword bplExpr			forall exists cast returns lambda div mod
 syn keyword bplStmt			goto return while call else if assert assume havoc then 
 syn keyword bplDecl			axiom function procedure type requires ensures modifies unique const var free implementation invariant
 " user labels
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index d67d275a..45afbcf0 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -10,7 +10,7 @@ syntax keyword dafnyTypeDef class datatype codatatype type iterator
 syntax keyword module import opened as default
 syntax keyword dafnyConditional if then else match case 
 syntax keyword dafnyRepeat while parallel
-syntax keyword dafnyStatement assume assert return yield new print break label where
+syntax keyword dafnyStatement assume assert return yield new print break label where calc
 syntax keyword dafnyKeyword var ghost returns yields null static this refines
 syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map
 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant