From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Util/BoogieBuildAndTest.cmd | 52 +- Util/Code Snippets/contractassertnonnull.snippet | 62 +- .../contractassertnonnullelem.snippet | 62 +- .../contractensuresnonnullelem.snippet | 60 +- Util/Code Snippets/contractensuresvalret.snippet | 60 +- .../contractensuresvalretNonNullElem.snippet | 60 +- Util/Code Snippets/contractinvnonnullelem.snippet | 62 +- .../contractrequiresnonnullelem.snippet | 62 +- Util/Emacs/boogie-mode.el | 240 +++---- Util/VS2010/Boogie/BoogieLanguageService.sln | 40 +- .../BoogieLanguageService.csproj | 356 ++++----- .../Boogie/BoogieLanguageService/Configuration.cs | 48 +- .../BoogieLanguageService/GlobalSuppressions.cs | 22 +- .../VS2010/Boogie/BoogieLanguageService/Grammar.cs | 794 ++++++++++----------- Util/VS2010/Boogie/BoogieLanguageService/Guids.cs | 24 +- .../Integration/AuthoringScope.cs | 130 ++-- .../Integration/Configuration.cs | 230 +++--- .../Integration/Declaration.cs | 58 +- .../Integration/Declarations.cs | 110 +-- .../Integration/IASTResolver.cs | 24 +- .../Integration/IronyLanguageService.cs | 686 +++++++++--------- .../Integration/IronyViewFilter.cs | 84 +-- .../Integration/LineScanner.cs | 116 +-- .../BoogieLanguageService/Integration/Method.cs | 38 +- .../BoogieLanguageService/Integration/Methods.cs | 98 +-- .../BoogieLanguageService/Integration/Package.cs | 258 +++---- .../BoogieLanguageService/Integration/Resolver.cs | 100 +-- .../BoogieLanguageService/Integration/Source.cs | 80 +-- .../IronyLanguageServicePackage.cs | 180 ++--- .../Properties/AssemblyInfo.cs | 72 +- .../BoogieLanguageService/Resources.Designer.cs | 126 ++-- .../Boogie/BoogieLanguageService/Resources.resx | 258 +++---- .../Boogie/BoogieLanguageService/VSPackage.resx | 256 +++---- .../source.extension.vsixmanifest | 54 +- Util/latex/boogie.sty | 242 +++---- 35 files changed, 2602 insertions(+), 2602 deletions(-) (limited to 'Util') diff --git a/Util/BoogieBuildAndTest.cmd b/Util/BoogieBuildAndTest.cmd index 08d5baeb..acaa8053 100644 --- a/Util/BoogieBuildAndTest.cmd +++ b/Util/BoogieBuildAndTest.cmd @@ -1,27 +1,27 @@ -@echo off -pushd ..\test -goto Cleanandbuild - -:Cleanandbuild -cls -@echo on -devenv ..\Source\Boogie.sln /Clean -@echo off -if errorlevel 1 goto fail -@echo on -devenv ..\source\Boogie.sln /Build -@echo off -if errorlevel 1 goto fail -goto reg - -:Reg -cls -call runtestall -goto end - -:fail -echo Some part of the rebuild failed. -goto end - -:end +@echo off +pushd ..\test +goto Cleanandbuild + +:Cleanandbuild +cls +@echo on +devenv ..\Source\Boogie.sln /Clean +@echo off +if errorlevel 1 goto fail +@echo on +devenv ..\source\Boogie.sln /Build +@echo off +if errorlevel 1 goto fail +goto reg + +:Reg +cls +call runtestall +goto end + +:fail +echo Some part of the rebuild failed. +goto end + +:end popd \ No newline at end of file diff --git a/Util/Code Snippets/contractassertnonnull.snippet b/Util/Code Snippets/contractassertnonnull.snippet index 4979600a..298cb164 100644 --- a/Util/Code Snippets/contractassertnonnull.snippet +++ b/Util/Code Snippets/contractassertnonnull.snippet @@ -1,31 +1,31 @@ - - - -
- - Expansion - - Contract.Assert(...!=null) - can - Emits a 'Contract.Assert' non-null clause - tabarbe -
- - - - System.Diagnostics.Contracts - - - - - condition - condition that must not be null - arg - - - - - - - - + + + +
+ + Expansion + + Contract.Assert(...!=null) + can + Emits a 'Contract.Assert' non-null clause + tabarbe +
+ + + + System.Diagnostics.Contracts + + + + + condition + condition that must not be null + arg + + + + + + + + diff --git a/Util/Code Snippets/contractassertnonnullelem.snippet b/Util/Code Snippets/contractassertnonnullelem.snippet index 86273d71..34c20a00 100644 --- a/Util/Code Snippets/contractassertnonnullelem.snippet +++ b/Util/Code Snippets/contractassertnonnullelem.snippet @@ -1,31 +1,31 @@ - - - -
- - Expansion - - Contract.Assert(cce.NonNullElements(...)) - cann - Emits a 'Contract.Assert' non-null elements clause - tabarbe -
- - - - System.Diagnostics.Contracts - - - - - collection - collection whose elements must not be null - arg - - - - - - - - + + + +
+ + Expansion + + Contract.Assert(cce.NonNullElements(...)) + cann + Emits a 'Contract.Assert' non-null elements clause + tabarbe +
+ + + + System.Diagnostics.Contracts + + + + + collection + collection whose elements must not be null + arg + + + + + + + + diff --git a/Util/Code Snippets/contractensuresnonnullelem.snippet b/Util/Code Snippets/contractensuresnonnullelem.snippet index fabd9d1a..9d462275 100644 --- a/Util/Code Snippets/contractensuresnonnullelem.snippet +++ b/Util/Code Snippets/contractensuresnonnullelem.snippet @@ -1,31 +1,31 @@ - - - -
- - Expansion - - Contract.Ensures(cce.NonNullElements(Contract.Result<...>())) - cenn - Emits a 'Contract.Ensures' non-null elements clause - tabarbe -
- - - - System.Diagnostics.Contracts - - - - - collection - Collection whose elements must not be null - List<string> - - - - - ()));$end$]]> - - + + + +
+ + Expansion + + Contract.Ensures(cce.NonNullElements(Contract.Result<...>())) + cenn + Emits a 'Contract.Ensures' non-null elements clause + tabarbe +
+ + + + System.Diagnostics.Contracts + + + + + collection + Collection whose elements must not be null + List<string> + + + + + ()));$end$]]> + + \ No newline at end of file diff --git a/Util/Code Snippets/contractensuresvalret.snippet b/Util/Code Snippets/contractensuresvalret.snippet index b46be4fc..0be87286 100644 --- a/Util/Code Snippets/contractensuresvalret.snippet +++ b/Util/Code Snippets/contractensuresvalret.snippet @@ -1,31 +1,31 @@ - - - -
- - Expansion - - Contract.Ensures(Contract.ValueAtReturn(...)!=null) - cern - Emits a 'Contract.Ensures' non-null out or ref parameter clause - tabarbe -
- - - - System.Diagnostics.Contracts - - - - - value - Value that must not be null - arg - - - - - - - + + + +
+ + Expansion + + Contract.Ensures(Contract.ValueAtReturn(...)!=null) + cern + Emits a 'Contract.Ensures' non-null out or ref parameter clause + tabarbe +
+ + + + System.Diagnostics.Contracts + + + + + value + Value that must not be null + arg + + + + + + + \ No newline at end of file diff --git a/Util/Code Snippets/contractensuresvalretNonNullElem.snippet b/Util/Code Snippets/contractensuresvalretNonNullElem.snippet index c5915f44..195e9b68 100644 --- a/Util/Code Snippets/contractensuresvalretNonNullElem.snippet +++ b/Util/Code Snippets/contractensuresvalretNonNullElem.snippet @@ -1,31 +1,31 @@ - - - -
- - Expansion - - Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(...))) - cernn - Emits a 'Contract.Ensures' cce.non-nullelements out parameter clause - tabarbe -
- - - - System.Diagnostics.Contracts - - - - - value - Value that must not be null - arg - - - - - - - + + + +
+ + Expansion + + Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(...))) + cernn + Emits a 'Contract.Ensures' cce.non-nullelements out parameter clause + tabarbe +
+ + + + System.Diagnostics.Contracts + + + + + value + Value that must not be null + arg + + + + + + + \ No newline at end of file diff --git a/Util/Code Snippets/contractinvnonnullelem.snippet b/Util/Code Snippets/contractinvnonnullelem.snippet index cd0ff1c6..e665411c 100644 --- a/Util/Code Snippets/contractinvnonnullelem.snippet +++ b/Util/Code Snippets/contractinvnonnullelem.snippet @@ -1,31 +1,31 @@ - - - -
- - Expansion - - Contract.Invariant(cce.NonNullElements(...)) - cinn - Emits a 'Contract.Invariant' non-null elements clause - tabarbe -
- - - - System.Diagnostics.Contracts - - - - - collection - collection whose elements must not be null - arg - - - - - - - - + + + +
+ + Expansion + + Contract.Invariant(cce.NonNullElements(...)) + cinn + Emits a 'Contract.Invariant' non-null elements clause + tabarbe +
+ + + + System.Diagnostics.Contracts + + + + + collection + collection whose elements must not be null + arg + + + + + + + + diff --git a/Util/Code Snippets/contractrequiresnonnullelem.snippet b/Util/Code Snippets/contractrequiresnonnullelem.snippet index eb07bc66..bd550cae 100644 --- a/Util/Code Snippets/contractrequiresnonnullelem.snippet +++ b/Util/Code Snippets/contractrequiresnonnullelem.snippet @@ -1,31 +1,31 @@ - - - -
- - Expansion - - Contract.Requires(cce.NonNullElements(...)) - crnn - Emits a 'Contract.Requires' non-null elements clause - tabarbe -
- - - - System.Diagnostics.Contracts - - - - - collection - collection whose elements must not be null - arg - - - - - - - - + + + +
+ + Expansion + + Contract.Requires(cce.NonNullElements(...)) + crnn + Emits a 'Contract.Requires' non-null elements clause + tabarbe +
+ + + + System.Diagnostics.Contracts + + + + + collection + collection whose elements must not be null + arg + + + + + + + + diff --git a/Util/Emacs/boogie-mode.el b/Util/Emacs/boogie-mode.el index 5763d695..39d1ef5d 100644 --- a/Util/Emacs/boogie-mode.el +++ b/Util/Emacs/boogie-mode.el @@ -1,120 +1,120 @@ -;; boogie-mode.el - GNU Emacs mode for Boogie 2 -;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why - -(defvar boogie-mode-hook nil) - -(defvar boogie-mode-map nil - "Keymap for Boogie major mode") - -(if boogie-mode-map nil - (setq boogie-mode-map (make-keymap)) - (define-key boogie-mode-map "\C-c\C-c" 'boogie-run-boogie) - (define-key boogie-mode-map [(control return)] 'font-lock-fontify-buffer)) - -(setq auto-mode-alist - (append - '(("\\.bpl" . boogie-mode)) - auto-mode-alist)) - -;; font-lock - -(defun boogie-regexp-opt (l) - (concat "\\<" (concat (regexp-opt l t) "\\>"))) - -(defconst boogie-font-lock-keywords-1 - (list - ; comments have the form /* ... */ - '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face) - ; or // ... - '("//\\([^ -]\\)*" . font-lock-comment-face) - - `(,(boogie-regexp-opt '( - "type" "const" "function" "axiom" "var" "procedure" "implementation" - "returns" "where" "requires" "ensures" "modifies" "free" "unique" - "invariant" "extends" "complete" - )) . font-lock-builtin-face) - `(,(boogie-regexp-opt '( - "assert" "assume" "break" "call" "then" "else" "havoc" "if" "goto" "return" "while" - "old" "forall" "exists" "lambda" "cast" "div" "mod" - "false" "true")) . font-lock-keyword-face) - `(,(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" - "bv30" "bv31" "bv32" "bv33" "bv34" "bv35" "bv36" "bv37" "bv38" "bv39" - "bv40" "bv41" "bv42" "bv43" "bv44" "bv45" "bv46" "bv47" "bv48" "bv49" - "bv50" "bv51" "bv52" "bv53" "bv54" "bv55" "bv56" "bv57" "bv58" "bv59" - "bv60" "bv61" "bv62" "bv63" "bv64" ; and so on - )) . font-lock-type-face) - ) - "Minimal highlighting for Boogie mode") - -(defvar boogie-font-lock-keywords boogie-font-lock-keywords-1 - "Default highlighting for Boogie mode") - -;; syntax - -(defvar boogie-mode-syntax-table nil - "Syntax table for boogie-mode") - -(defun boogie-create-syntax-table () - (if boogie-mode-syntax-table - () - (setq boogie-mode-syntax-table (make-syntax-table)) - (set-syntax-table boogie-mode-syntax-table) - (modify-syntax-entry ?' "w" boogie-mode-syntax-table) - (modify-syntax-entry ?_ "w" boogie-mode-syntax-table))) - -;; menu - -(require 'easymenu) - -(defun boogie-menu () - (easy-menu-define - boogie-mode-menu (list boogie-mode-map) - "Boogie Mode Menu." - '("Boogie" - ["Run Boogie" boogie-run-boogie t] - "---" - ["Recolor buffer" font-lock-fontify-buffer t] - "---" - )) - (easy-menu-add boogie-mode-menu)) - -;; commands - -(defun boogie-command-line (file) - (concat "boogie -nologo -abbrevOutput " file)) - -(defun boogie-run-boogie () - "run Boogie to check the Boogie program" - (interactive) - (let ((f (buffer-name))) - (compile (boogie-command-line f)))) - -;; setting the mode - -(defun boogie-mode () - "Major mode for editing Boogie programs. - -\\{boogie-mode-map}" - (interactive) - (kill-all-local-variables) - (boogie-create-syntax-table) - ; hilight - (make-local-variable 'font-lock-defaults) - (setq font-lock-defaults '(boogie-font-lock-keywords)) - ; indentation - ; (make-local-variable 'indent-line-function) - ; (setq indent-line-function 'boogie-indent-line) - ; menu - ; providing the mode - (setq major-mode 'boogie-mode) - (setq mode-name "Boogie") - (use-local-map boogie-mode-map) - (font-lock-mode 1) - (boogie-menu) - (run-hooks 'boogie-mode-hook)) - -(provide 'boogie-mode) +;; boogie-mode.el - GNU Emacs mode for Boogie 2 +;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why + +(defvar boogie-mode-hook nil) + +(defvar boogie-mode-map nil + "Keymap for Boogie major mode") + +(if boogie-mode-map nil + (setq boogie-mode-map (make-keymap)) + (define-key boogie-mode-map "\C-c\C-c" 'boogie-run-boogie) + (define-key boogie-mode-map [(control return)] 'font-lock-fontify-buffer)) + +(setq auto-mode-alist + (append + '(("\\.bpl" . boogie-mode)) + auto-mode-alist)) + +;; font-lock + +(defun boogie-regexp-opt (l) + (concat "\\<" (concat (regexp-opt l t) "\\>"))) + +(defconst boogie-font-lock-keywords-1 + (list + ; comments have the form /* ... */ + '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face) + ; or // ... + '("//\\([^ +]\\)*" . font-lock-comment-face) + + `(,(boogie-regexp-opt '( + "type" "const" "function" "axiom" "var" "procedure" "implementation" + "returns" "where" "requires" "ensures" "modifies" "free" "unique" + "invariant" "extends" "complete" + )) . font-lock-builtin-face) + `(,(boogie-regexp-opt '( + "assert" "assume" "break" "call" "then" "else" "havoc" "if" "goto" "return" "while" + "old" "forall" "exists" "lambda" "cast" "div" "mod" + "false" "true")) . font-lock-keyword-face) + `(,(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" + "bv30" "bv31" "bv32" "bv33" "bv34" "bv35" "bv36" "bv37" "bv38" "bv39" + "bv40" "bv41" "bv42" "bv43" "bv44" "bv45" "bv46" "bv47" "bv48" "bv49" + "bv50" "bv51" "bv52" "bv53" "bv54" "bv55" "bv56" "bv57" "bv58" "bv59" + "bv60" "bv61" "bv62" "bv63" "bv64" ; and so on + )) . font-lock-type-face) + ) + "Minimal highlighting for Boogie mode") + +(defvar boogie-font-lock-keywords boogie-font-lock-keywords-1 + "Default highlighting for Boogie mode") + +;; syntax + +(defvar boogie-mode-syntax-table nil + "Syntax table for boogie-mode") + +(defun boogie-create-syntax-table () + (if boogie-mode-syntax-table + () + (setq boogie-mode-syntax-table (make-syntax-table)) + (set-syntax-table boogie-mode-syntax-table) + (modify-syntax-entry ?' "w" boogie-mode-syntax-table) + (modify-syntax-entry ?_ "w" boogie-mode-syntax-table))) + +;; menu + +(require 'easymenu) + +(defun boogie-menu () + (easy-menu-define + boogie-mode-menu (list boogie-mode-map) + "Boogie Mode Menu." + '("Boogie" + ["Run Boogie" boogie-run-boogie t] + "---" + ["Recolor buffer" font-lock-fontify-buffer t] + "---" + )) + (easy-menu-add boogie-mode-menu)) + +;; commands + +(defun boogie-command-line (file) + (concat "boogie -nologo -abbrevOutput " file)) + +(defun boogie-run-boogie () + "run Boogie to check the Boogie program" + (interactive) + (let ((f (buffer-name))) + (compile (boogie-command-line f)))) + +;; setting the mode + +(defun boogie-mode () + "Major mode for editing Boogie programs. + +\\{boogie-mode-map}" + (interactive) + (kill-all-local-variables) + (boogie-create-syntax-table) + ; hilight + (make-local-variable 'font-lock-defaults) + (setq font-lock-defaults '(boogie-font-lock-keywords)) + ; indentation + ; (make-local-variable 'indent-line-function) + ; (setq indent-line-function 'boogie-indent-line) + ; menu + ; providing the mode + (setq major-mode 'boogie-mode) + (setq mode-name "Boogie") + (use-local-map boogie-mode-map) + (font-lock-mode 1) + (boogie-menu) + (run-hooks 'boogie-mode-hook)) + +(provide 'boogie-mode) diff --git a/Util/VS2010/Boogie/BoogieLanguageService.sln b/Util/VS2010/Boogie/BoogieLanguageService.sln index 0ad3f0e7..d54efb50 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService.sln +++ b/Util/VS2010/Boogie/BoogieLanguageService.sln @@ -1,20 +1,20 @@ - -Microsoft Visual Studio Solution File, Format Version 11.00 -# Visual Studio 2010 -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieLanguageService", "BoogieLanguageService\BoogieLanguageService.csproj", "{66E611EE-84D8-4EB9-9A33-164A53E00553}" -EndProject -Global - GlobalSection(SolutionConfigurationPlatforms) = preSolution - Debug|Any CPU = Debug|Any CPU - Release|Any CPU = Release|Any CPU - EndGlobalSection - GlobalSection(ProjectConfigurationPlatforms) = postSolution - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Debug|Any CPU.Build.0 = Debug|Any CPU - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Release|Any CPU.ActiveCfg = Release|Any CPU - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Release|Any CPU.Build.0 = Release|Any CPU - EndGlobalSection - GlobalSection(SolutionProperties) = preSolution - HideSolutionNode = FALSE - EndGlobalSection -EndGlobal + +Microsoft Visual Studio Solution File, Format Version 11.00 +# Visual Studio 2010 +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieLanguageService", "BoogieLanguageService\BoogieLanguageService.csproj", "{66E611EE-84D8-4EB9-9A33-164A53E00553}" +EndProject +Global + GlobalSection(SolutionConfigurationPlatforms) = preSolution + Debug|Any CPU = Debug|Any CPU + Release|Any CPU = Release|Any CPU + EndGlobalSection + GlobalSection(ProjectConfigurationPlatforms) = postSolution + {66E611EE-84D8-4EB9-9A33-164A53E00553}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {66E611EE-84D8-4EB9-9A33-164A53E00553}.Debug|Any CPU.Build.0 = Debug|Any CPU + {66E611EE-84D8-4EB9-9A33-164A53E00553}.Release|Any CPU.ActiveCfg = Release|Any CPU + {66E611EE-84D8-4EB9-9A33-164A53E00553}.Release|Any CPU.Build.0 = Release|Any CPU + EndGlobalSection + GlobalSection(SolutionProperties) = preSolution + HideSolutionNode = FALSE + EndGlobalSection +EndGlobal diff --git a/Util/VS2010/Boogie/BoogieLanguageService/BoogieLanguageService.csproj b/Util/VS2010/Boogie/BoogieLanguageService/BoogieLanguageService.csproj index 86e0a2bc..a7a0fd0c 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/BoogieLanguageService.csproj +++ b/Util/VS2010/Boogie/BoogieLanguageService/BoogieLanguageService.csproj @@ -1,179 +1,179 @@ - - - - Debug - AnyCPU - 9.0.30729 - 2.0 - Library - Properties - Demo.BoogieLanguageService - BoogieLanguageService - True - Key.snk - v4.0 - {66E611EE-84D8-4EB9-9A33-164A53E00553} - - - 4.0 - - - publish\ - true - Disk - false - Foreground - 7 - Days - false - false - true - 0 - 1.0.0.%2a - false - false - true - - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - AllRules.ruleset - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - true - AllRules.ruleset - - - - False - Resources\Irony.dll - - - - False - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Package.LanguageService.10.0.dll - - - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.10.0.dll - - - False - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Immutable.10.0.dll - - - - False - True - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Interop.10.0.dll - - - - - - False - ..\..\..\..\..\Program Files\Microsoft Visual Studio 2008 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.TextManager.Interop.8.0.dll - - - - - - - - - - - - - - - - - - - - - - - - - - - True - True - Resources.resx - - - - - - - - ResXFileCodeGenerator - Resources.Designer.cs - Designer - - - true - Designer - - - - - - - - - - - - False - .NET Framework 3.5 SP1 Client Profile - false - - - False - .NET Framework 3.5 SP1 - true - - - False - Microsoft Visual Basic PowerPacks 10.0 - true - - - False - Windows Installer 3.1 - true - - - - - true - true - - - - + + + + Debug + AnyCPU + 9.0.30729 + 2.0 + Library + Properties + Demo.BoogieLanguageService + BoogieLanguageService + True + Key.snk + v4.0 + {66E611EE-84D8-4EB9-9A33-164A53E00553} + + + 4.0 + + + publish\ + true + Disk + false + Foreground + 7 + Days + false + false + true + 0 + 1.0.0.%2a + false + false + true + + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + AllRules.ruleset + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + true + AllRules.ruleset + + + + False + Resources\Irony.dll + + + + False + C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Package.LanguageService.10.0.dll + + + C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.10.0.dll + + + False + C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Immutable.10.0.dll + + + + False + True + C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Interop.10.0.dll + + + + + + False + ..\..\..\..\..\Program Files\Microsoft Visual Studio 2008 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.TextManager.Interop.8.0.dll + + + + + + + + + + + + + + + + + + + + + + + + + + + True + True + Resources.resx + + + + + + + + ResXFileCodeGenerator + Resources.Designer.cs + Designer + + + true + Designer + + + + + + + + + + + + False + .NET Framework 3.5 SP1 Client Profile + false + + + False + .NET Framework 3.5 SP1 + true + + + False + Microsoft Visual Basic PowerPacks 10.0 + true + + + False + Windows Installer 3.1 + true + + + + + true + true + + + + \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Configuration.cs b/Util/VS2010/Boogie/BoogieLanguageService/Configuration.cs index 97775fdf..3a3fed64 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Configuration.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Configuration.cs @@ -1,24 +1,24 @@ -using System; -using System.Collections.Generic; -using Microsoft.VisualStudio.Package; -using Microsoft.VisualStudio.TextManager.Interop; - -namespace Demo -{ - public static partial class Configuration - { - public const string Name = "Boogie"; - public const string FormatList = "Boogie File (*.bpl)\n*.bpl"; - - static Configuration() - { - // default colors - currently, these need to be declared - CreateColor("Keyword", COLORINDEX.CI_BLUE, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Comment", COLORINDEX.CI_DARKGREEN, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Identifier", COLORINDEX.CI_SYSPLAINTEXT_FG, COLORINDEX.CI_USERTEXT_BK); - CreateColor("String", COLORINDEX.CI_MAROON, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Number", COLORINDEX.CI_RED, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Text", COLORINDEX.CI_SYSPLAINTEXT_FG, COLORINDEX.CI_USERTEXT_BK); - } - } -} +using System; +using System.Collections.Generic; +using Microsoft.VisualStudio.Package; +using Microsoft.VisualStudio.TextManager.Interop; + +namespace Demo +{ + public static partial class Configuration + { + public const string Name = "Boogie"; + public const string FormatList = "Boogie File (*.bpl)\n*.bpl"; + + static Configuration() + { + // default colors - currently, these need to be declared + CreateColor("Keyword", COLORINDEX.CI_BLUE, COLORINDEX.CI_USERTEXT_BK); + CreateColor("Comment", COLORINDEX.CI_DARKGREEN, COLORINDEX.CI_USERTEXT_BK); + CreateColor("Identifier", COLORINDEX.CI_SYSPLAINTEXT_FG, COLORINDEX.CI_USERTEXT_BK); + CreateColor("String", COLORINDEX.CI_MAROON, COLORINDEX.CI_USERTEXT_BK); + CreateColor("Number", COLORINDEX.CI_RED, COLORINDEX.CI_USERTEXT_BK); + CreateColor("Text", COLORINDEX.CI_SYSPLAINTEXT_FG, COLORINDEX.CI_USERTEXT_BK); + } + } +} diff --git a/Util/VS2010/Boogie/BoogieLanguageService/GlobalSuppressions.cs b/Util/VS2010/Boogie/BoogieLanguageService/GlobalSuppressions.cs index f0857cbb..746e3dae 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/GlobalSuppressions.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/GlobalSuppressions.cs @@ -1,11 +1,11 @@ -// This file is used by Code Analysis to maintain SuppressMessage -// attributes that are applied to this project. Project-level -// suppressions either have no target or are given a specific target -// and scoped to a namespace, type, member, etc. -// -// To add a suppression to this file, right-click the message in the -// Error List, point to "Suppress Message(s)", and click "In Project -// Suppression File". You do not need to add suppressions to this -// file manually. - -[assembly: System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Design", "CA1017:MarkAssembliesWithComVisible")] +// This file is used by Code Analysis to maintain SuppressMessage +// attributes that are applied to this project. Project-level +// suppressions either have no target or are given a specific target +// and scoped to a namespace, type, member, etc. +// +// To add a suppression to this file, right-click the message in the +// Error List, point to "Suppress Message(s)", and click "In Project +// Suppression File". You do not need to add suppressions to this +// file manually. + +[assembly: System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Design", "CA1017:MarkAssembliesWithComVisible")] diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs index fd7c561d..bedb0cfa 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs @@ -1,397 +1,397 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using Irony.Parsing; - -namespace Demo -{ - [Language("Boogie", "1.0", "Microsoft Research Boogie, intermediate verification language")] - public class Grammar : Irony.Parsing.Grammar - { - public Grammar() { - #region 1. Terminals - NumberLiteral n = TerminalFactory.CreateCSharpNumber("number"); - StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String"); - - IdentifierTerminal ident = new IdentifierTerminal("Identifier"); - this.MarkReservedWords( - "assert", "assume", "axiom", - "bool", "break", - "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", - "bv30", "bv31", "bv32", - "bv64", - "call", "complete", "const", - "div", - "else", "ensures", "exists", "extends", - "false", "forall", "free", "function", - "goto", - "havoc", - "if", "implementation", "int", "invariant", - "lambda", - "mod", "modifies", - "old", - "procedure", - "real", "requires", "return", "returns", - "then", "true", "type", - "unique", - "var", - "where", "while" - ); - - StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote); - - Terminal dot = ToTerm(".", "dot"); - Terminal less = ToTerm("<"); - Terminal greater = ToTerm(">"); - Terminal iff = ToTerm("<==>"); - Terminal implication = ToTerm("==>"); - Terminal explication = ToTerm("<=="); - Terminal LBracket = ToTerm("["); - Terminal RBracket = ToTerm("]"); - Terminal LParen = ToTerm("("); - Terminal RParen = ToTerm(")"); - Terminal RCurly = ToTerm("}"); - Terminal LCurly = ToTerm("{"); - Terminal LDoubleCurly = ToTerm("{{"); - Terminal RDoubleCurly = ToTerm("}}"); - Terminal comma = ToTerm(","); - Terminal semicolon = ToTerm(";"); - Terminal colon = ToTerm(":"); - Terminal doubleColon = ToTerm("::"); - - #endregion - - #region 2. Non-terminals - #region 2.1 Expressions - NonTerminal expression = new NonTerminal("Expr"); - NonTerminal BinOp = new NonTerminal("BinOp"); - NonTerminal LUnOp = new NonTerminal("LUnOp"); - NonTerminal RUnOp = new NonTerminal("RUnOp"); - - NonTerminal ArrayConstructor = new NonTerminal("ArrayConstructor"); - #endregion - - #region 2.2 QualifiedName - //Expression List: expr1, expr2, expr3, .. - NonTerminal expressionList = new NonTerminal("ExprList"); - NonTerminal identList = new NonTerminal("identList"); - //A name in form: a.b.c().d[1,2].e .... - NonTerminal NewStmt = new NonTerminal("NewStmt"); - NonTerminal NewArrStmt = new NonTerminal("NewArrStmt"); - NonTerminal QualifiedName = new NonTerminal("QualifiedName"); - NonTerminal GenericsPostfix = new NonTerminal("GenericsPostfix"); - NonTerminal ArrayExpression = new NonTerminal("ArrayExpression"); - NonTerminal FunctionExpression = new NonTerminal("FunctionExpression"); - NonTerminal selectExpr = new NonTerminal("selectExpr"); - #endregion - - #region 2.3 Statement - NonTerminal Condition = new NonTerminal("Condition"); - - NonTerminal Statement = new NonTerminal("Statement"); - NonTerminal Statements = new NonTerminal("Statements"); - - //Block - NonTerminal blockStatement = new NonTerminal("CompoundStatement"); - #endregion - - #region 2.4 Program and Functions - NonTerminal Prog = new NonTerminal("Prog"); - NonTerminal anything = new NonTerminal("anything"); // temporary hack - NonTerminal declaration = new NonTerminal("declaration"); - NonTerminal classDecl = new NonTerminal("class decl"); - NonTerminal memberDecl = new NonTerminal("member decl"); - NonTerminal fieldDecl = new NonTerminal("field declaration"); - NonTerminal idType = new NonTerminal("identifier type"); - NonTerminal typeDecl = new NonTerminal("type reference"); - NonTerminal methodDecl = new NonTerminal("method declaration"); - NonTerminal formalParameters = new NonTerminal("formals"); - NonTerminal methodSpec = new NonTerminal("method spec"); - NonTerminal formalsList = new NonTerminal("ParamaterListOpt"); - NonTerminal functionDecl = new NonTerminal("function declaration"); - NonTerminal predicateDecl = new NonTerminal("predicate declaration"); - NonTerminal invariantDecl = new NonTerminal("invariant declaration"); - NonTerminal Semi = new NonTerminal("semi"); - NonTerminal Rhs = new NonTerminal("right-hand side"); - NonTerminal FieldInit = new NonTerminal("field init"); - NonTerminal FieldInits = new NonTerminal("field inits"); - NonTerminal installBounds = new NonTerminal("installBounds"); - NonTerminal localVarStmt = new NonTerminal("localVarStmt"); - NonTerminal evalstate = new NonTerminal("evalstate"); - NonTerminal channelDecl = new NonTerminal("channel declaration"); - NonTerminal loopSpec = new NonTerminal("loop specification"); - NonTerminal rdPermArg = new NonTerminal("rdPermArg"); - #endregion - - #endregion - - #region 3. BNF rules - - Semi.Rule = semicolon; - - #region 3.1 Expressions - selectExpr.Rule = (ToTerm("this") + ".").Q() + QualifiedName; - evalstate.Rule = - ident + ToTerm(".") + - (ToTerm("acquire") - | "release" - | "fork" + FunctionExpression - ) - ; - rdPermArg.Rule = ToTerm("*") | expression; - - expression.Rule = ToTerm("true") - | "false" - | "null" - | "maxlock" - | "lockbottom" - | "this" - | "result" - | s - | n - | QualifiedName - // The following is needed: to parse "A=" | "<=" | "is" - | "=" | "+=" | "-=" - | "." - | "==>" | "<==>" | "<<" - ; - - LUnOp.Rule = ToTerm("-") | "~" | "!"; - RUnOp.Rule = ToTerm("++") | "--"; - - ArrayConstructor.Rule = LBracket + expressionList + RBracket; - #endregion - - #region 3.2 QualifiedName - ArrayExpression.Rule = QualifiedName + LBracket + expressionList + RBracket; - FunctionExpression.Rule = QualifiedName + LParen + expressionList.Q() + RParen; - - QualifiedName.Rule = ident | QualifiedName + dot + ident; - - - GenericsPostfix.Rule = less + QualifiedName + greater; - - //ExprList.Rule = Expr.Plus(comma); - #endregion - - #region 3.3 Statement - Condition.Rule = LParen + expression + RParen; - installBounds.Rule - = "installBounds" - //= ToTerm("between") + expressionList + "and" + expressionList - //| "below" + expressionList - //| "below" + expressionList + "above" + expressionList - //| "above" + expressionList - //| "above" + expressionList + "below" + expressionList - ; - FieldInit.Rule - = ident + ":=" + expression - ; - FieldInits.Rule = MakeStarRule(FieldInits, ToTerm(","), FieldInit); - Rhs.Rule - = ToTerm("new") + ident - | ToTerm("new") + ident + "{" + FieldInits + "}" - | ToTerm("new") + ident + installBounds - | ToTerm("new") + ident + "{" + FieldInits + "}" + installBounds - | expression - ; - localVarStmt.Rule - = idType + ":=" + Rhs + Semi - | idType + Semi - ; - loopSpec.Rule - = ToTerm("invariant") + expression + Semi - | "lockchange" + expressionList + Semi - ; - - - - Statement.Rule = Semi - | "if" + Condition + Statement - ; - Statements.Rule = MakeStarRule(Statements, null, Statement); - blockStatement.Rule = LCurly + Statements + RCurly; - - - #endregion - - #region 3.4 Prog - Prog.Rule = anything.Star() + Eof; - - anything.Rule - = ToTerm("assert") - | "assume" | "axiom" | - "bool" | "break" | - "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" | - "bv30" | "bv31" | "bv32" | - "bv64" | - "call" | "complete" | "const" | - "else" | "ensures" | "exists" | "extends" | - "false" | "forall" | "free" | "function" | - "goto" | - "havoc" | - "if" | "implementation" | "int" | "invariant" | - "lambda" | - "modifies" | - "old" | - "procedure" | - "real" | "requires" | "return" | "returns" | - "then" | "true" | "type" | - "unique" | - "var" | - "where" | "while" - | ident - | "}" - | "{" - | "(" - | ")" - | "[" - | "]" - | "," - | ":" - | ";" - | "." - | "`" - | "==" - | "=" - | "!=" - | "<" - | "<=" - | ">=" - | ">" - | "=>" - | ":=" - | "+" - | "-" - | "*" - | "/" - | "%" - | "!!" - | "|" - | "!" - | "&&" - | "||" - | "==>" - | "<==>" - | "#" - | "$" - | "^" - | n - | stringLiteral - ; - - idType.Rule - = ident + ":" + typeDecl - | ident - ; - - typeDecl.Rule - = (ToTerm("int") | "bool" | "real" | ident) - ; - - fieldDecl.Rule - = ToTerm("var") + idType + Semi - | ToTerm("ghost") + "var" + idType + Semi - ; - - methodSpec.Rule = (ToTerm("requires") | "ensures" | "lockchange") + expression + Semi; - - formalsList.Rule = MakeStarRule(formalsList, comma, idType); - formalParameters.Rule = LParen + formalsList + RParen; - methodDecl.Rule = "method" + ident + formalParameters - + (("returns" + formalParameters) | Empty) - + methodSpec.Star() - + blockStatement; - functionDecl.Rule - = ToTerm("function") + ident + formalParameters + ":" + typeDecl + methodSpec.Star() + "{" + expression + "}"; - predicateDecl.Rule - = ToTerm("predicate") + ident + "{" + expression + "}"; - invariantDecl.Rule - = ToTerm("invariant") + expression + Semi; - - memberDecl.Rule - = fieldDecl - | invariantDecl - | methodDecl - //| conditionDecl - | predicateDecl - | functionDecl - ; - classDecl.Rule - = (ToTerm("external") | Empty) + "class" + ident + ("module" + ident | Empty) + "{" + memberDecl.Star() + "}"; - channelDecl.Rule - = ToTerm("channel") + ident + formalParameters + "where" + expression + Semi - | ToTerm("channel") + ident + formalParameters + Semi; - declaration.Rule = classDecl | channelDecl - ; - - - Terminal Comment = new CommentTerminal("Comment", "/*", "*/"); - NonGrammarTerminals.Add(Comment); - Terminal LineComment = new CommentTerminal("LineComment", "//", "\n"); - NonGrammarTerminals.Add(LineComment); - #endregion - #endregion - - #region 4. Set starting symbol - this.Root = Prog; // Set grammar root - #endregion - - #region 5. Operators precedence - RegisterOperators(1, "<==>"); - RegisterOperators(2, "+", "-"); - RegisterOperators(3, "*", "div", "mod", "!!"); - RegisterOperators(4, Associativity.Right, "^"); - RegisterOperators(5, "||"); - RegisterOperators(6, "&&"); - RegisterOperators(7, "==", "=", "!=", ">", "<", ">=", "<="); - RegisterOperators(8, "in"); - RegisterOperators(9, "-", "!", "++", "--"); - RegisterOperators(10, "==>"); - RegisterOperators(11, "."); - - //RegisterOperators(10, Associativity.Right, ".",",", ")", "(", "]", "[", "{", "}"); - //RegisterOperators(11, Associativity.Right, "else"); - #endregion - - #region 6. Punctuation symbols - RegisterPunctuation("(", ")", "[", "]", "{", "}", ",", ";"); - #endregion - } - } -} +using System; +using System.Collections.Generic; +using System.Linq; +using Irony.Parsing; + +namespace Demo +{ + [Language("Boogie", "1.0", "Microsoft Research Boogie, intermediate verification language")] + public class Grammar : Irony.Parsing.Grammar + { + public Grammar() { + #region 1. Terminals + NumberLiteral n = TerminalFactory.CreateCSharpNumber("number"); + StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String"); + + IdentifierTerminal ident = new IdentifierTerminal("Identifier"); + this.MarkReservedWords( + "assert", "assume", "axiom", + "bool", "break", + "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", + "bv30", "bv31", "bv32", + "bv64", + "call", "complete", "const", + "div", + "else", "ensures", "exists", "extends", + "false", "forall", "free", "function", + "goto", + "havoc", + "if", "implementation", "int", "invariant", + "lambda", + "mod", "modifies", + "old", + "procedure", + "real", "requires", "return", "returns", + "then", "true", "type", + "unique", + "var", + "where", "while" + ); + + StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote); + + Terminal dot = ToTerm(".", "dot"); + Terminal less = ToTerm("<"); + Terminal greater = ToTerm(">"); + Terminal iff = ToTerm("<==>"); + Terminal implication = ToTerm("==>"); + Terminal explication = ToTerm("<=="); + Terminal LBracket = ToTerm("["); + Terminal RBracket = ToTerm("]"); + Terminal LParen = ToTerm("("); + Terminal RParen = ToTerm(")"); + Terminal RCurly = ToTerm("}"); + Terminal LCurly = ToTerm("{"); + Terminal LDoubleCurly = ToTerm("{{"); + Terminal RDoubleCurly = ToTerm("}}"); + Terminal comma = ToTerm(","); + Terminal semicolon = ToTerm(";"); + Terminal colon = ToTerm(":"); + Terminal doubleColon = ToTerm("::"); + + #endregion + + #region 2. Non-terminals + #region 2.1 Expressions + NonTerminal expression = new NonTerminal("Expr"); + NonTerminal BinOp = new NonTerminal("BinOp"); + NonTerminal LUnOp = new NonTerminal("LUnOp"); + NonTerminal RUnOp = new NonTerminal("RUnOp"); + + NonTerminal ArrayConstructor = new NonTerminal("ArrayConstructor"); + #endregion + + #region 2.2 QualifiedName + //Expression List: expr1, expr2, expr3, .. + NonTerminal expressionList = new NonTerminal("ExprList"); + NonTerminal identList = new NonTerminal("identList"); + //A name in form: a.b.c().d[1,2].e .... + NonTerminal NewStmt = new NonTerminal("NewStmt"); + NonTerminal NewArrStmt = new NonTerminal("NewArrStmt"); + NonTerminal QualifiedName = new NonTerminal("QualifiedName"); + NonTerminal GenericsPostfix = new NonTerminal("GenericsPostfix"); + NonTerminal ArrayExpression = new NonTerminal("ArrayExpression"); + NonTerminal FunctionExpression = new NonTerminal("FunctionExpression"); + NonTerminal selectExpr = new NonTerminal("selectExpr"); + #endregion + + #region 2.3 Statement + NonTerminal Condition = new NonTerminal("Condition"); + + NonTerminal Statement = new NonTerminal("Statement"); + NonTerminal Statements = new NonTerminal("Statements"); + + //Block + NonTerminal blockStatement = new NonTerminal("CompoundStatement"); + #endregion + + #region 2.4 Program and Functions + NonTerminal Prog = new NonTerminal("Prog"); + NonTerminal anything = new NonTerminal("anything"); // temporary hack + NonTerminal declaration = new NonTerminal("declaration"); + NonTerminal classDecl = new NonTerminal("class decl"); + NonTerminal memberDecl = new NonTerminal("member decl"); + NonTerminal fieldDecl = new NonTerminal("field declaration"); + NonTerminal idType = new NonTerminal("identifier type"); + NonTerminal typeDecl = new NonTerminal("type reference"); + NonTerminal methodDecl = new NonTerminal("method declaration"); + NonTerminal formalParameters = new NonTerminal("formals"); + NonTerminal methodSpec = new NonTerminal("method spec"); + NonTerminal formalsList = new NonTerminal("ParamaterListOpt"); + NonTerminal functionDecl = new NonTerminal("function declaration"); + NonTerminal predicateDecl = new NonTerminal("predicate declaration"); + NonTerminal invariantDecl = new NonTerminal("invariant declaration"); + NonTerminal Semi = new NonTerminal("semi"); + NonTerminal Rhs = new NonTerminal("right-hand side"); + NonTerminal FieldInit = new NonTerminal("field init"); + NonTerminal FieldInits = new NonTerminal("field inits"); + NonTerminal installBounds = new NonTerminal("installBounds"); + NonTerminal localVarStmt = new NonTerminal("localVarStmt"); + NonTerminal evalstate = new NonTerminal("evalstate"); + NonTerminal channelDecl = new NonTerminal("channel declaration"); + NonTerminal loopSpec = new NonTerminal("loop specification"); + NonTerminal rdPermArg = new NonTerminal("rdPermArg"); + #endregion + + #endregion + + #region 3. BNF rules + + Semi.Rule = semicolon; + + #region 3.1 Expressions + selectExpr.Rule = (ToTerm("this") + ".").Q() + QualifiedName; + evalstate.Rule = + ident + ToTerm(".") + + (ToTerm("acquire") + | "release" + | "fork" + FunctionExpression + ) + ; + rdPermArg.Rule = ToTerm("*") | expression; + + expression.Rule = ToTerm("true") + | "false" + | "null" + | "maxlock" + | "lockbottom" + | "this" + | "result" + | s + | n + | QualifiedName + // The following is needed: to parse "A=" | "<=" | "is" + | "=" | "+=" | "-=" + | "." + | "==>" | "<==>" | "<<" + ; + + LUnOp.Rule = ToTerm("-") | "~" | "!"; + RUnOp.Rule = ToTerm("++") | "--"; + + ArrayConstructor.Rule = LBracket + expressionList + RBracket; + #endregion + + #region 3.2 QualifiedName + ArrayExpression.Rule = QualifiedName + LBracket + expressionList + RBracket; + FunctionExpression.Rule = QualifiedName + LParen + expressionList.Q() + RParen; + + QualifiedName.Rule = ident | QualifiedName + dot + ident; + + + GenericsPostfix.Rule = less + QualifiedName + greater; + + //ExprList.Rule = Expr.Plus(comma); + #endregion + + #region 3.3 Statement + Condition.Rule = LParen + expression + RParen; + installBounds.Rule + = "installBounds" + //= ToTerm("between") + expressionList + "and" + expressionList + //| "below" + expressionList + //| "below" + expressionList + "above" + expressionList + //| "above" + expressionList + //| "above" + expressionList + "below" + expressionList + ; + FieldInit.Rule + = ident + ":=" + expression + ; + FieldInits.Rule = MakeStarRule(FieldInits, ToTerm(","), FieldInit); + Rhs.Rule + = ToTerm("new") + ident + | ToTerm("new") + ident + "{" + FieldInits + "}" + | ToTerm("new") + ident + installBounds + | ToTerm("new") + ident + "{" + FieldInits + "}" + installBounds + | expression + ; + localVarStmt.Rule + = idType + ":=" + Rhs + Semi + | idType + Semi + ; + loopSpec.Rule + = ToTerm("invariant") + expression + Semi + | "lockchange" + expressionList + Semi + ; + + + + Statement.Rule = Semi + | "if" + Condition + Statement + ; + Statements.Rule = MakeStarRule(Statements, null, Statement); + blockStatement.Rule = LCurly + Statements + RCurly; + + + #endregion + + #region 3.4 Prog + Prog.Rule = anything.Star() + Eof; + + anything.Rule + = ToTerm("assert") + | "assume" | "axiom" | + "bool" | "break" | + "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" | + "bv30" | "bv31" | "bv32" | + "bv64" | + "call" | "complete" | "const" | + "else" | "ensures" | "exists" | "extends" | + "false" | "forall" | "free" | "function" | + "goto" | + "havoc" | + "if" | "implementation" | "int" | "invariant" | + "lambda" | + "modifies" | + "old" | + "procedure" | + "real" | "requires" | "return" | "returns" | + "then" | "true" | "type" | + "unique" | + "var" | + "where" | "while" + | ident + | "}" + | "{" + | "(" + | ")" + | "[" + | "]" + | "," + | ":" + | ";" + | "." + | "`" + | "==" + | "=" + | "!=" + | "<" + | "<=" + | ">=" + | ">" + | "=>" + | ":=" + | "+" + | "-" + | "*" + | "/" + | "%" + | "!!" + | "|" + | "!" + | "&&" + | "||" + | "==>" + | "<==>" + | "#" + | "$" + | "^" + | n + | stringLiteral + ; + + idType.Rule + = ident + ":" + typeDecl + | ident + ; + + typeDecl.Rule + = (ToTerm("int") | "bool" | "real" | ident) + ; + + fieldDecl.Rule + = ToTerm("var") + idType + Semi + | ToTerm("ghost") + "var" + idType + Semi + ; + + methodSpec.Rule = (ToTerm("requires") | "ensures" | "lockchange") + expression + Semi; + + formalsList.Rule = MakeStarRule(formalsList, comma, idType); + formalParameters.Rule = LParen + formalsList + RParen; + methodDecl.Rule = "method" + ident + formalParameters + + (("returns" + formalParameters) | Empty) + + methodSpec.Star() + + blockStatement; + functionDecl.Rule + = ToTerm("function") + ident + formalParameters + ":" + typeDecl + methodSpec.Star() + "{" + expression + "}"; + predicateDecl.Rule + = ToTerm("predicate") + ident + "{" + expression + "}"; + invariantDecl.Rule + = ToTerm("invariant") + expression + Semi; + + memberDecl.Rule + = fieldDecl + | invariantDecl + | methodDecl + //| conditionDecl + | predicateDecl + | functionDecl + ; + classDecl.Rule + = (ToTerm("external") | Empty) + "class" + ident + ("module" + ident | Empty) + "{" + memberDecl.Star() + "}"; + channelDecl.Rule + = ToTerm("channel") + ident + formalParameters + "where" + expression + Semi + | ToTerm("channel") + ident + formalParameters + Semi; + declaration.Rule = classDecl | channelDecl + ; + + + Terminal Comment = new CommentTerminal("Comment", "/*", "*/"); + NonGrammarTerminals.Add(Comment); + Terminal LineComment = new CommentTerminal("LineComment", "//", "\n"); + NonGrammarTerminals.Add(LineComment); + #endregion + #endregion + + #region 4. Set starting symbol + this.Root = Prog; // Set grammar root + #endregion + + #region 5. Operators precedence + RegisterOperators(1, "<==>"); + RegisterOperators(2, "+", "-"); + RegisterOperators(3, "*", "div", "mod", "!!"); + RegisterOperators(4, Associativity.Right, "^"); + RegisterOperators(5, "||"); + RegisterOperators(6, "&&"); + RegisterOperators(7, "==", "=", "!=", ">", "<", ">=", "<="); + RegisterOperators(8, "in"); + RegisterOperators(9, "-", "!", "++", "--"); + RegisterOperators(10, "==>"); + RegisterOperators(11, "."); + + //RegisterOperators(10, Associativity.Right, ".",",", ")", "(", "]", "[", "{", "}"); + //RegisterOperators(11, Associativity.Right, "else"); + #endregion + + #region 6. Punctuation symbols + RegisterPunctuation("(", ")", "[", "]", "{", "}", ",", ";"); + #endregion + } + } +} diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Guids.cs b/Util/VS2010/Boogie/BoogieLanguageService/Guids.cs index a09463fd..73d0cbb0 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Guids.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Guids.cs @@ -1,13 +1,13 @@ -using System; - -namespace Demo -{ - static class GuidList - { - public const string guidIronyLanguageServiceString = "0A949930-AB4A-4A00-ABD0-191E81249240"; - public const string guidIronyLanguageServicePkgString = "FC7F6CE7-49C7-40C9-8636-EB37A936D77F"; - public const string guidIronyLanguageServiceCmdSetString = "72B8E853-2250-426B-9566-6D318ADE7C2D"; - - public static readonly Guid guidIronyLanguageServiceCmdSet = new Guid(guidIronyLanguageServiceCmdSetString); - }; +using System; + +namespace Demo +{ + static class GuidList + { + public const string guidIronyLanguageServiceString = "0A949930-AB4A-4A00-ABD0-191E81249240"; + public const string guidIronyLanguageServicePkgString = "FC7F6CE7-49C7-40C9-8636-EB37A936D77F"; + public const string guidIronyLanguageServiceCmdSetString = "72B8E853-2250-426B-9566-6D318ADE7C2D"; + + public static readonly Guid guidIronyLanguageServiceCmdSet = new Guid(guidIronyLanguageServiceCmdSetString); + }; } \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/AuthoringScope.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/AuthoringScope.cs index 9a49dbe4..b5bc4a0e 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/AuthoringScope.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/AuthoringScope.cs @@ -1,66 +1,66 @@ -using System; -using System.Collections.Generic; -using Microsoft.VisualStudio; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class AuthoringScope : Microsoft.VisualStudio.Package.AuthoringScope - { - public AuthoringScope(object parseResult) - { - this.parseResult = parseResult; - - // how should this be set? - this.resolver = new Resolver(); - } - - object parseResult; - IASTResolver resolver; - - // ParseReason.QuickInfo - public override string GetDataTipText(int line, int col, out TextSpan span) - { - span = new TextSpan(); - return null; - } - - // ParseReason.CompleteWord - // ParseReason.DisplayMemberList - // ParseReason.MemberSelect - // ParseReason.MemberSelectAndHilightBraces - public override Microsoft.VisualStudio.Package.Declarations GetDeclarations(IVsTextView view, int line, int col, TokenInfo info, ParseReason reason) - { - IList declarations; - switch (reason) - { - case ParseReason.CompleteWord: - declarations = resolver.FindCompletions(parseResult, line, col); - break; - case ParseReason.DisplayMemberList: - case ParseReason.MemberSelect: - case ParseReason.MemberSelectAndHighlightBraces: - declarations = resolver.FindMembers(parseResult, line, col); - break; - default: - throw new ArgumentException("reason"); - } - - return new Declarations(declarations); - } - - // ParseReason.GetMethods - public override Microsoft.VisualStudio.Package.Methods GetMethods(int line, int col, string name) - { - return new Methods(resolver.FindMethods(parseResult, line, col, name)); - } - - // ParseReason.Goto - public override string Goto(VSConstants.VSStd97CmdID cmd, IVsTextView textView, int line, int col, out TextSpan span) - { - span = new TextSpan(); - return null; - } - } +using System; +using System.Collections.Generic; +using Microsoft.VisualStudio; +using Microsoft.VisualStudio.TextManager.Interop; +using Microsoft.VisualStudio.Package; + +namespace Demo +{ + public class AuthoringScope : Microsoft.VisualStudio.Package.AuthoringScope + { + public AuthoringScope(object parseResult) + { + this.parseResult = parseResult; + + // how should this be set? + this.resolver = new Resolver(); + } + + object parseResult; + IASTResolver resolver; + + // ParseReason.QuickInfo + public override string GetDataTipText(int line, int col, out TextSpan span) + { + span = new TextSpan(); + return null; + } + + // ParseReason.CompleteWord + // ParseReason.DisplayMemberList + // ParseReason.MemberSelect + // ParseReason.MemberSelectAndHilightBraces + public override Microsoft.VisualStudio.Package.Declarations GetDeclarations(IVsTextView view, int line, int col, TokenInfo info, ParseReason reason) + { + IList declarations; + switch (reason) + { + case ParseReason.CompleteWord: + declarations = resolver.FindCompletions(parseResult, line, col); + break; + case ParseReason.DisplayMemberList: + case ParseReason.MemberSelect: + case ParseReason.MemberSelectAndHighlightBraces: + declarations = resolver.FindMembers(parseResult, line, col); + break; + default: + throw new ArgumentException("reason"); + } + + return new Declarations(declarations); + } + + // ParseReason.GetMethods + public override Microsoft.VisualStudio.Package.Methods GetMethods(int line, int col, string name) + { + return new Methods(resolver.FindMethods(parseResult, line, col, name)); + } + + // ParseReason.Goto + public override string Goto(VSConstants.VSStd97CmdID cmd, IVsTextView textView, int line, int col, out TextSpan span) + { + span = new TextSpan(); + return null; + } + } } \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Configuration.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Configuration.cs index f7412393..706471da 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Configuration.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Configuration.cs @@ -1,116 +1,116 @@ -using System; -using System.Collections.Generic; -using Microsoft.VisualStudio.Package; -using Microsoft.VisualStudio.TextManager.Interop; - -namespace Demo -{ - public static partial class Configuration - { - public static Grammar Grammar = new Grammar(); - static List colorableItems = new List(); - - public static IList ColorableItems - { - get { return colorableItems; } - } - - public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background) - { - return CreateColor(name, foreground, background, false, false); - } - - public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough) - { - colorableItems.Add(new ColorableItem(name, foreground, background, bold, strikethrough)); - return (TokenColor)colorableItems.Count; - } - - public static void ColorToken(string tokenName, TokenType type, TokenColor color, TokenTriggers trigger) - { - definitions[tokenName] = new TokenDefinition(type, color, trigger); - } - - public static TokenDefinition GetDefinition(string tokenName) - { - TokenDefinition result; - return definitions.TryGetValue(tokenName, out result) ? result : defaultDefinition; - } - - private static TokenDefinition defaultDefinition = new TokenDefinition(TokenType.Text, TokenColor.Text, TokenTriggers.None); - private static Dictionary definitions = new Dictionary(); - - public struct TokenDefinition - { - public TokenDefinition(TokenType type, TokenColor color, TokenTriggers triggers) - { - this.TokenType = type; - this.TokenColor = color; - this.TokenTriggers = triggers; - } - - public TokenType TokenType; - public TokenColor TokenColor; - public TokenTriggers TokenTriggers; - } - } - - public class ColorableItem : Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem - { - private string displayName; - private COLORINDEX background; - private COLORINDEX foreground; - private uint fontFlags = (uint)FONTFLAGS.FF_DEFAULT; - - public ColorableItem(string displayName, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough) - { - this.displayName = displayName; - this.background = background; - this.foreground = foreground; - - if (bold) - this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_BOLD; - if (strikethrough) - this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_STRIKETHROUGH; - } - - #region IVsColorableItem Members - public int GetDefaultColors(COLORINDEX[] piForeground, COLORINDEX[] piBackground) - { - if (null == piForeground) - { - throw new ArgumentNullException("piForeground"); - } - if (0 == piForeground.Length) - { - throw new ArgumentOutOfRangeException("piForeground"); - } - piForeground[0] = foreground; - - if (null == piBackground) - { - throw new ArgumentNullException("piBackground"); - } - if (0 == piBackground.Length) - { - throw new ArgumentOutOfRangeException("piBackground"); - } - piBackground[0] = background; - - return Microsoft.VisualStudio.VSConstants.S_OK; - } - - public int GetDefaultFontFlags(out uint pdwFontFlags) - { - pdwFontFlags = this.fontFlags; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - - public int GetDisplayName(out string pbstrName) - { - pbstrName = displayName; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - #endregion - } +using System; +using System.Collections.Generic; +using Microsoft.VisualStudio.Package; +using Microsoft.VisualStudio.TextManager.Interop; + +namespace Demo +{ + public static partial class Configuration + { + public static Grammar Grammar = new Grammar(); + static List colorableItems = new List(); + + public static IList ColorableItems + { + get { return colorableItems; } + } + + public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background) + { + return CreateColor(name, foreground, background, false, false); + } + + public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough) + { + colorableItems.Add(new ColorableItem(name, foreground, background, bold, strikethrough)); + return (TokenColor)colorableItems.Count; + } + + public static void ColorToken(string tokenName, TokenType type, TokenColor color, TokenTriggers trigger) + { + definitions[tokenName] = new TokenDefinition(type, color, trigger); + } + + public static TokenDefinition GetDefinition(string tokenName) + { + TokenDefinition result; + return definitions.TryGetValue(tokenName, out result) ? result : defaultDefinition; + } + + private static TokenDefinition defaultDefinition = new TokenDefinition(TokenType.Text, TokenColor.Text, TokenTriggers.None); + private static Dictionary definitions = new Dictionary(); + + public struct TokenDefinition + { + public TokenDefinition(TokenType type, TokenColor color, TokenTriggers triggers) + { + this.TokenType = type; + this.TokenColor = color; + this.TokenTriggers = triggers; + } + + public TokenType TokenType; + public TokenColor TokenColor; + public TokenTriggers TokenTriggers; + } + } + + public class ColorableItem : Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem + { + private string displayName; + private COLORINDEX background; + private COLORINDEX foreground; + private uint fontFlags = (uint)FONTFLAGS.FF_DEFAULT; + + public ColorableItem(string displayName, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough) + { + this.displayName = displayName; + this.background = background; + this.foreground = foreground; + + if (bold) + this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_BOLD; + if (strikethrough) + this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_STRIKETHROUGH; + } + + #region IVsColorableItem Members + public int GetDefaultColors(COLORINDEX[] piForeground, COLORINDEX[] piBackground) + { + if (null == piForeground) + { + throw new ArgumentNullException("piForeground"); + } + if (0 == piForeground.Length) + { + throw new ArgumentOutOfRangeException("piForeground"); + } + piForeground[0] = foreground; + + if (null == piBackground) + { + throw new ArgumentNullException("piBackground"); + } + if (0 == piBackground.Length) + { + throw new ArgumentOutOfRangeException("piBackground"); + } + piBackground[0] = background; + + return Microsoft.VisualStudio.VSConstants.S_OK; + } + + public int GetDefaultFontFlags(out uint pdwFontFlags) + { + pdwFontFlags = this.fontFlags; + return Microsoft.VisualStudio.VSConstants.S_OK; + } + + public int GetDisplayName(out string pbstrName) + { + pbstrName = displayName; + return Microsoft.VisualStudio.VSConstants.S_OK; + } + #endregion + } } \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declaration.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declaration.cs index c0fda5ca..fa1ac730 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declaration.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declaration.cs @@ -1,30 +1,30 @@ -using System; -using System.Collections.Generic; - -namespace Demo -{ - public struct Declaration : IComparable - { - public Declaration(string description, string displayText, int glyph, string name) - { - this.Description = description; - this.DisplayText = displayText; - this.Glyph = glyph; - this.Name = name; - } - - public string Description; - public string DisplayText; - public int Glyph; - public string Name; - - #region IComparable Members - - public int CompareTo(Declaration other) - { - return DisplayText.CompareTo(other.DisplayText); - } - - #endregion - } +using System; +using System.Collections.Generic; + +namespace Demo +{ + public struct Declaration : IComparable + { + public Declaration(string description, string displayText, int glyph, string name) + { + this.Description = description; + this.DisplayText = displayText; + this.Glyph = glyph; + this.Name = name; + } + + public string Description; + public string DisplayText; + public int Glyph; + public string Name; + + #region IComparable Members + + public int CompareTo(Declaration other) + { + return DisplayText.CompareTo(other.DisplayText); + } + + #endregion + } } \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declarations.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declarations.cs index 98a411ce..ddda8783 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declarations.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declarations.cs @@ -1,56 +1,56 @@ -/*************************************************************************** - -Copyright (c) Microsoft Corporation. All rights reserved. -This code is licensed under the Visual Studio SDK license terms. -THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF -ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY -IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR -PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT. - -***************************************************************************/ - -using System; -using System.Collections.Generic; -using System.Text; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class Declarations : Microsoft.VisualStudio.Package.Declarations - { - IList declarations; - public Declarations(IList declarations) - { - this.declarations = declarations; - } - - public override int GetCount() - { - return declarations.Count; - } - - public override string GetDescription(int index) - { - return declarations[index].Description; - } - - public override string GetDisplayText(int index) - { - return declarations[index].DisplayText; - } - - public override int GetGlyph(int index) - { - return declarations[index].Glyph; - } - - public override string GetName(int index) - { - if (index >= 0) - return declarations[index].Name; - - return null; - } - } +/*************************************************************************** + +Copyright (c) Microsoft Corporation. All rights reserved. +This code is licensed under the Visual Studio SDK license terms. +THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF +ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY +IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR +PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT. + +***************************************************************************/ + +using System; +using System.Collections.Generic; +using System.Text; +using Microsoft.VisualStudio.TextManager.Interop; +using Microsoft.VisualStudio.Package; + +namespace Demo +{ + public class Declarations : Microsoft.VisualStudio.Package.Declarations + { + IList declarations; + public Declarations(IList declarations) + { + this.declarations = declarations; + } + + public override int GetCount() + { + return declarations.Count; + } + + public override string GetDescription(int index) + { + return declarations[index].Description; + } + + public override string GetDisplayText(int index) + { + return declarations[index].DisplayText; + } + + public override int GetGlyph(int index) + { + return declarations[index].Glyph; + } + + public override string GetName(int index) + { + if (index >= 0) + return declarations[index].Name; + + return null; + } + } } \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IASTResolver.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IASTResolver.cs index 8de1a454..f3ff41f4 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IASTResolver.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IASTResolver.cs @@ -1,13 +1,13 @@ -using System; -using System.Collections.Generic; - -namespace Demo -{ - interface IASTResolver - { - IList FindCompletions(object result, int line, int col); - IList FindMembers(object result, int line, int col); - string FindQuickInfo(object result, int line, int col); - IList FindMethods(object result, int line, int col, string name); - } +using System; +using System.Collections.Generic; + +namespace Demo +{ + interface IASTResolver + { + IList FindCompletions(object result, int line, int col); + IList FindMembers(object result, int line, int col); + string FindQuickInfo(object result, int line, int col); + IList FindMethods(object result, int line, int col, string name); + } } \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs index 1d1bdce4..30279078 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs @@ -1,343 +1,343 @@ -using System; -using System.Collections.Generic; -using System.Diagnostics; -using Microsoft.VisualStudio; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -using Irony.Parsing; -using Irony.Ast; - -using System.IO; - -namespace Demo -{ - public class IronyLanguageService : Microsoft.VisualStudio.Package.LanguageService - { - private Grammar grammar; - private Parser parser; - private ParsingContext context; - - public IronyLanguageService() - { - grammar = new Grammar(); - parser = new Parser(Configuration.Grammar); - context = new ParsingContext(parser); - } - - - #region Custom Colors - public override int GetColorableItem(int index, out IVsColorableItem item) - { - if (index <= Configuration.ColorableItems.Count) - { - item = Configuration.ColorableItems[index - 1]; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - else - { - throw new ArgumentNullException("index"); - } - } - - public override int GetItemCount(out int count) - { - count = Configuration.ColorableItems.Count; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - #endregion - - #region MPF Accessor and Factory specialisation - private LanguagePreferences preferences; - public override LanguagePreferences GetLanguagePreferences() - { - if (this.preferences == null) - { - this.preferences = new LanguagePreferences(this.Site, - typeof(IronyLanguageService).GUID, - this.Name); - this.preferences.Init(); - } - - return this.preferences; - } - - public override Microsoft.VisualStudio.Package.Source CreateSource(IVsTextLines buffer) - { - return new Source(this, buffer, this.GetColorizer(buffer)); - } - - private IScanner scanner; - public override IScanner GetScanner(IVsTextLines buffer) - { - if (scanner == null) - this.scanner = new LineScanner(grammar); - - return this.scanner; - } - #endregion - - public override void OnIdle(bool periodic) - { - // from IronPythonLanguage sample - // this appears to be necessary to get a parse request with ParseReason = Check? - Source src = (Source)GetSource(this.LastActiveTextView); - if (src != null && src.LastParseTime >= Int32.MaxValue >> 12) - { - src.LastParseTime = 0; - } - base.OnIdle(periodic); - } - - public override Microsoft.VisualStudio.Package.AuthoringScope ParseSource(ParseRequest req) - { - Debug.Print("ParseSource at ({0}:{1}), reason {2}", req.Line, req.Col, req.Reason); - Source source = (Source)this.GetSource(req.FileName); - switch (req.Reason) - { - case ParseReason.Check: - // This is where you perform your syntax highlighting. - // Parse entire source as given in req.Text. - // Store results in the AuthoringScope object. - var parsed = parser.Parse(req.Text, req.FileName); - var root = parsed.Root; - if (root != null) { - - AstNode node = (AstNode)root.AstNode; - source.ParseResult = node; - } - - // Used for brace matching. - TokenStack braces = parser.Context.OpenBraces; - foreach (Token brace in braces) { - if (brace.OtherBrace == null) continue; - TextSpan openBrace = new TextSpan(); - openBrace.iStartLine = brace.Location.Line; - openBrace.iStartIndex = brace.Location.Column; - openBrace.iEndLine = brace.Location.Line; - openBrace.iEndIndex = openBrace.iStartIndex + brace.Length; - - TextSpan closeBrace = new TextSpan(); - closeBrace.iStartLine = brace.OtherBrace.Location.Line; - closeBrace.iStartIndex = brace.OtherBrace.Location.Column; - closeBrace.iEndLine = brace.OtherBrace.Location.Line; - closeBrace.iEndIndex = closeBrace.iStartIndex + brace.OtherBrace.Length; - - if (source.Braces == null) { - source.Braces = new List(); - } - source.Braces.Add(new TextSpan[2] { openBrace, closeBrace }); - } - - if (parser.Context.CurrentParseTree.ParserMessages.Count > 0) { - foreach (ParserMessage error in parser.Context.CurrentParseTree.ParserMessages) { - TextSpan span = new TextSpan(); - span.iStartLine = span.iEndLine = error.Location.Line - 1; - span.iStartIndex = error.Location.Column; - span.iEndIndex = error.Location.Position; - req.Sink.AddError(req.FileName, error.Message, span, Severity.Error); - } - } else { // parse looks okay, send it to Boogie. - if (!File.Exists(@"C:\tmp\StartBoogie.bat")) { - AddErrorBecauseOfToolProblems(req, @"Can't find C:\tmp\StartBoogie.bat"); - } else { - - // From: http://dotnetperls.com/process-redirect-standard-output - // (Also, see: http://msdn.microsoft.com/en-us/library/system.diagnostics.processstartinfo.redirectstandardoutput.aspx) - // - // Setup the process with the ProcessStartInfo class. - // - ProcessStartInfo start = new ProcessStartInfo(); - start.FileName = @"cmd.exe"; - start.Arguments = @"/c C:\tmp\StartBoogie.bat"; // Specify exe name. - start.UseShellExecute = false; - start.RedirectStandardInput = true; - start.RedirectStandardOutput = true; - start.CreateNoWindow = true; - //start.WindowStyle = ProcessWindowStyle.Minimized; // need this or else you see the window pop up - // - // Start the process. - // - using (Process process = Process.Start(start)) { - // - // Push the file contents to the new process - // - StreamWriter myStreamWriter = process.StandardInput; - myStreamWriter.WriteLine(req.Text); - myStreamWriter.Close(); - // - // Read in all the text from the process with the StreamReader. - // - using (StreamReader reader = process.StandardOutput) { - //string result = reader.ReadToEnd(); - //Console.Write(result); - - for (string line = reader.ReadLine(); !String.IsNullOrEmpty(line); line = reader.ReadLine()) { - // the lines of interest have the form "filename(line,col): some_error_label: error_message" - // where "some_error_label" is "Error" or "syntax error" or "Error BP5003" or "Related location" - string message; - int n = line.IndexOf("): ", 2); // we start at 2, to avoid problems with "C:\..." - if (n == -1) { - continue; - } else { - int m = line.IndexOf(": ", n + 3); - if (m == -1) { - continue; - } - message = line.Substring(m + 2); - } - line = line.Substring(0, n); // line now has the form "filename(line,col" - - n = line.LastIndexOf(','); - if (n == -1) { continue; } - var colString = line.Substring(n + 1); - line = line.Substring(0, n); // line now has the form "filename(line" - - n = line.LastIndexOf('('); - if (n == -1) { continue; } - var lineString = line.Substring(n + 1); - - try { - TextSpan span = new TextSpan(); - span.iStartLine = span.iEndLine = Int32.Parse(lineString) - 1; - span.iStartIndex = Int32.Parse(colString) - 1; - span.iEndIndex = span.iStartIndex + 5; // hack - req.Sink.AddError(req.FileName, message, span, Severity.Error); - } catch (System.FormatException) { - continue; - } catch (System.OverflowException) { - continue; - } - } - } - } - } - } - - break; - - case ParseReason.DisplayMemberList: - // Parse the line specified in req.Line for the two - // tokens just before req.Col to obtain the identifier - // and the member connector symbol. - // Examine existing parse tree for members of the identifer - // and return a list of members in your version of the - // Declarations class as stored in the AuthoringScope - // object. - break; - - case ParseReason.MethodTip: - // Parse the line specified in req.Line for the token - // just before req.Col to obtain the name of the method - // being entered. - // Examine the existing parse tree for all method signatures - // with the same name and return a list of those signatures - // in your version of the Methods class as stored in the - // AuthoringScope object. - break; - - case ParseReason.HighlightBraces: - case ParseReason.MemberSelectAndHighlightBraces: - if (source.Braces != null) - { - foreach (TextSpan[] brace in source.Braces) - { - if (brace.Length == 2) - req.Sink.MatchPair(brace[0], brace[1], 1); - else if (brace.Length >= 3) - req.Sink.MatchTriple(brace[0], brace[1], brace[2], 1); - } - } - break; - } - - return new AuthoringScope(source.ParseResult); - } - - private static void AddErrorBecauseOfToolProblems(ParseRequest req, string msg) { - TextSpan span = new TextSpan(); - span.iStartLine = span.iEndLine = 1; - span.iStartIndex = 1; - span.iEndIndex = 2; - req.Sink.AddError(req.FileName, msg, span, Severity.Error); - } - - /// - /// Called to determine if the given location can have a breakpoint applied to it. - /// - /// The IVsTextBuffer object containing the source file. - /// The line number where the breakpoint is to be set. - /// The offset into the line where the breakpoint is to be set. - /// - /// Returns the TextSpan giving the extent of the code affected by the breakpoint if the - /// breakpoint can be set. - /// - /// - /// If successful, returns S_OK; otherwise returns S_FALSE if there is no code at the given - /// position or returns an error code (the validation is deferred until the debug engine is loaded). - /// - /// - /// - /// CAUTION: Even if you do not intend to support the ValidateBreakpointLocation but your language - /// does support breakpoints, you must override the ValidateBreakpointLocation method and return a - /// span that contains the specified line and column; otherwise, breakpoints cannot be set anywhere - /// except line 1. You can return E_NOTIMPL to indicate that you do not otherwise support this - /// method but the span must always be set. The example shows how this can be done. - /// - /// - /// Since the language service parses the code, it generally knows what is considered code and what - /// is not. Normally, the debug engine is loaded and the pending breakpoints are bound to the source. It is at this time the breakpoint location is validated. This method is a fast way to determine if a breakpoint can be set at a particular location without loading the debug engine. - /// - /// - /// You can implement this method to call the ParseSource method with the parse reason of CodeSpan. - /// The parser examines the specified location and returns a span identifying the code at that - /// location. If there is code at the location, the span identifying that code should be passed to - /// your implementation of the CodeSpan method in your version of the AuthoringSink class. Then your - /// implementation of the ValidateBreakpointLocation method retrieves that span from your version of - /// the AuthoringSink class and returns that span in the pCodeSpan argument. - /// - /// - /// The base method returns E_NOTIMPL. - /// - /// - public override int ValidateBreakpointLocation(IVsTextBuffer buffer, int line, int col, TextSpan[] pCodeSpan) - { - // TODO: Add code to not allow breakpoints to be placed on non-code lines. - // TODO: Refactor to allow breakpoint locations to span multiple lines. - if (pCodeSpan != null) - { - pCodeSpan[0].iStartLine = line; - pCodeSpan[0].iStartIndex = col; - pCodeSpan[0].iEndLine = line; - pCodeSpan[0].iEndIndex = col; - if (buffer != null) - { - int length; - buffer.GetLengthOfLine(line, out length); - pCodeSpan[0].iStartIndex = 0; - pCodeSpan[0].iEndIndex = length; - } - return VSConstants.S_OK; - } - else - { - return VSConstants.S_FALSE; - } - } - - public override ViewFilter CreateViewFilter(CodeWindowManager mgr, IVsTextView newView) - { - return new IronyViewFilter(mgr, newView); - } - - public override string Name - { - get { return Configuration.Name; } - } - - public override string GetFormatFilterList() - { - return Configuration.FormatList; - } - } -} +using System; +using System.Collections.Generic; +using System.Diagnostics; +using Microsoft.VisualStudio; +using Microsoft.VisualStudio.TextManager.Interop; +using Microsoft.VisualStudio.Package; + +using Irony.Parsing; +using Irony.Ast; + +using System.IO; + +namespace Demo +{ + public class IronyLanguageService : Microsoft.VisualStudio.Package.LanguageService + { + private Grammar grammar; + private Parser parser; + private ParsingContext context; + + public IronyLanguageService() + { + grammar = new Grammar(); + parser = new Parser(Configuration.Grammar); + context = new ParsingContext(parser); + } + + + #region Custom Colors + public override int GetColorableItem(int index, out IVsColorableItem item) + { + if (index <= Configuration.ColorableItems.Count) + { + item = Configuration.ColorableItems[index - 1]; + return Microsoft.VisualStudio.VSConstants.S_OK; + } + else + { + throw new ArgumentNullException("index"); + } + } + + public override int GetItemCount(out int count) + { + count = Configuration.ColorableItems.Count; + return Microsoft.VisualStudio.VSConstants.S_OK; + } + #endregion + + #region MPF Accessor and Factory specialisation + private LanguagePreferences preferences; + public override LanguagePreferences GetLanguagePreferences() + { + if (this.preferences == null) + { + this.preferences = new LanguagePreferences(this.Site, + typeof(IronyLanguageService).GUID, + this.Name); + this.preferences.Init(); + } + + return this.preferences; + } + + public override Microsoft.VisualStudio.Package.Source CreateSource(IVsTextLines buffer) + { + return new Source(this, buffer, this.GetColorizer(buffer)); + } + + private IScanner scanner; + public override IScanner GetScanner(IVsTextLines buffer) + { + if (scanner == null) + this.scanner = new LineScanner(grammar); + + return this.scanner; + } + #endregion + + public override void OnIdle(bool periodic) + { + // from IronPythonLanguage sample + // this appears to be necessary to get a parse request with ParseReason = Check? + Source src = (Source)GetSource(this.LastActiveTextView); + if (src != null && src.LastParseTime >= Int32.MaxValue >> 12) + { + src.LastParseTime = 0; + } + base.OnIdle(periodic); + } + + public override Microsoft.VisualStudio.Package.AuthoringScope ParseSource(ParseRequest req) + { + Debug.Print("ParseSource at ({0}:{1}), reason {2}", req.Line, req.Col, req.Reason); + Source source = (Source)this.GetSource(req.FileName); + switch (req.Reason) + { + case ParseReason.Check: + // This is where you perform your syntax highlighting. + // Parse entire source as given in req.Text. + // Store results in the AuthoringScope object. + var parsed = parser.Parse(req.Text, req.FileName); + var root = parsed.Root; + if (root != null) { + + AstNode node = (AstNode)root.AstNode; + source.ParseResult = node; + } + + // Used for brace matching. + TokenStack braces = parser.Context.OpenBraces; + foreach (Token brace in braces) { + if (brace.OtherBrace == null) continue; + TextSpan openBrace = new TextSpan(); + openBrace.iStartLine = brace.Location.Line; + openBrace.iStartIndex = brace.Location.Column; + openBrace.iEndLine = brace.Location.Line; + openBrace.iEndIndex = openBrace.iStartIndex + brace.Length; + + TextSpan closeBrace = new TextSpan(); + closeBrace.iStartLine = brace.OtherBrace.Location.Line; + closeBrace.iStartIndex = brace.OtherBrace.Location.Column; + closeBrace.iEndLine = brace.OtherBrace.Location.Line; + closeBrace.iEndIndex = closeBrace.iStartIndex + brace.OtherBrace.Length; + + if (source.Braces == null) { + source.Braces = new List(); + } + source.Braces.Add(new TextSpan[2] { openBrace, closeBrace }); + } + + if (parser.Context.CurrentParseTree.ParserMessages.Count > 0) { + foreach (ParserMessage error in parser.Context.CurrentParseTree.ParserMessages) { + TextSpan span = new TextSpan(); + span.iStartLine = span.iEndLine = error.Location.Line - 1; + span.iStartIndex = error.Location.Column; + span.iEndIndex = error.Location.Position; + req.Sink.AddError(req.FileName, error.Message, span, Severity.Error); + } + } else { // parse looks okay, send it to Boogie. + if (!File.Exists(@"C:\tmp\StartBoogie.bat")) { + AddErrorBecauseOfToolProblems(req, @"Can't find C:\tmp\StartBoogie.bat"); + } else { + + // From: http://dotnetperls.com/process-redirect-standard-output + // (Also, see: http://msdn.microsoft.com/en-us/library/system.diagnostics.processstartinfo.redirectstandardoutput.aspx) + // + // Setup the process with the ProcessStartInfo class. + // + ProcessStartInfo start = new ProcessStartInfo(); + start.FileName = @"cmd.exe"; + start.Arguments = @"/c C:\tmp\StartBoogie.bat"; // Specify exe name. + start.UseShellExecute = false; + start.RedirectStandardInput = true; + start.RedirectStandardOutput = true; + start.CreateNoWindow = true; + //start.WindowStyle = ProcessWindowStyle.Minimized; // need this or else you see the window pop up + // + // Start the process. + // + using (Process process = Process.Start(start)) { + // + // Push the file contents to the new process + // + StreamWriter myStreamWriter = process.StandardInput; + myStreamWriter.WriteLine(req.Text); + myStreamWriter.Close(); + // + // Read in all the text from the process with the StreamReader. + // + using (StreamReader reader = process.StandardOutput) { + //string result = reader.ReadToEnd(); + //Console.Write(result); + + for (string line = reader.ReadLine(); !String.IsNullOrEmpty(line); line = reader.ReadLine()) { + // the lines of interest have the form "filename(line,col): some_error_label: error_message" + // where "some_error_label" is "Error" or "syntax error" or "Error BP5003" or "Related location" + string message; + int n = line.IndexOf("): ", 2); // we start at 2, to avoid problems with "C:\..." + if (n == -1) { + continue; + } else { + int m = line.IndexOf(": ", n + 3); + if (m == -1) { + continue; + } + message = line.Substring(m + 2); + } + line = line.Substring(0, n); // line now has the form "filename(line,col" + + n = line.LastIndexOf(','); + if (n == -1) { continue; } + var colString = line.Substring(n + 1); + line = line.Substring(0, n); // line now has the form "filename(line" + + n = line.LastIndexOf('('); + if (n == -1) { continue; } + var lineString = line.Substring(n + 1); + + try { + TextSpan span = new TextSpan(); + span.iStartLine = span.iEndLine = Int32.Parse(lineString) - 1; + span.iStartIndex = Int32.Parse(colString) - 1; + span.iEndIndex = span.iStartIndex + 5; // hack + req.Sink.AddError(req.FileName, message, span, Severity.Error); + } catch (System.FormatException) { + continue; + } catch (System.OverflowException) { + continue; + } + } + } + } + } + } + + break; + + case ParseReason.DisplayMemberList: + // Parse the line specified in req.Line for the two + // tokens just before req.Col to obtain the identifier + // and the member connector symbol. + // Examine existing parse tree for members of the identifer + // and return a list of members in your version of the + // Declarations class as stored in the AuthoringScope + // object. + break; + + case ParseReason.MethodTip: + // Parse the line specified in req.Line for the token + // just before req.Col to obtain the name of the method + // being entered. + // Examine the existing parse tree for all method signatures + // with the same name and return a list of those signatures + // in your version of the Methods class as stored in the + // AuthoringScope object. + break; + + case ParseReason.HighlightBraces: + case ParseReason.MemberSelectAndHighlightBraces: + if (source.Braces != null) + { + foreach (TextSpan[] brace in source.Braces) + { + if (brace.Length == 2) + req.Sink.MatchPair(brace[0], brace[1], 1); + else if (brace.Length >= 3) + req.Sink.MatchTriple(brace[0], brace[1], brace[2], 1); + } + } + break; + } + + return new AuthoringScope(source.ParseResult); + } + + private static void AddErrorBecauseOfToolProblems(ParseRequest req, string msg) { + TextSpan span = new TextSpan(); + span.iStartLine = span.iEndLine = 1; + span.iStartIndex = 1; + span.iEndIndex = 2; + req.Sink.AddError(req.FileName, msg, span, Severity.Error); + } + + /// + /// Called to determine if the given location can have a breakpoint applied to it. + /// + /// The IVsTextBuffer object containing the source file. + /// The line number where the breakpoint is to be set. + /// The offset into the line where the breakpoint is to be set. + /// + /// Returns the TextSpan giving the extent of the code affected by the breakpoint if the + /// breakpoint can be set. + /// + /// + /// If successful, returns S_OK; otherwise returns S_FALSE if there is no code at the given + /// position or returns an error code (the validation is deferred until the debug engine is loaded). + /// + /// + /// + /// CAUTION: Even if you do not intend to support the ValidateBreakpointLocation but your language + /// does support breakpoints, you must override the ValidateBreakpointLocation method and return a + /// span that contains the specified line and column; otherwise, breakpoints cannot be set anywhere + /// except line 1. You can return E_NOTIMPL to indicate that you do not otherwise support this + /// method but the span must always be set. The example shows how this can be done. + /// + /// + /// Since the language service parses the code, it generally knows what is considered code and what + /// is not. Normally, the debug engine is loaded and the pending breakpoints are bound to the source. It is at this time the breakpoint location is validated. This method is a fast way to determine if a breakpoint can be set at a particular location without loading the debug engine. + /// + /// + /// You can implement this method to call the ParseSource method with the parse reason of CodeSpan. + /// The parser examines the specified location and returns a span identifying the code at that + /// location. If there is code at the location, the span identifying that code should be passed to + /// your implementation of the CodeSpan method in your version of the AuthoringSink class. Then your + /// implementation of the ValidateBreakpointLocation method retrieves that span from your version of + /// the AuthoringSink class and returns that span in the pCodeSpan argument. + /// + /// + /// The base method returns E_NOTIMPL. + /// + /// + public override int ValidateBreakpointLocation(IVsTextBuffer buffer, int line, int col, TextSpan[] pCodeSpan) + { + // TODO: Add code to not allow breakpoints to be placed on non-code lines. + // TODO: Refactor to allow breakpoint locations to span multiple lines. + if (pCodeSpan != null) + { + pCodeSpan[0].iStartLine = line; + pCodeSpan[0].iStartIndex = col; + pCodeSpan[0].iEndLine = line; + pCodeSpan[0].iEndIndex = col; + if (buffer != null) + { + int length; + buffer.GetLengthOfLine(line, out length); + pCodeSpan[0].iStartIndex = 0; + pCodeSpan[0].iEndIndex = length; + } + return VSConstants.S_OK; + } + else + { + return VSConstants.S_FALSE; + } + } + + public override ViewFilter CreateViewFilter(CodeWindowManager mgr, IVsTextView newView) + { + return new IronyViewFilter(mgr, newView); + } + + public override string Name + { + get { return Configuration.Name; } + } + + public override string GetFormatFilterList() + { + return Configuration.FormatList; + } + } +} diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyViewFilter.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyViewFilter.cs index 55c3509e..7c673629 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyViewFilter.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyViewFilter.cs @@ -1,42 +1,42 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.VisualStudio.Package; -using Microsoft.VisualStudio.TextManager.Interop; - -using VsCommands2K = Microsoft.VisualStudio.VSConstants.VSStd2KCmdID; - -namespace Demo -{ - public class IronyViewFilter : ViewFilter - { - public IronyViewFilter(CodeWindowManager mgr, IVsTextView view) - : base(mgr, view) - { - - } - - public override void HandlePostExec(ref Guid guidCmdGroup, uint nCmdId, uint nCmdexecopt, IntPtr pvaIn, IntPtr pvaOut, bool bufferWasChanged) - { - if (guidCmdGroup == typeof(VsCommands2K).GUID) - { - VsCommands2K cmd = (VsCommands2K)nCmdId; - switch (cmd) - { - case VsCommands2K.UP: - case VsCommands2K.UP_EXT: - case VsCommands2K.UP_EXT_COL: - case VsCommands2K.DOWN: - case VsCommands2K.DOWN_EXT: - case VsCommands2K.DOWN_EXT_COL: - Source.OnCommand(TextView, cmd, '\0'); - return; - } - } - - - base.HandlePostExec(ref guidCmdGroup, nCmdId, nCmdexecopt, pvaIn, pvaOut, bufferWasChanged); - } - } -} +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using Microsoft.VisualStudio.Package; +using Microsoft.VisualStudio.TextManager.Interop; + +using VsCommands2K = Microsoft.VisualStudio.VSConstants.VSStd2KCmdID; + +namespace Demo +{ + public class IronyViewFilter : ViewFilter + { + public IronyViewFilter(CodeWindowManager mgr, IVsTextView view) + : base(mgr, view) + { + + } + + public override void HandlePostExec(ref Guid guidCmdGroup, uint nCmdId, uint nCmdexecopt, IntPtr pvaIn, IntPtr pvaOut, bool bufferWasChanged) + { + if (guidCmdGroup == typeof(VsCommands2K).GUID) + { + VsCommands2K cmd = (VsCommands2K)nCmdId; + switch (cmd) + { + case VsCommands2K.UP: + case VsCommands2K.UP_EXT: + case VsCommands2K.UP_EXT_COL: + case VsCommands2K.DOWN: + case VsCommands2K.DOWN_EXT: + case VsCommands2K.DOWN_EXT_COL: + Source.OnCommand(TextView, cmd, '\0'); + return; + } + } + + + base.HandlePostExec(ref guidCmdGroup, nCmdId, nCmdexecopt, pvaIn, pvaOut, bufferWasChanged); + } + } +} diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/LineScanner.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/LineScanner.cs index 966e9c43..b5fdeb8b 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/LineScanner.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/LineScanner.cs @@ -1,58 +1,58 @@ -using System; -using Microsoft.VisualStudio.Package; -using Irony.Parsing; - -namespace Demo -{ - public class LineScanner : IScanner - { - private Parser parser; - - public LineScanner(Grammar grammar) - { - this.parser = new Parser(grammar); - this.parser.Context.Mode = ParseMode.VsLineScan; - } - - public bool ScanTokenAndProvideInfoAboutIt(TokenInfo tokenInfo, ref int state) - { - // Reads each token in a source line and performs syntax coloring. It will continue to - // be called for the source until false is returned. - Token token = parser.Scanner.VsReadToken(ref state); - - // !EOL and !EOF - if (token != null && token.Terminal != Grammar.CurrentGrammar.Eof && token.Category != TokenCategory.Error) - { - tokenInfo.StartIndex = token.Location.Position; - tokenInfo.EndIndex = tokenInfo.StartIndex + token.Length - 1; - if (token.EditorInfo != null) { - tokenInfo.Color = (Microsoft.VisualStudio.Package.TokenColor)token.EditorInfo.Color; - tokenInfo.Type = (Microsoft.VisualStudio.Package.TokenType)token.EditorInfo.Type; - } - - if (token.KeyTerm != null && token.KeyTerm.EditorInfo != null) - { - tokenInfo.Trigger = - (Microsoft.VisualStudio.Package.TokenTriggers)token.KeyTerm.EditorInfo.Triggers; - } - else - { - if (token.EditorInfo != null) { - tokenInfo.Trigger = - (Microsoft.VisualStudio.Package.TokenTriggers)token.EditorInfo.Triggers; - } - } - - return true; - } - - return false; - } - - public void SetSource(string source, int offset) - { - // Stores line of source to be used by ScanTokenAndProvideInfoAboutIt. - parser.Scanner.VsSetSource(source, offset); - } - } -} +using System; +using Microsoft.VisualStudio.Package; +using Irony.Parsing; + +namespace Demo +{ + public class LineScanner : IScanner + { + private Parser parser; + + public LineScanner(Grammar grammar) + { + this.parser = new Parser(grammar); + this.parser.Context.Mode = ParseMode.VsLineScan; + } + + public bool ScanTokenAndProvideInfoAboutIt(TokenInfo tokenInfo, ref int state) + { + // Reads each token in a source line and performs syntax coloring. It will continue to + // be called for the source until false is returned. + Token token = parser.Scanner.VsReadToken(ref state); + + // !EOL and !EOF + if (token != null && token.Terminal != Grammar.CurrentGrammar.Eof && token.Category != TokenCategory.Error) + { + tokenInfo.StartIndex = token.Location.Position; + tokenInfo.EndIndex = tokenInfo.StartIndex + token.Length - 1; + if (token.EditorInfo != null) { + tokenInfo.Color = (Microsoft.VisualStudio.Package.TokenColor)token.EditorInfo.Color; + tokenInfo.Type = (Microsoft.VisualStudio.Package.TokenType)token.EditorInfo.Type; + } + + if (token.KeyTerm != null && token.KeyTerm.EditorInfo != null) + { + tokenInfo.Trigger = + (Microsoft.VisualStudio.Package.TokenTriggers)token.KeyTerm.EditorInfo.Triggers; + } + else + { + if (token.EditorInfo != null) { + tokenInfo.Trigger = + (Microsoft.VisualStudio.Package.TokenTriggers)token.EditorInfo.Triggers; + } + } + + return true; + } + + return false; + } + + public void SetSource(string source, int offset) + { + // Stores line of source to be used by ScanTokenAndProvideInfoAboutIt. + parser.Scanner.VsSetSource(source, offset); + } + } +} diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Method.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Method.cs index c5071612..6b6ba00e 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Method.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Method.cs @@ -1,20 +1,20 @@ -using System; -using System.Collections.Generic; - -namespace Demo -{ - public struct Method - { - public string Name; - public string Description; - public string Type; - public IList Parameters; - } - - public struct Parameter - { - public string Name; - public string Display; - public string Description; - } +using System; +using System.Collections.Generic; + +namespace Demo +{ + public struct Method + { + public string Name; + public string Description; + public string Type; + public IList Parameters; + } + + public struct Parameter + { + public string Name; + public string Display; + public string Description; + } } \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Methods.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Methods.cs index 1d7c124f..7ce0bb2b 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Methods.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Methods.cs @@ -1,50 +1,50 @@ -using System; -using System.Collections.Generic; -using System.Text; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class Methods : Microsoft.VisualStudio.Package.Methods - { - IList methods; - public Methods(IList methods) - { - this.methods = methods; - } - - public override int GetCount() - { - return methods.Count; - } - - public override string GetName(int index) - { - return methods[index].Name; - } - - public override string GetDescription(int index) - { - return methods[index].Description; - } - - public override string GetType(int index) - { - return methods[index].Type; - } - - public override int GetParameterCount(int index) - { - return (methods[index].Parameters == null) ? 0 : methods[index].Parameters.Count; - } - - public override void GetParameterInfo(int index, int paramIndex, out string name, out string display, out string description) - { - Parameter parameter = methods[index].Parameters[paramIndex]; - name = parameter.Name; - display = parameter.Display; - description = parameter.Description; - } - } +using System; +using System.Collections.Generic; +using System.Text; +using Microsoft.VisualStudio.TextManager.Interop; +using Microsoft.VisualStudio.Package; + +namespace Demo +{ + public class Methods : Microsoft.VisualStudio.Package.Methods + { + IList methods; + public Methods(IList methods) + { + this.methods = methods; + } + + public override int GetCount() + { + return methods.Count; + } + + public override string GetName(int index) + { + return methods[index].Name; + } + + public override string GetDescription(int index) + { + return methods[index].Description; + } + + public override string GetType(int index) + { + return methods[index].Type; + } + + public override int GetParameterCount(int index) + { + return (methods[index].Parameters == null) ? 0 : methods[index].Parameters.Count; + } + + public override void GetParameterInfo(int index, int paramIndex, out string name, out string display, out string description) + { + Parameter parameter = methods[index].Parameters[paramIndex]; + name = parameter.Name; + display = parameter.Display; + description = parameter.Description; + } + } } \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Package.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Package.cs index dc1244d6..28762c41 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Package.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Package.cs @@ -1,130 +1,130 @@ -using System; -using System.Collections.Generic; -using System.Text; -using System.Runtime.InteropServices; -using Microsoft.VisualStudio.OLE.Interop; -using MPF = Microsoft.VisualStudio.Package; -using System.ComponentModel.Design; - -namespace Demo -{ - public class IronyPackage : Microsoft.VisualStudio.Shell.Package, IOleComponent - { - uint componentID = 0; - public IronyPackage() - { - ServiceCreatorCallback callback = new ServiceCreatorCallback( - delegate(IServiceContainer container, Type serviceType) - { - if (typeof(IronyLanguageService) == serviceType) - { - IronyLanguageService language = new IronyLanguageService(); - language.SetSite(this); - - // register for idle time callbacks - IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager; - if (componentID == 0 && mgr != null) - { - OLECRINFO[] crinfo = new OLECRINFO[1]; - crinfo[0].cbSize = (uint)Marshal.SizeOf(typeof(OLECRINFO)); - crinfo[0].grfcrf = (uint)_OLECRF.olecrfNeedIdleTime | - (uint)_OLECRF.olecrfNeedPeriodicIdleTime; - crinfo[0].grfcadvf = (uint)_OLECADVF.olecadvfModal | - (uint)_OLECADVF.olecadvfRedrawOff | - (uint)_OLECADVF.olecadvfWarningsOff; - crinfo[0].uIdleTimeInterval = 300; - int hr = mgr.FRegisterComponent(this, crinfo, out componentID); - } - - return language; - } - else - { - return null; - } - }); - - // proffer the LanguageService - (this as IServiceContainer).AddService(typeof(IronyLanguageService), callback, true); - } - - protected override void Dispose(bool disposing) - { - try - { - if (componentID != 0) - { - IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager; - if (mgr != null) - { - mgr.FRevokeComponent(componentID); - } - componentID = 0; - } - } - finally - { - base.Dispose(disposing); - } - } - - #region IOleComponent Members - public int FContinueMessageLoop(uint uReason, IntPtr pvLoopData, MSG[] pMsgPeeked) - { - return 1; - } - - public int FDoIdle(uint grfidlef) - { - IronyLanguageService ls = GetService(typeof(IronyLanguageService)) as IronyLanguageService; - - if (ls != null) - { - ls.OnIdle((grfidlef & (uint)_OLEIDLEF.oleidlefPeriodic) != 0); - } - - return 0; - } - - public int FPreTranslateMessage(MSG[] pMsg) - { - return 0; - } - - public int FQueryTerminate(int fPromptUser) - { - return 1; - } - - public int FReserved1(uint dwReserved, uint message, IntPtr wParam, IntPtr lParam) - { - return 1; - } - - public IntPtr HwndGetWindow(uint dwWhich, uint dwReserved) - { - return IntPtr.Zero; - } - - public void OnActivationChange(IOleComponent pic, int fSameComponent, OLECRINFO[] pcrinfo, int fHostIsActivating, OLECHOSTINFO[] pchostinfo, uint dwReserved) - { - } - - public void OnAppActivate(int fActive, uint dwOtherThreadID) - { - } - - public void OnEnterState(uint uStateID, int fEnter) - { - } - - public void OnLoseActivation() - { - } - - public void Terminate() - { - } - #endregion - } +using System; +using System.Collections.Generic; +using System.Text; +using System.Runtime.InteropServices; +using Microsoft.VisualStudio.OLE.Interop; +using MPF = Microsoft.VisualStudio.Package; +using System.ComponentModel.Design; + +namespace Demo +{ + public class IronyPackage : Microsoft.VisualStudio.Shell.Package, IOleComponent + { + uint componentID = 0; + public IronyPackage() + { + ServiceCreatorCallback callback = new ServiceCreatorCallback( + delegate(IServiceContainer container, Type serviceType) + { + if (typeof(IronyLanguageService) == serviceType) + { + IronyLanguageService language = new IronyLanguageService(); + language.SetSite(this); + + // register for idle time callbacks + IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager; + if (componentID == 0 && mgr != null) + { + OLECRINFO[] crinfo = new OLECRINFO[1]; + crinfo[0].cbSize = (uint)Marshal.SizeOf(typeof(OLECRINFO)); + crinfo[0].grfcrf = (uint)_OLECRF.olecrfNeedIdleTime | + (uint)_OLECRF.olecrfNeedPeriodicIdleTime; + crinfo[0].grfcadvf = (uint)_OLECADVF.olecadvfModal | + (uint)_OLECADVF.olecadvfRedrawOff | + (uint)_OLECADVF.olecadvfWarningsOff; + crinfo[0].uIdleTimeInterval = 300; + int hr = mgr.FRegisterComponent(this, crinfo, out componentID); + } + + return language; + } + else + { + return null; + } + }); + + // proffer the LanguageService + (this as IServiceContainer).AddService(typeof(IronyLanguageService), callback, true); + } + + protected override void Dispose(bool disposing) + { + try + { + if (componentID != 0) + { + IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager; + if (mgr != null) + { + mgr.FRevokeComponent(componentID); + } + componentID = 0; + } + } + finally + { + base.Dispose(disposing); + } + } + + #region IOleComponent Members + public int FContinueMessageLoop(uint uReason, IntPtr pvLoopData, MSG[] pMsgPeeked) + { + return 1; + } + + public int FDoIdle(uint grfidlef) + { + IronyLanguageService ls = GetService(typeof(IronyLanguageService)) as IronyLanguageService; + + if (ls != null) + { + ls.OnIdle((grfidlef & (uint)_OLEIDLEF.oleidlefPeriodic) != 0); + } + + return 0; + } + + public int FPreTranslateMessage(MSG[] pMsg) + { + return 0; + } + + public int FQueryTerminate(int fPromptUser) + { + return 1; + } + + public int FReserved1(uint dwReserved, uint message, IntPtr wParam, IntPtr lParam) + { + return 1; + } + + public IntPtr HwndGetWindow(uint dwWhich, uint dwReserved) + { + return IntPtr.Zero; + } + + public void OnActivationChange(IOleComponent pic, int fSameComponent, OLECRINFO[] pcrinfo, int fHostIsActivating, OLECHOSTINFO[] pchostinfo, uint dwReserved) + { + } + + public void OnAppActivate(int fActive, uint dwOtherThreadID) + { + } + + public void OnEnterState(uint uStateID, int fEnter) + { + } + + public void OnLoseActivation() + { + } + + public void Terminate() + { + } + #endregion + } } \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Resolver.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Resolver.cs index 9f6ddeba..579a8a37 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Resolver.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Resolver.cs @@ -1,50 +1,50 @@ -using System; -using System.Collections.Generic; -using System.Text; -using Irony.Parsing; - -namespace Demo -{ - public class Resolver : Demo.IASTResolver - { - #region IASTResolver Members - - - public IList FindCompletions(object result, int line, int col) - { - // Used for intellisense. - List declarations = new List(); - - // Add keywords defined by grammar - foreach (KeyTerm key in Configuration.Grammar.KeyTerms.Values) - { - if(key.OptionIsSet(TermOptions.IsKeyword)) - { - declarations.Add(new Declaration("", key.Name, 206, key.Name)); - } - } - - declarations.Sort(); - return declarations; - } - - public IList FindMembers(object result, int line, int col) - { - List members = new List(); - - return members; - } - - public string FindQuickInfo(object result, int line, int col) - { - return "unknown"; - } - - public IList FindMethods(object result, int line, int col, string name) - { - return new List(); - } - - #endregion - } -} +using System; +using System.Collections.Generic; +using System.Text; +using Irony.Parsing; + +namespace Demo +{ + public class Resolver : Demo.IASTResolver + { + #region IASTResolver Members + + + public IList FindCompletions(object result, int line, int col) + { + // Used for intellisense. + List declarations = new List(); + + // Add keywords defined by grammar + foreach (KeyTerm key in Configuration.Grammar.KeyTerms.Values) + { + if(key.OptionIsSet(TermOptions.IsKeyword)) + { + declarations.Add(new Declaration("", key.Name, 206, key.Name)); + } + } + + declarations.Sort(); + return declarations; + } + + public IList FindMembers(object result, int line, int col) + { + List members = new List(); + + return members; + } + + public string FindQuickInfo(object result, int line, int col) + { + return "unknown"; + } + + public IList FindMethods(object result, int line, int col, string name) + { + return new List(); + } + + #endregion + } +} diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Source.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Source.cs index 418bec01..92b5a884 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Source.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Source.cs @@ -1,41 +1,41 @@ -/*************************************************************************** - -Copyright (c) Microsoft Corporation. All rights reserved. -This code is licensed under the Visual Studio SDK license terms. -THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF -ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY -IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR -PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT. - -***************************************************************************/ - -using System; -using System.Collections.Generic; -using System.Text; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class Source : Microsoft.VisualStudio.Package.Source - { - public Source(LanguageService service, IVsTextLines textLines, Colorizer colorizer) - : base(service, textLines, colorizer) - { - } - - private object parseResult; - public object ParseResult - { - get { return parseResult; } - set { parseResult = value; } - } - - private IList braces; - public IList Braces - { - get { return braces; } - set { braces = value; } - } - } +/*************************************************************************** + +Copyright (c) Microsoft Corporation. All rights reserved. +This code is licensed under the Visual Studio SDK license terms. +THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF +ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY +IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR +PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT. + +***************************************************************************/ + +using System; +using System.Collections.Generic; +using System.Text; +using Microsoft.VisualStudio.TextManager.Interop; +using Microsoft.VisualStudio.Package; + +namespace Demo +{ + public class Source : Microsoft.VisualStudio.Package.Source + { + public Source(LanguageService service, IVsTextLines textLines, Colorizer colorizer) + : base(service, textLines, colorizer) + { + } + + private object parseResult; + public object ParseResult + { + get { return parseResult; } + set { parseResult = value; } + } + + private IList braces; + public IList Braces + { + get { return braces; } + set { braces = value; } + } + } } \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/IronyLanguageServicePackage.cs b/Util/VS2010/Boogie/BoogieLanguageService/IronyLanguageServicePackage.cs index 411207c7..0b5ed7a2 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/IronyLanguageServicePackage.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/IronyLanguageServicePackage.cs @@ -1,90 +1,90 @@ -// VsPkg.cs : Implementation of IronyLanguageService -// - -using System; -using System.Diagnostics; -using System.Globalization; -using System.Runtime.InteropServices; -using System.ComponentModel.Design; -using Microsoft.Win32; -using Microsoft.VisualStudio.Shell.Interop; -using Microsoft.VisualStudio.OLE.Interop; -using Microsoft.VisualStudio.Shell; - -namespace Demo -{ - /// - /// This is the class that implements the package exposed by this assembly. - /// - /// The minimum requirement for a class to be considered a valid package for Visual Studio - /// is to implement the IVsPackage interface and register itself with the shell. - /// This package uses the helper classes defined inside the Managed Package Framework (MPF) - /// to do it: it derives from the Package class that provides the implementation of the - /// IVsPackage interface and uses the registration attributes defined in the framework to - /// register itself and its components with the shell. - /// - // This attribute tells the registration utility (regpkg.exe) that this class needs - // to be registered as package. - [PackageRegistration(UseManagedResourcesOnly = true)] - // A Visual Studio component can be registered under different regitry roots; for instance - // when you debug your package you want to register it in the experimental hive. This - // attribute specifies the registry root to use if no one is provided to regpkg.exe with - // the /root switch. - [DefaultRegistryRoot("Software\\Microsoft\\VisualStudio\\10.0Exp")] - // This attribute is used to register the informations needed to show the this package - // in the Help/About dialog of Visual Studio. - [InstalledProductRegistration(/*false,*/ "#110", "#112", "1.0", IconResourceID = 400)] - // This attribute will make your language service accessible by other packages installed. - [ProvideService(typeof(IronyLanguageService))] - // This attribute(s) associates file extensions with your language service. - [ProvideLanguageExtension(typeof(IronyLanguageService), ".bpl")] - - // This attributes informs Visual Studio that this package provides a langauge service and - // which features are implemented. - [ProvideLanguageService(typeof(IronyLanguageService), Configuration.Name, 0, - CodeSense = true, - EnableCommenting = true, - MatchBraces = true, - MatchBracesAtCaret = true, - ShowMatchingBrace = true, - AutoOutlining = true)] - // In order be loaded inside Visual Studio in a machine that has not the VS SDK installed, - // package needs to have a valid load key (it can be requested at - // http://msdn.microsoft.com/vstudio/extend/). This attributes tells the shell that this - // package has a load key embedded in its resources. - [ProvideLoadKey("Standard", "1.0", "Boogie", "Demo", 104)] - [Guid(GuidList.guidIronyLanguageServicePkgString)] - public sealed class BoogieLanguageService : IronyPackage - { - /// - /// Default constructor of the package. - /// Inside this method you can place any initialization code that does not require - /// any Visual Studio service because at this point the package object is created but - /// not sited yet inside Visual Studio environment. The place to do all the other - /// initialization is the Initialize method. - /// - public BoogieLanguageService() - { - Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering constructor for: {0}", this.ToString())); - } - - - - ///////////////////////////////////////////////////////////////////////////// - // Overriden Package Implementation - #region Package Members - - /// - /// Initialization of the package; this method is called right after the package is sited, so this is the place - /// where you can put all the initilaization code that rely on services provided by VisualStudio. - /// - protected override void Initialize() - { - Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering Initialize() of: {0}", this.ToString())); - base.Initialize(); - - } - #endregion - - } -} +// VsPkg.cs : Implementation of IronyLanguageService +// + +using System; +using System.Diagnostics; +using System.Globalization; +using System.Runtime.InteropServices; +using System.ComponentModel.Design; +using Microsoft.Win32; +using Microsoft.VisualStudio.Shell.Interop; +using Microsoft.VisualStudio.OLE.Interop; +using Microsoft.VisualStudio.Shell; + +namespace Demo +{ + /// + /// This is the class that implements the package exposed by this assembly. + /// + /// The minimum requirement for a class to be considered a valid package for Visual Studio + /// is to implement the IVsPackage interface and register itself with the shell. + /// This package uses the helper classes defined inside the Managed Package Framework (MPF) + /// to do it: it derives from the Package class that provides the implementation of the + /// IVsPackage interface and uses the registration attributes defined in the framework to + /// register itself and its components with the shell. + /// + // This attribute tells the registration utility (regpkg.exe) that this class needs + // to be registered as package. + [PackageRegistration(UseManagedResourcesOnly = true)] + // A Visual Studio component can be registered under different regitry roots; for instance + // when you debug your package you want to register it in the experimental hive. This + // attribute specifies the registry root to use if no one is provided to regpkg.exe with + // the /root switch. + [DefaultRegistryRoot("Software\\Microsoft\\VisualStudio\\10.0Exp")] + // This attribute is used to register the informations needed to show the this package + // in the Help/About dialog of Visual Studio. + [InstalledProductRegistration(/*false,*/ "#110", "#112", "1.0", IconResourceID = 400)] + // This attribute will make your language service accessible by other packages installed. + [ProvideService(typeof(IronyLanguageService))] + // This attribute(s) associates file extensions with your language service. + [ProvideLanguageExtension(typeof(IronyLanguageService), ".bpl")] + + // This attributes informs Visual Studio that this package provides a langauge service and + // which features are implemented. + [ProvideLanguageService(typeof(IronyLanguageService), Configuration.Name, 0, + CodeSense = true, + EnableCommenting = true, + MatchBraces = true, + MatchBracesAtCaret = true, + ShowMatchingBrace = true, + AutoOutlining = true)] + // In order be loaded inside Visual Studio in a machine that has not the VS SDK installed, + // package needs to have a valid load key (it can be requested at + // http://msdn.microsoft.com/vstudio/extend/). This attributes tells the shell that this + // package has a load key embedded in its resources. + [ProvideLoadKey("Standard", "1.0", "Boogie", "Demo", 104)] + [Guid(GuidList.guidIronyLanguageServicePkgString)] + public sealed class BoogieLanguageService : IronyPackage + { + /// + /// Default constructor of the package. + /// Inside this method you can place any initialization code that does not require + /// any Visual Studio service because at this point the package object is created but + /// not sited yet inside Visual Studio environment. The place to do all the other + /// initialization is the Initialize method. + /// + public BoogieLanguageService() + { + Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering constructor for: {0}", this.ToString())); + } + + + + ///////////////////////////////////////////////////////////////////////////// + // Overriden Package Implementation + #region Package Members + + /// + /// Initialization of the package; this method is called right after the package is sited, so this is the place + /// where you can put all the initilaization code that rely on services provided by VisualStudio. + /// + protected override void Initialize() + { + Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering Initialize() of: {0}", this.ToString())); + base.Initialize(); + + } + #endregion + + } +} diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Properties/AssemblyInfo.cs b/Util/VS2010/Boogie/BoogieLanguageService/Properties/AssemblyInfo.cs index 118d4488..6848b03a 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Properties/AssemblyInfo.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Properties/AssemblyInfo.cs @@ -1,36 +1,36 @@ -using System; -using System.Reflection; -using System.Resources; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("Package Name")] -[assembly: AssemblyDescription("")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("Company")] -[assembly: AssemblyProduct("Package Name")] -[assembly: AssemblyCopyright("")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] -[assembly: ComVisible(false)] -[assembly: CLSCompliant(false)] -[assembly: NeutralResourcesLanguage("en-US")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Revision and Build Numbers -// by using the '*' as shown below: - -[assembly: AssemblyVersion("1.0.0.0")] -[assembly: AssemblyFileVersion("1.0.0.0")] - - - +using System; +using System.Reflection; +using System.Resources; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("Package Name")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("Company")] +[assembly: AssemblyProduct("Package Name")] +[assembly: AssemblyCopyright("")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] +[assembly: ComVisible(false)] +[assembly: CLSCompliant(false)] +[assembly: NeutralResourcesLanguage("en-US")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Revision and Build Numbers +// by using the '*' as shown below: + +[assembly: AssemblyVersion("1.0.0.0")] +[assembly: AssemblyFileVersion("1.0.0.0")] + + + diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Resources.Designer.cs b/Util/VS2010/Boogie/BoogieLanguageService/Resources.Designer.cs index 1b30575c..98bd9301 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Resources.Designer.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Resources.Designer.cs @@ -1,63 +1,63 @@ -//------------------------------------------------------------------------------ -// -// This code was generated by a tool. -// Runtime Version:4.0.21006.1 -// -// Changes to this file may cause incorrect behavior and will be lost if -// the code is regenerated. -// -//------------------------------------------------------------------------------ - -namespace Demo { - using System; - - - /// - /// A strongly-typed resource class, for looking up localized strings, etc. - /// - // This class was auto-generated by the StronglyTypedResourceBuilder - // class via a tool like ResGen or Visual Studio. - // To add or remove a member, edit your .ResX file then rerun ResGen - // with the /str option, or rebuild your VS project. - [global::System.CodeDom.Compiler.GeneratedCodeAttribute("System.Resources.Tools.StronglyTypedResourceBuilder", "4.0.0.0")] - [global::System.Diagnostics.DebuggerNonUserCodeAttribute()] - [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()] - internal class Resources { - - private static global::System.Resources.ResourceManager resourceMan; - - private static global::System.Globalization.CultureInfo resourceCulture; - - [global::System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1811:AvoidUncalledPrivateCode")] - internal Resources() { - } - - /// - /// Returns the cached ResourceManager instance used by this class. - /// - [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)] - internal static global::System.Resources.ResourceManager ResourceManager { - get { - if (object.ReferenceEquals(resourceMan, null)) { - global::System.Resources.ResourceManager temp = new global::System.Resources.ResourceManager("Demo.BoogieLanguageService.Resources", typeof(Resources).Assembly); - resourceMan = temp; - } - return resourceMan; - } - } - - /// - /// Overrides the current thread's CurrentUICulture property for all - /// resource lookups using this strongly typed resource class. - /// - [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)] - internal static global::System.Globalization.CultureInfo Culture { - get { - return resourceCulture; - } - set { - resourceCulture = value; - } - } - } -} +//------------------------------------------------------------------------------ +// +// This code was generated by a tool. +// Runtime Version:4.0.21006.1 +// +// Changes to this file may cause incorrect behavior and will be lost if +// the code is regenerated. +// +//------------------------------------------------------------------------------ + +namespace Demo { + using System; + + + /// + /// A strongly-typed resource class, for looking up localized strings, etc. + /// + // This class was auto-generated by the StronglyTypedResourceBuilder + // class via a tool like ResGen or Visual Studio. + // To add or remove a member, edit your .ResX file then rerun ResGen + // with the /str option, or rebuild your VS project. + [global::System.CodeDom.Compiler.GeneratedCodeAttribute("System.Resources.Tools.StronglyTypedResourceBuilder", "4.0.0.0")] + [global::System.Diagnostics.DebuggerNonUserCodeAttribute()] + [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()] + internal class Resources { + + private static global::System.Resources.ResourceManager resourceMan; + + private static global::System.Globalization.CultureInfo resourceCulture; + + [global::System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1811:AvoidUncalledPrivateCode")] + internal Resources() { + } + + /// + /// Returns the cached ResourceManager instance used by this class. + /// + [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)] + internal static global::System.Resources.ResourceManager ResourceManager { + get { + if (object.ReferenceEquals(resourceMan, null)) { + global::System.Resources.ResourceManager temp = new global::System.Resources.ResourceManager("Demo.BoogieLanguageService.Resources", typeof(Resources).Assembly); + resourceMan = temp; + } + return resourceMan; + } + } + + /// + /// Overrides the current thread's CurrentUICulture property for all + /// resource lookups using this strongly typed resource class. + /// + [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)] + internal static global::System.Globalization.CultureInfo Culture { + get { + return resourceCulture; + } + set { + resourceCulture = value; + } + } + } +} diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Resources.resx b/Util/VS2010/Boogie/BoogieLanguageService/Resources.resx index 03fef612..7ad9af7a 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Resources.resx +++ b/Util/VS2010/Boogie/BoogieLanguageService/Resources.resx @@ -1,130 +1,130 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - text/microsoft-resx - - - 2.0 - - - System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + text/microsoft-resx + + + 2.0 + + + System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 + + + System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 + + \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/VSPackage.resx b/Util/VS2010/Boogie/BoogieLanguageService/VSPackage.resx index 17dae8cb..fb95a654 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/VSPackage.resx +++ b/Util/VS2010/Boogie/BoogieLanguageService/VSPackage.resx @@ -1,129 +1,129 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - text/microsoft-resx - - - 2.0 - - - System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - Paste PLK Here - - - Boogie - - - Microsoft Research Boogie, intermediate verification language - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + text/microsoft-resx + + + 2.0 + + + System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 + + + System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 + + + Paste PLK Here + + + Boogie + + + Microsoft Research Boogie, intermediate verification language + \ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/source.extension.vsixmanifest b/Util/VS2010/Boogie/BoogieLanguageService/source.extension.vsixmanifest index a6528172..4a64ecc2 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/source.extension.vsixmanifest +++ b/Util/VS2010/Boogie/BoogieLanguageService/source.extension.vsixmanifest @@ -1,27 +1,27 @@ - - - - - BoogieService - Microsoft Research - 1.0 - Information about my package - 1033 - - - - Pro - VST_All - - - - - - - - - - BoogieService.pkgdef - - - + + + + + BoogieService + Microsoft Research + 1.0 + Information about my package + 1033 + + + + Pro + VST_All + + + + + + + + + + BoogieService.pkgdef + + + diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty index e67c61f4..65fa7fb1 100644 --- a/Util/latex/boogie.sty +++ b/Util/latex/boogie.sty @@ -1,121 +1,121 @@ -% boogie.sty -% Boogie mode for the LaTeX listings package. -% Rustan Leino, 30 May 2008. -% Example: -% \begin{boogie} -% type Field \alpha; -% var Heap: <<\alpha>>[ref, Field \alpha]\alpha where IsHeap(Heap); -% function IsHeap(<<\alpha>>[ref, Field \alpha]\alpha) returns (bool); -% procedure Inc(x: int) returns (y: int) -% modifies Heap; -% { -% havoc Heap; -% if (0 <= x && x < 100) { -% y := x + 1; -% } -% } -% \end{boogie} - -\usepackage{listings} - -\lstdefinelanguage{boogie}{ - 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,% - bv30,bv31,bv32,bv33,bv34,bv35,bv36,bv37,bv38,bv39,% - bv40,bv41,bv42,bv43,bv44,bv45,bv46,bv47,bv48,bv49,% - bv50,bv51,bv52,bv53,bv54,bv55,bv56,bv57,bv58,bv59,% - bv60,bv61,bv62,bv63,bv64,% ... - const,unique,complete,partition, - axiom, - function,returns, - var,where, - procedure,implementation, - requires,modifies,ensures,free, - % expressions - false,true,null,old,then,div,mod, - % statements - assert,assume,havoc,call,if,else,while,invariant,break,return,goto, - }, - literate=% - {:}{$\colon$}1 - {::}{$\bullet$}2 - {:=}{$:$$=$}2 - {!}{$\lnot$}1 - {==}{$=$}1 - {!=}{$\neq$}1 - {&&}{$\land$}1 - {||}{$\lor$}1 - {<=}{$\le$}1 - {>=}{$\ge$}1 - {==>}{$\Longrightarrow$}3 - {<==>}{$\Longleftrightarrow$}4 - {forall}{$\forall$}1 - {exists}{$\exists$}1 - {lambda}{$\lambda$}1 - % the following isn't actually Boogie, but it gives the option to produce nicer latex - {<<}{$\langle$}1 - {>>}{$\rangle$}1 - {\\alpha}{$\alpha$}1 - {\\beta}{$\beta$}1 - {\\gamma}{$\gamma$}1 - {\\delta}{$\delta$}1 - {\\epsilon}{$\epsilon$}1 - {\\zeta}{$\zeta$}1 - {\\eta}{$\eta$}1 - {\\theta}{$\theta$}1 - {\\iota}{$\iota$}1 - {\\kappa}{$\kappa$}1 - {\\lambda}{$\lambda$}1 - {\\mu}{$\mu$}1 - {\\nu}{$\nu$}1 - {\\xi}{$\xi$}1 - {\\pi}{$\pi$}1 - {\\rho}{$\rho$}1 - {\\sigma}{$\sigma$}1 - {\\tau}{$\tau$}1 - {\\upsilon}{$\upsilon$}1 - {\\phi}{$\phi$}1 - {\\chi}{$\chi$}1 - {\\psi}{$\psi$}1 - {\\omega}{$\omega$}1 - {\\Gamma}{$\Gamma$}1 - {\\Delta}{$\Delta$}1 - {\\Theta}{$\Theta$}1 - {\\Lambda}{$\Lambda$}1 - {\\Xi}{$\Xi$}1 - {\\Pi}{$\Pi$}1 - {\\Sigma}{$\Sigma$}1 - {\\Upsilon}{$\Upsilon$}1 - {\\Phi}{$\Phi$}1 - {\\Psi}{$\Psi$}1 - {\\Omega}{$\Omega$}1 - , - sensitive=true, % case sensitive - morecomment=[l]{//}, - morecomment=[s]{/*}{*/}, - morestring=[b]", - numbers=none, - firstnumber=0, - numberstyle=\tiny, - stepnumber=5, - basicstyle=\scriptsize\sffamily, - commentstyle=\itshape, - keywordstyle=\bfseries, - ndkeywordstyle=\bfseries, -} -\lstnewenvironment{boogie}[1][]{% - \lstset{language=boogie, - floatplacement={tbp},captionpos=b, - frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{} -\lstnewenvironment{boogieNoLines}[1][]{% - \lstset{language=boogie, - floatplacement={tbp},captionpos=b, - xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{} -\def\inlineboogie{% - \lstinline[language=boogie,basicstyle=\ttfamily,columns=fixed]} -\newcommand{\lstfile}[1]{ - \lstinputlisting[language=boogie,% - frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1} -} +% boogie.sty +% Boogie mode for the LaTeX listings package. +% Rustan Leino, 30 May 2008. +% Example: +% \begin{boogie} +% type Field \alpha; +% var Heap: <<\alpha>>[ref, Field \alpha]\alpha where IsHeap(Heap); +% function IsHeap(<<\alpha>>[ref, Field \alpha]\alpha) returns (bool); +% procedure Inc(x: int) returns (y: int) +% modifies Heap; +% { +% havoc Heap; +% if (0 <= x && x < 100) { +% y := x + 1; +% } +% } +% \end{boogie} + +\usepackage{listings} + +\lstdefinelanguage{boogie}{ + 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,% + bv30,bv31,bv32,bv33,bv34,bv35,bv36,bv37,bv38,bv39,% + bv40,bv41,bv42,bv43,bv44,bv45,bv46,bv47,bv48,bv49,% + bv50,bv51,bv52,bv53,bv54,bv55,bv56,bv57,bv58,bv59,% + bv60,bv61,bv62,bv63,bv64,% ... + const,unique,complete,partition, + axiom, + function,returns, + var,where, + procedure,implementation, + requires,modifies,ensures,free, + % expressions + false,true,null,old,then,div,mod, + % statements + assert,assume,havoc,call,if,else,while,invariant,break,return,goto, + }, + literate=% + {:}{$\colon$}1 + {::}{$\bullet$}2 + {:=}{$:$$=$}2 + {!}{$\lnot$}1 + {==}{$=$}1 + {!=}{$\neq$}1 + {&&}{$\land$}1 + {||}{$\lor$}1 + {<=}{$\le$}1 + {>=}{$\ge$}1 + {==>}{$\Longrightarrow$}3 + {<==>}{$\Longleftrightarrow$}4 + {forall}{$\forall$}1 + {exists}{$\exists$}1 + {lambda}{$\lambda$}1 + % the following isn't actually Boogie, but it gives the option to produce nicer latex + {<<}{$\langle$}1 + {>>}{$\rangle$}1 + {\\alpha}{$\alpha$}1 + {\\beta}{$\beta$}1 + {\\gamma}{$\gamma$}1 + {\\delta}{$\delta$}1 + {\\epsilon}{$\epsilon$}1 + {\\zeta}{$\zeta$}1 + {\\eta}{$\eta$}1 + {\\theta}{$\theta$}1 + {\\iota}{$\iota$}1 + {\\kappa}{$\kappa$}1 + {\\lambda}{$\lambda$}1 + {\\mu}{$\mu$}1 + {\\nu}{$\nu$}1 + {\\xi}{$\xi$}1 + {\\pi}{$\pi$}1 + {\\rho}{$\rho$}1 + {\\sigma}{$\sigma$}1 + {\\tau}{$\tau$}1 + {\\upsilon}{$\upsilon$}1 + {\\phi}{$\phi$}1 + {\\chi}{$\chi$}1 + {\\psi}{$\psi$}1 + {\\omega}{$\omega$}1 + {\\Gamma}{$\Gamma$}1 + {\\Delta}{$\Delta$}1 + {\\Theta}{$\Theta$}1 + {\\Lambda}{$\Lambda$}1 + {\\Xi}{$\Xi$}1 + {\\Pi}{$\Pi$}1 + {\\Sigma}{$\Sigma$}1 + {\\Upsilon}{$\Upsilon$}1 + {\\Phi}{$\Phi$}1 + {\\Psi}{$\Psi$}1 + {\\Omega}{$\Omega$}1 + , + sensitive=true, % case sensitive + morecomment=[l]{//}, + morecomment=[s]{/*}{*/}, + morestring=[b]", + numbers=none, + firstnumber=0, + numberstyle=\tiny, + stepnumber=5, + basicstyle=\scriptsize\sffamily, + commentstyle=\itshape, + keywordstyle=\bfseries, + ndkeywordstyle=\bfseries, +} +\lstnewenvironment{boogie}[1][]{% + \lstset{language=boogie, + floatplacement={tbp},captionpos=b, + frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{} +\lstnewenvironment{boogieNoLines}[1][]{% + \lstset{language=boogie, + floatplacement={tbp},captionpos=b, + xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{} +\def\inlineboogie{% + \lstinline[language=boogie,basicstyle=\ttfamily,columns=fixed]} +\newcommand{\lstfile}[1]{ + \lstinputlisting[language=boogie,% + frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1} +} -- cgit v1.2.3