diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
| commit | 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d (patch) | |
| tree | 27d5f9b0d130c6c1a6758bc0b7456b0aa51e34e0 /Util | |
| parent | e11d65009d0b4ba1327f5f5dd6b26367330611f0 (diff) | |
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.
Diffstat (limited to 'Util')
35 files changed, 2602 insertions, 2602 deletions
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 @@ -<?xml version="1.0" encoding="utf-8"?>
-<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet">
- <CodeSnippet Format="1.0.0">
- <Header>
- <SnippetTypes>
- <SnippetType>Expansion</SnippetType>
- </SnippetTypes>
- <Title>Contract.Assert(...!=null)</Title>
- <Shortcut>can</Shortcut>
- <Description>Emits a 'Contract.Assert' non-null clause</Description>
- <Author>tabarbe</Author>
- </Header>
- <Snippet>
- <Imports>
- <Import>
- <Namespace>System.Diagnostics.Contracts</Namespace>
- </Import>
- </Imports>
- <Declarations>
- <Object Editable="true">
- <ID>condition</ID>
- <ToolTip>condition that must not be null</ToolTip>
- <Default>arg</Default>
- <Function>
- </Function>
- </Object>
- </Declarations>
- <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Assert($condition$ != null);$end$]]></Code>
- </Snippet>
- </CodeSnippet>
-</CodeSnippets>
+<?xml version="1.0" encoding="utf-8"?> +<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet"> + <CodeSnippet Format="1.0.0"> + <Header> + <SnippetTypes> + <SnippetType>Expansion</SnippetType> + </SnippetTypes> + <Title>Contract.Assert(...!=null)</Title> + <Shortcut>can</Shortcut> + <Description>Emits a 'Contract.Assert' non-null clause</Description> + <Author>tabarbe</Author> + </Header> + <Snippet> + <Imports> + <Import> + <Namespace>System.Diagnostics.Contracts</Namespace> + </Import> + </Imports> + <Declarations> + <Object Editable="true"> + <ID>condition</ID> + <ToolTip>condition that must not be null</ToolTip> + <Default>arg</Default> + <Function> + </Function> + </Object> + </Declarations> + <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Assert($condition$ != null);$end$]]></Code> + </Snippet> + </CodeSnippet> +</CodeSnippets> 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 @@ -<?xml version="1.0" encoding="utf-8"?>
-<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet">
- <CodeSnippet Format="1.0.0">
- <Header>
- <SnippetTypes>
- <SnippetType>Expansion</SnippetType>
- </SnippetTypes>
- <Title>Contract.Assert(cce.NonNullElements(...))</Title>
- <Shortcut>cann</Shortcut>
- <Description>Emits a 'Contract.Assert' non-null elements clause</Description>
- <Author>tabarbe</Author>
- </Header>
- <Snippet>
- <Imports>
- <Import>
- <Namespace>System.Diagnostics.Contracts</Namespace>
- </Import>
- </Imports>
- <Declarations>
- <Object Editable="true">
- <ID>collection</ID>
- <ToolTip>collection whose elements must not be null</ToolTip>
- <Default>arg</Default>
- <Function>
- </Function>
- </Object>
- </Declarations>
- <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Assert(cce.NonNullElements($collection$));$end$]]></Code>
- </Snippet>
- </CodeSnippet>
-</CodeSnippets>
+<?xml version="1.0" encoding="utf-8"?> +<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet"> + <CodeSnippet Format="1.0.0"> + <Header> + <SnippetTypes> + <SnippetType>Expansion</SnippetType> + </SnippetTypes> + <Title>Contract.Assert(cce.NonNullElements(...))</Title> + <Shortcut>cann</Shortcut> + <Description>Emits a 'Contract.Assert' non-null elements clause</Description> + <Author>tabarbe</Author> + </Header> + <Snippet> + <Imports> + <Import> + <Namespace>System.Diagnostics.Contracts</Namespace> + </Import> + </Imports> + <Declarations> + <Object Editable="true"> + <ID>collection</ID> + <ToolTip>collection whose elements must not be null</ToolTip> + <Default>arg</Default> + <Function> + </Function> + </Object> + </Declarations> + <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Assert(cce.NonNullElements($collection$));$end$]]></Code> + </Snippet> + </CodeSnippet> +</CodeSnippets> 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 @@ -<?xml version="1.0" encoding="utf-8"?>
-<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet">
- <CodeSnippet Format="1.0.0">
- <Header>
- <SnippetTypes>
- <SnippetType>Expansion</SnippetType>
- </SnippetTypes>
- <Title>Contract.Ensures(cce.NonNullElements(Contract.Result<...>()))</Title>
- <Shortcut>cenn</Shortcut>
- <Description>Emits a 'Contract.Ensures' non-null elements clause</Description>
- <Author>tabarbe</Author>
- </Header>
- <Snippet>
- <Imports>
- <Import>
- <Namespace>System.Diagnostics.Contracts</Namespace>
- </Import>
- </Imports>
- <Declarations>
- <Object Editable="true">
- <ID>collection</ID>
- <ToolTip>Collection whose elements must not be null</ToolTip>
- <Default>List<string></Default>
- <Function>
- </Function>
- </Object>
- </Declarations>
- <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Ensures(cce.NonNullElements(Contract.Result<$collection$>()));$end$]]></Code>
- </Snippet>
- </CodeSnippet>
+<?xml version="1.0" encoding="utf-8"?> +<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet"> + <CodeSnippet Format="1.0.0"> + <Header> + <SnippetTypes> + <SnippetType>Expansion</SnippetType> + </SnippetTypes> + <Title>Contract.Ensures(cce.NonNullElements(Contract.Result<...>()))</Title> + <Shortcut>cenn</Shortcut> + <Description>Emits a 'Contract.Ensures' non-null elements clause</Description> + <Author>tabarbe</Author> + </Header> + <Snippet> + <Imports> + <Import> + <Namespace>System.Diagnostics.Contracts</Namespace> + </Import> + </Imports> + <Declarations> + <Object Editable="true"> + <ID>collection</ID> + <ToolTip>Collection whose elements must not be null</ToolTip> + <Default>List<string></Default> + <Function> + </Function> + </Object> + </Declarations> + <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Ensures(cce.NonNullElements(Contract.Result<$collection$>()));$end$]]></Code> + </Snippet> + </CodeSnippet> </CodeSnippets>
\ 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 @@ -<?xml version="1.0" encoding="utf-8"?>
-<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet">
- <CodeSnippet Format="1.0.0">
- <Header>
- <SnippetTypes>
- <SnippetType>Expansion</SnippetType>
- </SnippetTypes>
- <Title>Contract.Ensures(Contract.ValueAtReturn(...)!=null)</Title>
- <Shortcut>cern</Shortcut>
- <Description>Emits a 'Contract.Ensures' non-null out or ref parameter clause</Description>
- <Author>tabarbe</Author>
- </Header>
- <Snippet>
- <Imports>
- <Import>
- <Namespace>System.Diagnostics.Contracts</Namespace>
- </Import>
- </Imports>
- <Declarations>
- <Object Editable="true">
- <ID>value</ID>
- <ToolTip>Value that must not be null</ToolTip>
- <Default>arg</Default>
- <Function>
- </Function>
- </Object>
- </Declarations>
- <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Ensures(Contract.ValueAtReturn(out $value$)!=null);$end$]]></Code>
- </Snippet>
- </CodeSnippet>
+<?xml version="1.0" encoding="utf-8"?> +<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet"> + <CodeSnippet Format="1.0.0"> + <Header> + <SnippetTypes> + <SnippetType>Expansion</SnippetType> + </SnippetTypes> + <Title>Contract.Ensures(Contract.ValueAtReturn(...)!=null)</Title> + <Shortcut>cern</Shortcut> + <Description>Emits a 'Contract.Ensures' non-null out or ref parameter clause</Description> + <Author>tabarbe</Author> + </Header> + <Snippet> + <Imports> + <Import> + <Namespace>System.Diagnostics.Contracts</Namespace> + </Import> + </Imports> + <Declarations> + <Object Editable="true"> + <ID>value</ID> + <ToolTip>Value that must not be null</ToolTip> + <Default>arg</Default> + <Function> + </Function> + </Object> + </Declarations> + <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Ensures(Contract.ValueAtReturn(out $value$)!=null);$end$]]></Code> + </Snippet> + </CodeSnippet> </CodeSnippets>
\ 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 @@ -<?xml version="1.0" encoding="utf-8"?>
-<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet">
- <CodeSnippet Format="1.0.0">
- <Header>
- <SnippetTypes>
- <SnippetType>Expansion</SnippetType>
- </SnippetTypes>
- <Title>Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(...)))</Title>
- <Shortcut>cernn</Shortcut>
- <Description>Emits a 'Contract.Ensures' cce.non-nullelements out parameter clause</Description>
- <Author>tabarbe</Author>
- </Header>
- <Snippet>
- <Imports>
- <Import>
- <Namespace>System.Diagnostics.Contracts</Namespace>
- </Import>
- </Imports>
- <Declarations>
- <Object Editable="true">
- <ID>value</ID>
- <ToolTip>Value that must not be null</ToolTip>
- <Default>arg</Default>
- <Function>
- </Function>
- </Object>
- </Declarations>
- <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out $value$)));$end$]]></Code>
- </Snippet>
- </CodeSnippet>
+<?xml version="1.0" encoding="utf-8"?> +<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet"> + <CodeSnippet Format="1.0.0"> + <Header> + <SnippetTypes> + <SnippetType>Expansion</SnippetType> + </SnippetTypes> + <Title>Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(...)))</Title> + <Shortcut>cernn</Shortcut> + <Description>Emits a 'Contract.Ensures' cce.non-nullelements out parameter clause</Description> + <Author>tabarbe</Author> + </Header> + <Snippet> + <Imports> + <Import> + <Namespace>System.Diagnostics.Contracts</Namespace> + </Import> + </Imports> + <Declarations> + <Object Editable="true"> + <ID>value</ID> + <ToolTip>Value that must not be null</ToolTip> + <Default>arg</Default> + <Function> + </Function> + </Object> + </Declarations> + <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out $value$)));$end$]]></Code> + </Snippet> + </CodeSnippet> </CodeSnippets>
\ 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 @@ -<?xml version="1.0" encoding="utf-8"?>
-<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet">
- <CodeSnippet Format="1.0.0">
- <Header>
- <SnippetTypes>
- <SnippetType>Expansion</SnippetType>
- </SnippetTypes>
- <Title>Contract.Invariant(cce.NonNullElements(...))</Title>
- <Shortcut>cinn</Shortcut>
- <Description>Emits a 'Contract.Invariant' non-null elements clause</Description>
- <Author>tabarbe</Author>
- </Header>
- <Snippet>
- <Imports>
- <Import>
- <Namespace>System.Diagnostics.Contracts</Namespace>
- </Import>
- </Imports>
- <Declarations>
- <Object Editable="true">
- <ID>collection</ID>
- <ToolTip>collection whose elements must not be null</ToolTip>
- <Default>arg</Default>
- <Function>
- </Function>
- </Object>
- </Declarations>
- <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Invariant(cce.NonNullElements($collection$));$end$]]></Code>
- </Snippet>
- </CodeSnippet>
-</CodeSnippets>
+<?xml version="1.0" encoding="utf-8"?> +<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet"> + <CodeSnippet Format="1.0.0"> + <Header> + <SnippetTypes> + <SnippetType>Expansion</SnippetType> + </SnippetTypes> + <Title>Contract.Invariant(cce.NonNullElements(...))</Title> + <Shortcut>cinn</Shortcut> + <Description>Emits a 'Contract.Invariant' non-null elements clause</Description> + <Author>tabarbe</Author> + </Header> + <Snippet> + <Imports> + <Import> + <Namespace>System.Diagnostics.Contracts</Namespace> + </Import> + </Imports> + <Declarations> + <Object Editable="true"> + <ID>collection</ID> + <ToolTip>collection whose elements must not be null</ToolTip> + <Default>arg</Default> + <Function> + </Function> + </Object> + </Declarations> + <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Invariant(cce.NonNullElements($collection$));$end$]]></Code> + </Snippet> + </CodeSnippet> +</CodeSnippets> 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 @@ -<?xml version="1.0" encoding="utf-8"?>
-<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet">
- <CodeSnippet Format="1.0.0">
- <Header>
- <SnippetTypes>
- <SnippetType>Expansion</SnippetType>
- </SnippetTypes>
- <Title>Contract.Requires(cce.NonNullElements(...))</Title>
- <Shortcut>crnn</Shortcut>
- <Description>Emits a 'Contract.Requires' non-null elements clause</Description>
- <Author>tabarbe</Author>
- </Header>
- <Snippet>
- <Imports>
- <Import>
- <Namespace>System.Diagnostics.Contracts</Namespace>
- </Import>
- </Imports>
- <Declarations>
- <Object Editable="true">
- <ID>collection</ID>
- <ToolTip>collection whose elements must not be null</ToolTip>
- <Default>arg</Default>
- <Function>
- </Function>
- </Object>
- </Declarations>
- <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Requires(cce.NonNullElements($collection$));$end$]]></Code>
- </Snippet>
- </CodeSnippet>
-</CodeSnippets>
+<?xml version="1.0" encoding="utf-8"?> +<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet"> + <CodeSnippet Format="1.0.0"> + <Header> + <SnippetTypes> + <SnippetType>Expansion</SnippetType> + </SnippetTypes> + <Title>Contract.Requires(cce.NonNullElements(...))</Title> + <Shortcut>crnn</Shortcut> + <Description>Emits a 'Contract.Requires' non-null elements clause</Description> + <Author>tabarbe</Author> + </Header> + <Snippet> + <Imports> + <Import> + <Namespace>System.Diagnostics.Contracts</Namespace> + </Import> + </Imports> + <Declarations> + <Object Editable="true"> + <ID>collection</ID> + <ToolTip>collection whose elements must not be null</ToolTip> + <Default>arg</Default> + <Function> + </Function> + </Object> + </Declarations> + <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Requires(cce.NonNullElements($collection$));$end$]]></Code> + </Snippet> + </CodeSnippet> +</CodeSnippets> 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 @@ -<?xml version="1.0" encoding="utf-8"?>
-<Project DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003" ToolsVersion="4.0">
- <PropertyGroup>
- <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.30729</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <OutputType>Library</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>Demo.BoogieLanguageService</RootNamespace>
- <AssemblyName>BoogieLanguageService</AssemblyName>
- <SignAssembly>True</SignAssembly>
- <AssemblyOriginatorKeyFile>Key.snk</AssemblyOriginatorKeyFile>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <ProjectGuid>{66E611EE-84D8-4EB9-9A33-164A53E00553}</ProjectGuid>
- <FileUpgradeFlags>
- </FileUpgradeFlags>
- <OldToolsVersion>4.0</OldToolsVersion>
- <UpgradeBackupLocation>
- </UpgradeBackupLocation>
- <PublishUrl>publish\</PublishUrl>
- <Install>true</Install>
- <InstallFrom>Disk</InstallFrom>
- <UpdateEnabled>false</UpdateEnabled>
- <UpdateMode>Foreground</UpdateMode>
- <UpdateInterval>7</UpdateInterval>
- <UpdateIntervalUnits>Days</UpdateIntervalUnits>
- <UpdatePeriodically>false</UpdatePeriodically>
- <UpdateRequired>false</UpdateRequired>
- <MapFileExtensions>true</MapFileExtensions>
- <ApplicationRevision>0</ApplicationRevision>
- <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
- <IsWebBootstrapper>false</IsWebBootstrapper>
- <UseApplicationTrust>false</UseApplicationTrust>
- <BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile />
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <DebugType>full</DebugType>
- <Optimize>false</Optimize>
- <OutputPath>bin\Debug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
- <DebugType>pdbonly</DebugType>
- <Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
- <DefineConstants>TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <RunCodeAnalysis>true</RunCodeAnalysis>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <ItemGroup>
- <Reference Include="Irony, Version=1.0.0.0, Culture=neutral, PublicKeyToken=ca48ace7223ead47, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>Resources\Irony.dll</HintPath>
- </Reference>
- <Reference Include="Microsoft.VisualStudio.OLE.Interop" />
- <Reference Include="Microsoft.VisualStudio.Package.LanguageService.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Package.LanguageService.10.0.dll</HintPath>
- </Reference>
- <Reference Include="Microsoft.VisualStudio.Shell.10.0">
- <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.10.0.dll</HintPath>
- </Reference>
- <Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Immutable.10.0.dll</HintPath>
- </Reference>
- <Reference Include="Microsoft.VisualStudio.Shell.Interop" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
- <SpecificVersion>False</SpecificVersion>
- <EmbedInteropTypes>True</EmbedInteropTypes>
- <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Interop.10.0.dll</HintPath>
- </Reference>
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.9.0" />
- <Reference Include="Microsoft.VisualStudio.TextManager.Interop" />
- <Reference Include="Microsoft.VisualStudio.TextManager.Interop.8.0, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>..\..\..\..\..\Program Files\Microsoft Visual Studio 2008 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.TextManager.Interop.8.0.dll</HintPath>
- </Reference>
- <Reference Include="System" />
- <Reference Include="System.Data" />
- <Reference Include="System.Design" />
- <Reference Include="System.Drawing" />
- <Reference Include="System.Windows.Forms" />
- <Reference Include="System.Xml" />
- </ItemGroup>
- <ItemGroup>
- <Compile Include="Configuration.cs" />
- <Compile Include="Grammar.cs" />
- <Compile Include="Guids.cs" />
- <Compile Include="Integration\AuthoringScope.cs" />
- <Compile Include="Integration\Configuration.cs" />
- <Compile Include="Integration\Declaration.cs" />
- <Compile Include="Integration\Declarations.cs" />
- <Compile Include="Integration\IASTResolver.cs" />
- <Compile Include="Integration\IronyViewFilter.cs" />
- <Compile Include="Integration\IronyLanguageService.cs" />
- <Compile Include="Integration\LineScanner.cs" />
- <Compile Include="Integration\Method.cs" />
- <Compile Include="Integration\Methods.cs" />
- <Compile Include="Integration\Package.cs" />
- <Compile Include="Integration\Resolver.cs" />
- <Compile Include="Integration\Source.cs" />
- <Compile Include="Resources.Designer.cs">
- <AutoGen>True</AutoGen>
- <DesignTime>True</DesignTime>
- <DependentUpon>Resources.resx</DependentUpon>
- </Compile>
- <Compile Include="GlobalSuppressions.cs" />
- <Compile Include="IronyLanguageServicePackage.cs" />
- <Compile Include="Properties\AssemblyInfo.cs" />
- </ItemGroup>
- <ItemGroup>
- <EmbeddedResource Include="Resources.resx">
- <Generator>ResXFileCodeGenerator</Generator>
- <LastGenOutput>Resources.Designer.cs</LastGenOutput>
- <SubType>Designer</SubType>
- </EmbeddedResource>
- <EmbeddedResource Include="VSPackage.resx">
- <MergeWithCTO>true</MergeWithCTO>
- <SubType>Designer</SubType>
- </EmbeddedResource>
- </ItemGroup>
- <ItemGroup>
- <Content Include="Resources\Irony.dll" />
- <None Include="source.extension.vsixmanifest" />
- </ItemGroup>
- <ItemGroup>
- <None Include="Key.snk" />
- </ItemGroup>
- <ItemGroup>
- <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
- <Install>false</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.VisualBasic.PowerPacks.10.0">
- <Visible>False</Visible>
- <ProductName>Microsoft Visual Basic PowerPacks 10.0</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
- <Visible>False</Visible>
- <ProductName>Windows Installer 3.1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- </ItemGroup>
- <PropertyGroup>
- <!--
- To specify a different registry root to register your package, uncomment the TargetRegistryRoot
- tag and specify a registry root in it.
- <TargetRegistryRoot></TargetRegistryRoot>
- -->
- <RegisterOutputPackage>true</RegisterOutputPackage>
- <RegisterWithCodebase>true</RegisterWithCodebase>
- </PropertyGroup>
- <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />
- <Import Project="$(MSBuildExtensionsPath)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" />
- <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
- Other similar extension points exist, see Microsoft.Common.targets.
- <Target Name="BeforeBuild">
- </Target>
- <Target Name="AfterBuild">
- </Target>
- -->
+<?xml version="1.0" encoding="utf-8"?> +<Project DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003" ToolsVersion="4.0"> + <PropertyGroup> + <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> + <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform> + <ProductVersion>9.0.30729</ProductVersion> + <SchemaVersion>2.0</SchemaVersion> + <OutputType>Library</OutputType> + <AppDesignerFolder>Properties</AppDesignerFolder> + <RootNamespace>Demo.BoogieLanguageService</RootNamespace> + <AssemblyName>BoogieLanguageService</AssemblyName> + <SignAssembly>True</SignAssembly> + <AssemblyOriginatorKeyFile>Key.snk</AssemblyOriginatorKeyFile> + <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> + <ProjectGuid>{66E611EE-84D8-4EB9-9A33-164A53E00553}</ProjectGuid> + <FileUpgradeFlags> + </FileUpgradeFlags> + <OldToolsVersion>4.0</OldToolsVersion> + <UpgradeBackupLocation> + </UpgradeBackupLocation> + <PublishUrl>publish\</PublishUrl> + <Install>true</Install> + <InstallFrom>Disk</InstallFrom> + <UpdateEnabled>false</UpdateEnabled> + <UpdateMode>Foreground</UpdateMode> + <UpdateInterval>7</UpdateInterval> + <UpdateIntervalUnits>Days</UpdateIntervalUnits> + <UpdatePeriodically>false</UpdatePeriodically> + <UpdateRequired>false</UpdateRequired> + <MapFileExtensions>true</MapFileExtensions> + <ApplicationRevision>0</ApplicationRevision> + <ApplicationVersion>1.0.0.%2a</ApplicationVersion> + <IsWebBootstrapper>false</IsWebBootstrapper> + <UseApplicationTrust>false</UseApplicationTrust> + <BootstrapperEnabled>true</BootstrapperEnabled> + <TargetFrameworkProfile /> + </PropertyGroup> + <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> + <DebugSymbols>true</DebugSymbols> + <DebugType>full</DebugType> + <Optimize>false</Optimize> + <OutputPath>bin\Debug\</OutputPath> + <DefineConstants>DEBUG;TRACE</DefineConstants> + <ErrorReport>prompt</ErrorReport> + <WarningLevel>4</WarningLevel> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + </PropertyGroup> + <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' "> + <DebugType>pdbonly</DebugType> + <Optimize>true</Optimize> + <OutputPath>bin\Release\</OutputPath> + <DefineConstants>TRACE</DefineConstants> + <ErrorReport>prompt</ErrorReport> + <WarningLevel>4</WarningLevel> + <RunCodeAnalysis>true</RunCodeAnalysis> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + </PropertyGroup> + <ItemGroup> + <Reference Include="Irony, Version=1.0.0.0, Culture=neutral, PublicKeyToken=ca48ace7223ead47, processorArchitecture=MSIL"> + <SpecificVersion>False</SpecificVersion> + <HintPath>Resources\Irony.dll</HintPath> + </Reference> + <Reference Include="Microsoft.VisualStudio.OLE.Interop" /> + <Reference Include="Microsoft.VisualStudio.Package.LanguageService.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL"> + <SpecificVersion>False</SpecificVersion> + <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Package.LanguageService.10.0.dll</HintPath> + </Reference> + <Reference Include="Microsoft.VisualStudio.Shell.10.0"> + <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.10.0.dll</HintPath> + </Reference> + <Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL"> + <SpecificVersion>False</SpecificVersion> + <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Immutable.10.0.dll</HintPath> + </Reference> + <Reference Include="Microsoft.VisualStudio.Shell.Interop" /> + <Reference Include="Microsoft.VisualStudio.Shell.Interop.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a"> + <SpecificVersion>False</SpecificVersion> + <EmbedInteropTypes>True</EmbedInteropTypes> + <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Interop.10.0.dll</HintPath> + </Reference> + <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0" /> + <Reference Include="Microsoft.VisualStudio.Shell.Interop.9.0" /> + <Reference Include="Microsoft.VisualStudio.TextManager.Interop" /> + <Reference Include="Microsoft.VisualStudio.TextManager.Interop.8.0, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a"> + <SpecificVersion>False</SpecificVersion> + <HintPath>..\..\..\..\..\Program Files\Microsoft Visual Studio 2008 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.TextManager.Interop.8.0.dll</HintPath> + </Reference> + <Reference Include="System" /> + <Reference Include="System.Data" /> + <Reference Include="System.Design" /> + <Reference Include="System.Drawing" /> + <Reference Include="System.Windows.Forms" /> + <Reference Include="System.Xml" /> + </ItemGroup> + <ItemGroup> + <Compile Include="Configuration.cs" /> + <Compile Include="Grammar.cs" /> + <Compile Include="Guids.cs" /> + <Compile Include="Integration\AuthoringScope.cs" /> + <Compile Include="Integration\Configuration.cs" /> + <Compile Include="Integration\Declaration.cs" /> + <Compile Include="Integration\Declarations.cs" /> + <Compile Include="Integration\IASTResolver.cs" /> + <Compile Include="Integration\IronyViewFilter.cs" /> + <Compile Include="Integration\IronyLanguageService.cs" /> + <Compile Include="Integration\LineScanner.cs" /> + <Compile Include="Integration\Method.cs" /> + <Compile Include="Integration\Methods.cs" /> + <Compile Include="Integration\Package.cs" /> + <Compile Include="Integration\Resolver.cs" /> + <Compile Include="Integration\Source.cs" /> + <Compile Include="Resources.Designer.cs"> + <AutoGen>True</AutoGen> + <DesignTime>True</DesignTime> + <DependentUpon>Resources.resx</DependentUpon> + </Compile> + <Compile Include="GlobalSuppressions.cs" /> + <Compile Include="IronyLanguageServicePackage.cs" /> + <Compile Include="Properties\AssemblyInfo.cs" /> + </ItemGroup> + <ItemGroup> + <EmbeddedResource Include="Resources.resx"> + <Generator>ResXFileCodeGenerator</Generator> + <LastGenOutput>Resources.Designer.cs</LastGenOutput> + <SubType>Designer</SubType> + </EmbeddedResource> + <EmbeddedResource Include="VSPackage.resx"> + <MergeWithCTO>true</MergeWithCTO> + <SubType>Designer</SubType> + </EmbeddedResource> + </ItemGroup> + <ItemGroup> + <Content Include="Resources\Irony.dll" /> + <None Include="source.extension.vsixmanifest" /> + </ItemGroup> + <ItemGroup> + <None Include="Key.snk" /> + </ItemGroup> + <ItemGroup> + <BootstrapperPackage Include="Microsoft.Net.Client.3.5"> + <Visible>False</Visible> + <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName> + <Install>false</Install> + </BootstrapperPackage> + <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1"> + <Visible>False</Visible> + <ProductName>.NET Framework 3.5 SP1</ProductName> + <Install>true</Install> + </BootstrapperPackage> + <BootstrapperPackage Include="Microsoft.VisualBasic.PowerPacks.10.0"> + <Visible>False</Visible> + <ProductName>Microsoft Visual Basic PowerPacks 10.0</ProductName> + <Install>true</Install> + </BootstrapperPackage> + <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1"> + <Visible>False</Visible> + <ProductName>Windows Installer 3.1</ProductName> + <Install>true</Install> + </BootstrapperPackage> + </ItemGroup> + <PropertyGroup> + <!-- + To specify a different registry root to register your package, uncomment the TargetRegistryRoot + tag and specify a registry root in it. + <TargetRegistryRoot></TargetRegistryRoot> + --> + <RegisterOutputPackage>true</RegisterOutputPackage> + <RegisterWithCodebase>true</RegisterWithCodebase> + </PropertyGroup> + <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" /> + <Import Project="$(MSBuildExtensionsPath)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" /> + <!-- To modify your build process, add your task inside one of the targets below and uncomment it. + Other similar extension points exist, see Microsoft.Common.targets. + <Target Name="BeforeBuild"> + </Target> + <Target Name="AfterBuild"> + </Target> + --> </Project>
\ 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<B ..." either as comparison or as beginning of GenericsPostfix
- | QualifiedName + less + expression
- //| QualifiedName + less + QualifiedName + greater
- //| NewStmt
- | NewArrStmt
- | ArrayExpression
- | FunctionExpression
- | ArrayConstructor
- | expression + BinOp + expression
- | LUnOp + expression
- | expression + RUnOp
- | LParen + expression + RParen
- | ToTerm("unfolding") + expression + "in" + expression
- | ToTerm("acc") + "(" + selectExpr + (("," + expression) | Empty) + ")"
- | ToTerm("old") + "(" + expression + ")"
- | ToTerm("eval") + "(" + evalstate + "," + expression + ")"
- | ToTerm("credit") + "(" + expression + "," + expression + ")"
- | ToTerm("credit") + "(" + expression + ")"
- | expression + PreferShiftHere() + "?" + expression + ":" + expression
- | ToTerm("rd") +
- (ToTerm("holds") + "(" + expression + ")"
- | "(" + selectExpr + rdPermArg.Q() + ")"
- )
-
- ;
- expressionList.Rule = MakePlusRule(expressionList, comma, expression);
- identList.Rule = MakePlusRule(identList, comma, ident);
- NewStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LParen + expressionList.Q() + RParen;
- NewArrStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LBracket + expressionList.Q() + RBracket;
- BinOp.Rule = ToTerm("+") | "-" | "*" | "div" | "mod" | "^" | "&" | "|"
- | "&&" | "||" | "==" | "!=" | greater | less
- | ">=" | "<=" | "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<B ..." either as comparison or as beginning of GenericsPostfix + | QualifiedName + less + expression + //| QualifiedName + less + QualifiedName + greater + //| NewStmt + | NewArrStmt + | ArrayExpression + | FunctionExpression + | ArrayConstructor + | expression + BinOp + expression + | LUnOp + expression + | expression + RUnOp + | LParen + expression + RParen + | ToTerm("unfolding") + expression + "in" + expression + | ToTerm("acc") + "(" + selectExpr + (("," + expression) | Empty) + ")" + | ToTerm("old") + "(" + expression + ")" + | ToTerm("eval") + "(" + evalstate + "," + expression + ")" + | ToTerm("credit") + "(" + expression + "," + expression + ")" + | ToTerm("credit") + "(" + expression + ")" + | expression + PreferShiftHere() + "?" + expression + ":" + expression + | ToTerm("rd") + + (ToTerm("holds") + "(" + expression + ")" + | "(" + selectExpr + rdPermArg.Q() + ")" + ) + + ; + expressionList.Rule = MakePlusRule(expressionList, comma, expression); + identList.Rule = MakePlusRule(identList, comma, ident); + NewStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LParen + expressionList.Q() + RParen; + NewArrStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LBracket + expressionList.Q() + RBracket; + BinOp.Rule = ToTerm("+") | "-" | "*" | "div" | "mod" | "^" | "&" | "|" + | "&&" | "||" | "==" | "!=" | greater | less + | ">=" | "<=" | "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<Declaration> 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<Declaration> 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<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem> colorableItems = new List<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem>();
-
- public static IList<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem> 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<string, TokenDefinition> definitions = new Dictionary<string, TokenDefinition>();
-
- 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<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem> colorableItems = new List<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem>(); + + public static IList<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem> 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<string, TokenDefinition> definitions = new Dictionary<string, TokenDefinition>(); + + 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<Declaration>
- {
- 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<Declaration> Members
-
- public int CompareTo(Declaration other)
- {
- return DisplayText.CompareTo(other.DisplayText);
- }
-
- #endregion
- }
+using System; +using System.Collections.Generic; + +namespace Demo +{ + public struct Declaration : IComparable<Declaration> + { + 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<Declaration> 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<Declaration> declarations;
- public Declarations(IList<Declaration> 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<Declaration> declarations; + public Declarations(IList<Declaration> 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<Declaration> FindCompletions(object result, int line, int col);
- IList<Declaration> FindMembers(object result, int line, int col);
- string FindQuickInfo(object result, int line, int col);
- IList<Method> FindMethods(object result, int line, int col, string name);
- }
+using System; +using System.Collections.Generic; + +namespace Demo +{ + interface IASTResolver + { + IList<Declaration> FindCompletions(object result, int line, int col); + IList<Declaration> FindMembers(object result, int line, int col); + string FindQuickInfo(object result, int line, int col); + IList<Method> 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<TextSpan[]>();
- }
- 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);
- }
-
- /// <summary>
- /// Called to determine if the given location can have a breakpoint applied to it.
- /// </summary>
- /// <param name="buffer">The IVsTextBuffer object containing the source file.</param>
- /// <param name="line">The line number where the breakpoint is to be set.</param>
- /// <param name="col">The offset into the line where the breakpoint is to be set.</param>
- /// <param name="pCodeSpan">
- /// Returns the TextSpan giving the extent of the code affected by the breakpoint if the
- /// breakpoint can be set.
- /// </param>
- /// <returns>
- /// 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).
- /// </returns>
- /// <remarks>
- /// <para>
- /// 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.
- /// </para>
- /// <para>
- /// 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.
- /// </para>
- /// <para>
- /// 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.
- /// </para>
- /// <para>
- /// The base method returns E_NOTIMPL.
- /// </para>
- /// </remarks>
- 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<TextSpan[]>(); + } + 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); + } + + /// <summary> + /// Called to determine if the given location can have a breakpoint applied to it. + /// </summary> + /// <param name="buffer">The IVsTextBuffer object containing the source file.</param> + /// <param name="line">The line number where the breakpoint is to be set.</param> + /// <param name="col">The offset into the line where the breakpoint is to be set.</param> + /// <param name="pCodeSpan"> + /// Returns the TextSpan giving the extent of the code affected by the breakpoint if the + /// breakpoint can be set. + /// </param> + /// <returns> + /// 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). + /// </returns> + /// <remarks> + /// <para> + /// 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. + /// </para> + /// <para> + /// 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. + /// </para> + /// <para> + /// 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. + /// </para> + /// <para> + /// The base method returns E_NOTIMPL. + /// </para> + /// </remarks> + 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<Parameter> 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<Parameter> 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<Method> methods;
- public Methods(IList<Method> 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<Method> methods; + public Methods(IList<Method> 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<Demo.Declaration> FindCompletions(object result, int line, int col)
- {
- // Used for intellisense.
- List<Demo.Declaration> declarations = new List<Demo.Declaration>();
-
- // 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<Demo.Declaration> FindMembers(object result, int line, int col)
- {
- List<Demo.Declaration> members = new List<Demo.Declaration>();
-
- return members;
- }
-
- public string FindQuickInfo(object result, int line, int col)
- {
- return "unknown";
- }
-
- public IList<Demo.Method> FindMethods(object result, int line, int col, string name)
- {
- return new List<Demo.Method>();
- }
-
- #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<Demo.Declaration> FindCompletions(object result, int line, int col) + { + // Used for intellisense. + List<Demo.Declaration> declarations = new List<Demo.Declaration>(); + + // 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<Demo.Declaration> FindMembers(object result, int line, int col) + { + List<Demo.Declaration> members = new List<Demo.Declaration>(); + + return members; + } + + public string FindQuickInfo(object result, int line, int col) + { + return "unknown"; + } + + public IList<Demo.Method> FindMethods(object result, int line, int col, string name) + { + return new List<Demo.Method>(); + } + + #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<TextSpan[]> braces;
- public IList<TextSpan[]> 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<TextSpan[]> braces; + public IList<TextSpan[]> 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
-{
- /// <summary>
- /// 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.
- /// </summary>
- // 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
- {
- /// <summary>
- /// 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.
- /// </summary>
- public BoogieLanguageService()
- {
- Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering constructor for: {0}", this.ToString()));
- }
-
-
-
- /////////////////////////////////////////////////////////////////////////////
- // Overriden Package Implementation
- #region Package Members
-
- /// <summary>
- /// 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.
- /// </summary>
- 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 +{ + /// <summary> + /// 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. + /// </summary> + // 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 + { + /// <summary> + /// 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. + /// </summary> + public BoogieLanguageService() + { + Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering constructor for: {0}", this.ToString())); + } + + + + ///////////////////////////////////////////////////////////////////////////// + // Overriden Package Implementation + #region Package Members + + /// <summary> + /// 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. + /// </summary> + 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 @@ -//------------------------------------------------------------------------------
-// <auto-generated>
-// 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.
-// </auto-generated>
-//------------------------------------------------------------------------------
-
-namespace Demo {
- using System;
-
-
- /// <summary>
- /// A strongly-typed resource class, for looking up localized strings, etc.
- /// </summary>
- // 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() {
- }
-
- /// <summary>
- /// Returns the cached ResourceManager instance used by this class.
- /// </summary>
- [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;
- }
- }
-
- /// <summary>
- /// Overrides the current thread's CurrentUICulture property for all
- /// resource lookups using this strongly typed resource class.
- /// </summary>
- [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)]
- internal static global::System.Globalization.CultureInfo Culture {
- get {
- return resourceCulture;
- }
- set {
- resourceCulture = value;
- }
- }
- }
-}
+//------------------------------------------------------------------------------ +// <auto-generated> +// 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. +// </auto-generated> +//------------------------------------------------------------------------------ + +namespace Demo { + using System; + + + /// <summary> + /// A strongly-typed resource class, for looking up localized strings, etc. + /// </summary> + // 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() { + } + + /// <summary> + /// Returns the cached ResourceManager instance used by this class. + /// </summary> + [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; + } + } + + /// <summary> + /// Overrides the current thread's CurrentUICulture property for all + /// resource lookups using this strongly typed resource class. + /// </summary> + [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 @@ -<?xml version="1.0" encoding="utf-8"?>
-<!--
- VS SDK Notes: This resx file contains the resources that will be consumed directly by your package.
- For example, if you chose to create a tool window, there is a resource with ID 'CanNotCreateWindow'. This
- is used in VsPkg.cs to determine the string to show the user if there is an error when attempting to create
- the tool window.
-
- Resources that are accessed directly from your package *by Visual Studio* are stored in the VSPackage.resx
- file.
--->
-<root>
- <!--
- Microsoft ResX Schema
-
- Version 2.0
-
- The primary goals of this format is to allow a simple XML format
- that is mostly human readable. The generation and parsing of the
- various data types are done through the TypeConverter classes
- associated with the data types.
-
- Example:
-
- ... ado.net/XML headers & schema ...
- <resheader name="resmimetype">text/microsoft-resx</resheader>
- <resheader name="version">2.0</resheader>
- <resheader name="reader">System.Resources.ResXResourceReader, System.Windows.Forms, ...</resheader>
- <resheader name="writer">System.Resources.ResXResourceWriter, System.Windows.Forms, ...</resheader>
- <data name="Name1"><value>this is my long string</value><comment>this is a comment</comment></data>
- <data name="Color1" type="System.Drawing.Color, System.Drawing">Blue</data>
- <data name="Bitmap1" mimetype="application/x-microsoft.net.object.binary.base64">
- <value>[base64 mime encoded serialized .NET Framework object]</value>
- </data>
- <data name="Icon1" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64">
- <value>[base64 mime encoded string representing a byte array form of the .NET Framework object]</value>
- <comment>This is a comment</comment>
- </data>
-
- There are any number of "resheader" rows that contain simple
- name/value pairs.
-
- Each data row contains a name, and value. The row also contains a
- type or mimetype. Type corresponds to a .NET class that support
- text/value conversion through the TypeConverter architecture.
- Classes that don't support this are serialized and stored with the
- mimetype set.
-
- The mimetype is used for serialized objects, and tells the
- ResXResourceReader how to depersist the object. This is currently not
- extensible. For a given mimetype the value must be set accordingly:
-
- Note - application/x-microsoft.net.object.binary.base64 is the format
- that the ResXResourceWriter will generate, however the reader can
- read any of the formats listed below.
-
- mimetype: application/x-microsoft.net.object.binary.base64
- value : The object must be serialized with
- : System.Runtime.Serialization.Formatters.Binary.BinaryFormatter
- : and then encoded with base64 encoding.
-
- mimetype: application/x-microsoft.net.object.soap.base64
- value : The object must be serialized with
- : System.Runtime.Serialization.Formatters.Soap.SoapFormatter
- : and then encoded with base64 encoding.
-
- mimetype: application/x-microsoft.net.object.bytearray.base64
- value : The object must be serialized into a byte array
- : using a System.ComponentModel.TypeConverter
- : and then encoded with base64 encoding.
- -->
- <xsd:schema id="root" xmlns="" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:msdata="urn:schemas-microsoft-com:xml-msdata">
- <xsd:import namespace="http://www.w3.org/XML/1998/namespace" />
- <xsd:element name="root" msdata:IsDataSet="true">
- <xsd:complexType>
- <xsd:choice maxOccurs="unbounded">
- <xsd:element name="metadata">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" />
- </xsd:sequence>
- <xsd:attribute name="name" use="required" type="xsd:string" />
- <xsd:attribute name="type" type="xsd:string" />
- <xsd:attribute name="mimetype" type="xsd:string" />
- <xsd:attribute ref="xml:space" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="assembly">
- <xsd:complexType>
- <xsd:attribute name="alias" type="xsd:string" />
- <xsd:attribute name="name" type="xsd:string" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="data">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />
- <xsd:element name="comment" type="xsd:string" minOccurs="0" msdata:Ordinal="2" />
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required" msdata:Ordinal="1" />
- <xsd:attribute name="type" type="xsd:string" msdata:Ordinal="3" />
- <xsd:attribute name="mimetype" type="xsd:string" msdata:Ordinal="4" />
- <xsd:attribute ref="xml:space" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="resheader">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required" />
- </xsd:complexType>
- </xsd:element>
- </xsd:choice>
- </xsd:complexType>
- </xsd:element>
- </xsd:schema>
- <resheader name="resmimetype">
- <value>text/microsoft-resx</value>
- </resheader>
- <resheader name="version">
- <value>2.0</value>
- </resheader>
- <resheader name="reader">
- <value>System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>
- </resheader>
- <resheader name="writer">
- <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>
- </resheader>
- <assembly alias="System.Windows.Forms" name="System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089" />
+<?xml version="1.0" encoding="utf-8"?> +<!-- + VS SDK Notes: This resx file contains the resources that will be consumed directly by your package. + For example, if you chose to create a tool window, there is a resource with ID 'CanNotCreateWindow'. This + is used in VsPkg.cs to determine the string to show the user if there is an error when attempting to create + the tool window. + + Resources that are accessed directly from your package *by Visual Studio* are stored in the VSPackage.resx + file. +--> +<root> + <!-- + Microsoft ResX Schema + + Version 2.0 + + The primary goals of this format is to allow a simple XML format + that is mostly human readable. The generation and parsing of the + various data types are done through the TypeConverter classes + associated with the data types. + + Example: + + ... ado.net/XML headers & schema ... + <resheader name="resmimetype">text/microsoft-resx</resheader> + <resheader name="version">2.0</resheader> + <resheader name="reader">System.Resources.ResXResourceReader, System.Windows.Forms, ...</resheader> + <resheader name="writer">System.Resources.ResXResourceWriter, System.Windows.Forms, ...</resheader> + <data name="Name1"><value>this is my long string</value><comment>this is a comment</comment></data> + <data name="Color1" type="System.Drawing.Color, System.Drawing">Blue</data> + <data name="Bitmap1" mimetype="application/x-microsoft.net.object.binary.base64"> + <value>[base64 mime encoded serialized .NET Framework object]</value> + </data> + <data name="Icon1" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64"> + <value>[base64 mime encoded string representing a byte array form of the .NET Framework object]</value> + <comment>This is a comment</comment> + </data> + + There are any number of "resheader" rows that contain simple + name/value pairs. + + Each data row contains a name, and value. The row also contains a + type or mimetype. Type corresponds to a .NET class that support + text/value conversion through the TypeConverter architecture. + Classes that don't support this are serialized and stored with the + mimetype set. + + The mimetype is used for serialized objects, and tells the + ResXResourceReader how to depersist the object. This is currently not + extensible. For a given mimetype the value must be set accordingly: + + Note - application/x-microsoft.net.object.binary.base64 is the format + that the ResXResourceWriter will generate, however the reader can + read any of the formats listed below. + + mimetype: application/x-microsoft.net.object.binary.base64 + value : The object must be serialized with + : System.Runtime.Serialization.Formatters.Binary.BinaryFormatter + : and then encoded with base64 encoding. + + mimetype: application/x-microsoft.net.object.soap.base64 + value : The object must be serialized with + : System.Runtime.Serialization.Formatters.Soap.SoapFormatter + : and then encoded with base64 encoding. + + mimetype: application/x-microsoft.net.object.bytearray.base64 + value : The object must be serialized into a byte array + : using a System.ComponentModel.TypeConverter + : and then encoded with base64 encoding. + --> + <xsd:schema id="root" xmlns="" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:msdata="urn:schemas-microsoft-com:xml-msdata"> + <xsd:import namespace="http://www.w3.org/XML/1998/namespace" /> + <xsd:element name="root" msdata:IsDataSet="true"> + <xsd:complexType> + <xsd:choice maxOccurs="unbounded"> + <xsd:element name="metadata"> + <xsd:complexType> + <xsd:sequence> + <xsd:element name="value" type="xsd:string" minOccurs="0" /> + </xsd:sequence> + <xsd:attribute name="name" use="required" type="xsd:string" /> + <xsd:attribute name="type" type="xsd:string" /> + <xsd:attribute name="mimetype" type="xsd:string" /> + <xsd:attribute ref="xml:space" /> + </xsd:complexType> + </xsd:element> + <xsd:element name="assembly"> + <xsd:complexType> + <xsd:attribute name="alias" type="xsd:string" /> + <xsd:attribute name="name" type="xsd:string" /> + </xsd:complexType> + </xsd:element> + <xsd:element name="data"> + <xsd:complexType> + <xsd:sequence> + <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" /> + <xsd:element name="comment" type="xsd:string" minOccurs="0" msdata:Ordinal="2" /> + </xsd:sequence> + <xsd:attribute name="name" type="xsd:string" use="required" msdata:Ordinal="1" /> + <xsd:attribute name="type" type="xsd:string" msdata:Ordinal="3" /> + <xsd:attribute name="mimetype" type="xsd:string" msdata:Ordinal="4" /> + <xsd:attribute ref="xml:space" /> + </xsd:complexType> + </xsd:element> + <xsd:element name="resheader"> + <xsd:complexType> + <xsd:sequence> + <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" /> + </xsd:sequence> + <xsd:attribute name="name" type="xsd:string" use="required" /> + </xsd:complexType> + </xsd:element> + </xsd:choice> + </xsd:complexType> + </xsd:element> + </xsd:schema> + <resheader name="resmimetype"> + <value>text/microsoft-resx</value> + </resheader> + <resheader name="version"> + <value>2.0</value> + </resheader> + <resheader name="reader"> + <value>System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value> + </resheader> + <resheader name="writer"> + <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value> + </resheader> + <assembly alias="System.Windows.Forms" name="System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089" /> </root>
\ 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 @@ -<?xml version="1.0" encoding="utf-8"?>
-<root>
- <!--
- Microsoft ResX Schema
-
- Version 2.0
-
- The primary goals of this format is to allow a simple XML format
- that is mostly human readable. The generation and parsing of the
- various data types are done through the TypeConverter classes
- associated with the data types.
-
- Example:
-
- ... ado.net/XML headers & schema ...
- <resheader name="resmimetype">text/microsoft-resx</resheader>
- <resheader name="version">2.0</resheader>
- <resheader name="reader">System.Resources.ResXResourceReader, System.Windows.Forms, ...</resheader>
- <resheader name="writer">System.Resources.ResXResourceWriter, System.Windows.Forms, ...</resheader>
- <data name="Name1"><value>this is my long string</value><comment>this is a comment</comment></data>
- <data name="Color1" type="System.Drawing.Color, System.Drawing">Blue</data>
- <data name="Bitmap1" mimetype="application/x-microsoft.net.object.binary.base64">
- <value>[base64 mime encoded serialized .NET Framework object]</value>
- </data>
- <data name="Icon1" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64">
- <value>[base64 mime encoded string representing a byte array form of the .NET Framework object]</value>
- <comment>This is a comment</comment>
- </data>
-
- There are any number of "resheader" rows that contain simple
- name/value pairs.
-
- Each data row contains a name, and value. The row also contains a
- type or mimetype. Type corresponds to a .NET class that support
- text/value conversion through the TypeConverter architecture.
- Classes that don't support this are serialized and stored with the
- mimetype set.
-
- The mimetype is used for serialized objects, and tells the
- ResXResourceReader how to depersist the object. This is currently not
- extensible. For a given mimetype the value must be set accordingly:
-
- Note - application/x-microsoft.net.object.binary.base64 is the format
- that the ResXResourceWriter will generate, however the reader can
- read any of the formats listed below.
-
- mimetype: application/x-microsoft.net.object.binary.base64
- value : The object must be serialized with
- : System.Runtime.Serialization.Formatters.Binary.BinaryFormatter
- : and then encoded with base64 encoding.
-
- mimetype: application/x-microsoft.net.object.soap.base64
- value : The object must be serialized with
- : System.Runtime.Serialization.Formatters.Soap.SoapFormatter
- : and then encoded with base64 encoding.
-
- mimetype: application/x-microsoft.net.object.bytearray.base64
- value : The object must be serialized into a byte array
- : using a System.ComponentModel.TypeConverter
- : and then encoded with base64 encoding.
- -->
- <xsd:schema id="root" xmlns="" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:msdata="urn:schemas-microsoft-com:xml-msdata">
- <xsd:import namespace="http://www.w3.org/XML/1998/namespace" />
- <xsd:element name="root" msdata:IsDataSet="true">
- <xsd:complexType>
- <xsd:choice maxOccurs="unbounded">
- <xsd:element name="metadata">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" />
- </xsd:sequence>
- <xsd:attribute name="name" use="required" type="xsd:string" />
- <xsd:attribute name="type" type="xsd:string" />
- <xsd:attribute name="mimetype" type="xsd:string" />
- <xsd:attribute ref="xml:space" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="assembly">
- <xsd:complexType>
- <xsd:attribute name="alias" type="xsd:string" />
- <xsd:attribute name="name" type="xsd:string" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="data">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />
- <xsd:element name="comment" type="xsd:string" minOccurs="0" msdata:Ordinal="2" />
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required" msdata:Ordinal="1" />
- <xsd:attribute name="type" type="xsd:string" msdata:Ordinal="3" />
- <xsd:attribute name="mimetype" type="xsd:string" msdata:Ordinal="4" />
- <xsd:attribute ref="xml:space" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="resheader">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required" />
- </xsd:complexType>
- </xsd:element>
- </xsd:choice>
- </xsd:complexType>
- </xsd:element>
- </xsd:schema>
- <resheader name="resmimetype">
- <value>text/microsoft-resx</value>
- </resheader>
- <resheader name="version">
- <value>2.0</value>
- </resheader>
- <resheader name="reader">
- <value>System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>
- </resheader>
- <resheader name="writer">
- <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>
- </resheader>
- <data name="104" xml:space="preserve">
- <value>Paste PLK Here</value>
- </data>
- <data name="110" xml:space="preserve">
- <value>Boogie</value>
- </data>
- <data name="112" xml:space="preserve">
- <value>Microsoft Research Boogie, intermediate verification language</value>
- </data>
+<?xml version="1.0" encoding="utf-8"?> +<root> + <!-- + Microsoft ResX Schema + + Version 2.0 + + The primary goals of this format is to allow a simple XML format + that is mostly human readable. The generation and parsing of the + various data types are done through the TypeConverter classes + associated with the data types. + + Example: + + ... ado.net/XML headers & schema ... + <resheader name="resmimetype">text/microsoft-resx</resheader> + <resheader name="version">2.0</resheader> + <resheader name="reader">System.Resources.ResXResourceReader, System.Windows.Forms, ...</resheader> + <resheader name="writer">System.Resources.ResXResourceWriter, System.Windows.Forms, ...</resheader> + <data name="Name1"><value>this is my long string</value><comment>this is a comment</comment></data> + <data name="Color1" type="System.Drawing.Color, System.Drawing">Blue</data> + <data name="Bitmap1" mimetype="application/x-microsoft.net.object.binary.base64"> + <value>[base64 mime encoded serialized .NET Framework object]</value> + </data> + <data name="Icon1" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64"> + <value>[base64 mime encoded string representing a byte array form of the .NET Framework object]</value> + <comment>This is a comment</comment> + </data> + + There are any number of "resheader" rows that contain simple + name/value pairs. + + Each data row contains a name, and value. The row also contains a + type or mimetype. Type corresponds to a .NET class that support + text/value conversion through the TypeConverter architecture. + Classes that don't support this are serialized and stored with the + mimetype set. + + The mimetype is used for serialized objects, and tells the + ResXResourceReader how to depersist the object. This is currently not + extensible. For a given mimetype the value must be set accordingly: + + Note - application/x-microsoft.net.object.binary.base64 is the format + that the ResXResourceWriter will generate, however the reader can + read any of the formats listed below. + + mimetype: application/x-microsoft.net.object.binary.base64 + value : The object must be serialized with + : System.Runtime.Serialization.Formatters.Binary.BinaryFormatter + : and then encoded with base64 encoding. + + mimetype: application/x-microsoft.net.object.soap.base64 + value : The object must be serialized with + : System.Runtime.Serialization.Formatters.Soap.SoapFormatter + : and then encoded with base64 encoding. + + mimetype: application/x-microsoft.net.object.bytearray.base64 + value : The object must be serialized into a byte array + : using a System.ComponentModel.TypeConverter + : and then encoded with base64 encoding. + --> + <xsd:schema id="root" xmlns="" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:msdata="urn:schemas-microsoft-com:xml-msdata"> + <xsd:import namespace="http://www.w3.org/XML/1998/namespace" /> + <xsd:element name="root" msdata:IsDataSet="true"> + <xsd:complexType> + <xsd:choice maxOccurs="unbounded"> + <xsd:element name="metadata"> + <xsd:complexType> + <xsd:sequence> + <xsd:element name="value" type="xsd:string" minOccurs="0" /> + </xsd:sequence> + <xsd:attribute name="name" use="required" type="xsd:string" /> + <xsd:attribute name="type" type="xsd:string" /> + <xsd:attribute name="mimetype" type="xsd:string" /> + <xsd:attribute ref="xml:space" /> + </xsd:complexType> + </xsd:element> + <xsd:element name="assembly"> + <xsd:complexType> + <xsd:attribute name="alias" type="xsd:string" /> + <xsd:attribute name="name" type="xsd:string" /> + </xsd:complexType> + </xsd:element> + <xsd:element name="data"> + <xsd:complexType> + <xsd:sequence> + <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" /> + <xsd:element name="comment" type="xsd:string" minOccurs="0" msdata:Ordinal="2" /> + </xsd:sequence> + <xsd:attribute name="name" type="xsd:string" use="required" msdata:Ordinal="1" /> + <xsd:attribute name="type" type="xsd:string" msdata:Ordinal="3" /> + <xsd:attribute name="mimetype" type="xsd:string" msdata:Ordinal="4" /> + <xsd:attribute ref="xml:space" /> + </xsd:complexType> + </xsd:element> + <xsd:element name="resheader"> + <xsd:complexType> + <xsd:sequence> + <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" /> + </xsd:sequence> + <xsd:attribute name="name" type="xsd:string" use="required" /> + </xsd:complexType> + </xsd:element> + </xsd:choice> + </xsd:complexType> + </xsd:element> + </xsd:schema> + <resheader name="resmimetype"> + <value>text/microsoft-resx</value> + </resheader> + <resheader name="version"> + <value>2.0</value> + </resheader> + <resheader name="reader"> + <value>System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value> + </resheader> + <resheader name="writer"> + <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value> + </resheader> + <data name="104" xml:space="preserve"> + <value>Paste PLK Here</value> + </data> + <data name="110" xml:space="preserve"> + <value>Boogie</value> + </data> + <data name="112" xml:space="preserve"> + <value>Microsoft Research Boogie, intermediate verification language</value> + </data> </root>
\ 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 @@ -<?xml version="1.0" encoding="utf-8"?>
-<Vsix xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema" Version="1.0.0" xmlns="http://schemas.microsoft.com/developer/vsx-schema/2010">
-
- <Identifier Id="BoogieService.MicrosoftResearch.A38156F6-63DF-4E3C-8D23-07D3DE0D3388">
- <Name>BoogieService</Name>
- <Author>Microsoft Research</Author>
- <Version>1.0</Version>
- <Description>Information about my package</Description>
- <Locale>1033</Locale>
- <!--<InstalledByMSI>false</InstalledByMSI>-->
- <SupportedProducts>
- <VisualStudio Version="10.0">
- <Edition>Pro</Edition>
- <Edition>VST_All</Edition>
- </VisualStudio>
- </SupportedProducts>
- <SupportedFrameworkRuntimeEdition MinVersion="2.0" MaxVersion="4.0" />
- </Identifier>
-
- <References/>
-
- <Content>
- <VsPackage>
- BoogieService.pkgdef
- </VsPackage>
- </Content>
-</Vsix>
+<?xml version="1.0" encoding="utf-8"?> +<Vsix xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema" Version="1.0.0" xmlns="http://schemas.microsoft.com/developer/vsx-schema/2010"> + + <Identifier Id="BoogieService.MicrosoftResearch.A38156F6-63DF-4E3C-8D23-07D3DE0D3388"> + <Name>BoogieService</Name> + <Author>Microsoft Research</Author> + <Version>1.0</Version> + <Description>Information about my package</Description> + <Locale>1033</Locale> + <!--<InstalledByMSI>false</InstalledByMSI>--> + <SupportedProducts> + <VisualStudio Version="10.0"> + <Edition>Pro</Edition> + <Edition>VST_All</Edition> + </VisualStudio> + </SupportedProducts> + <SupportedFrameworkRuntimeEdition MinVersion="2.0" MaxVersion="4.0" /> + </Identifier> + + <References/> + + <Content> + <VsPackage> + BoogieService.pkgdef + </VsPackage> + </Content> +</Vsix> 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} +} |