Merge

7 files changed, 32 insertions, 21 deletions

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>