Merge

7 files changed, 25 insertions, 9 deletions

diff --git a/Util/Emacs/boogie-mode.el b/Util/Emacs/boogie-mode.el
index 5b60dcab..86721a74 100644
--- a/Util/Emacs/boogie-mode.el
+++ b/Util/Emacs/boogie-mode.el
@@ -36,7 +36,7 @@
         )) . 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"

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

diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs
index 02d14b93..4e38f654 100644
--- a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs
+++ b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs
@@ -23,13 +23,14 @@ 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",

@@ -181,7 +182,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"

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

@@ -376,7 +377,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/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/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/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..43336262 100644
--- a/Util/latex/boogie.sty
+++ b/Util/latex/boogie.sty
@@ -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/vim/syntax/boogie.vim b/Util/vim/syntax/boogie.vim
index 667a2b8c..673f967e 100644
--- a/Util/vim/syntax/boogie.vim
+++ b/Util/vim/syntax/boogie.vim
@@ -15,7 +15,7 @@ set cpo&vim
 " type
 syn keyword bplType			bool int
 " 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