diff options
| author |  rustanleino <unknown> | 2010-07-19 20:46:55 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-07-19 20:46:55 +0000 |
| commit | 28e03877a9c41dc0556d17115ccd1647f9eddcf6 (patch) | |
| tree | 0a4c8f27752ea637fcf1609cdea1fe498fed1596 | |
| parent | 4a0723a7c122f78f7e6808a4ed9a48d2d58b210f (diff) | |
Chalice: Introduced '[[ S ]]' as a shorthand syntax for 'lock (this) { S }'. Think of the new brackets as atomicity brackets (see PetersonsAlgorithm.chalice)
Chalice: Added Peterson's algorithm to test suite (safety properties only)
VS 2010 integration: Updated Chalice and Dafny modes, added keyword highlighting for a new Boogie mode
41 files changed, 2300 insertions, 17 deletions
diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer index 5df00502..ab085a36 100644 --- a/Chalice/examples/Answer +++ b/Chalice/examples/Answer @@ -240,6 +240,9 @@ Boogie program verifier finished with 19 verified, 4 errors 65.5: The loop might lock/unlock more than the lockchange clause allows.
Boogie program verifier finished with 14 verified, 3 errors
+------ Running regression test PetersonsAlgorithm.chalice
+
+Boogie program verifier finished with 7 verified, 0 errors
------ Running regression test cell-defaults.chalice
96.5: The heap of the callee might not be strictly smaller than the heap of the caller.
102.5: The heap of the callee might not be strictly smaller than the heap of the caller.
diff --git a/Chalice/examples/PetersonsAlgorithm.chalice b/Chalice/examples/PetersonsAlgorithm.chalice new file mode 100644 index 00000000..8760b04b --- /dev/null +++ b/Chalice/examples/PetersonsAlgorithm.chalice @@ -0,0 +1,79 @@ +class Peterson {
+ var x0: bool;
+ var x1: bool;
+ var turn: bool;
+ ghost var cs0: bool;
+ ghost var cs1: bool;
+ ghost var b0: bool;
+ ghost var b1: bool;
+
+ invariant acc(x0,50) && acc(x1,50) && acc(turn);
+ invariant acc(cs0,50) && acc(cs1,50) && acc(b0,50) && acc(b1,50);
+ invariant cs0 ==> x0 && !b0 && (!x1 || !turn || b1);
+ invariant cs1 ==> x1 && !b1 && (!x0 || turn || b0);
+
+ method Main() {
+ var p := new Peterson{ x0 := false, x1 := false,
+ cs0 := false, cs1 := false, b0 := false, b1 := false };
+ share p;
+ fork p.Process0();
+ fork p.Process1();
+ // The purpose of the following loop is simply to prove mutual exclusion, that is,
+ // to prove that !(cs0 && cs1) follows from the monitor invariant.
+ while (true)
+ invariant rd(p.mu) && waitlevel << p.mu;
+ {
+ lock (p) { assert !(p.cs0 && p.cs1); }
+ }
+ }
+
+ method Process0()
+ requires rd(mu) && waitlevel << mu;
+ requires acc(x0,50) && acc(cs0,50) && acc(b0,50) && !x0 && !cs0 && !b0;
+ {
+ while (true)
+ invariant rd(mu) && waitlevel << mu;
+ invariant acc(x0,50) && acc(cs0,50) && acc(b0,50) && !x0 && !cs0 && !b0;
+ {
+ [[ x0 := true; b0 := true; ]]
+ [[ turn := true; b0 := false; ]]
+ // await (!x1 || !turn)
+ var waiting := true;
+ while (waiting)
+ invariant rd(mu) && waitlevel << mu && acc(cs0,50);
+ invariant acc(x0,50) && acc(b0,50) && x0 && !b0;
+ invariant !waiting ==> cs0;
+ {
+ [[ if (!x1) { waiting := false; cs0 := true; } ]]
+ [[ if (!turn) { waiting := false; cs0 := true; } ]]
+ }
+ // critical section...
+ [[ cs0 := false; x0 := false; ]]
+ }
+ }
+
+ method Process1()
+ requires rd(mu) && waitlevel << mu;
+ requires acc(x1,50) && acc(cs1,50) && acc(b1,50) && !x1 && !cs1 && !b1;
+ {
+ while (true)
+ invariant rd(mu) && waitlevel << mu;
+ invariant acc(x1,50) && acc(cs1,50) && acc(b1,50) && !x1 && !cs1 && !b1;
+ {
+ [[ x1 := true; b1 := true; ]]
+ [[ turn := false; b1 := false; ]]
+ // await (!x0 || turn)
+ var waiting := true;
+ while (waiting)
+ invariant rd(mu) && waitlevel << mu && acc(cs1,50);
+ invariant acc(x1,50) && acc(b1,50) && x1 && !b1;
+ invariant !waiting ==> cs1;
+ {
+ [[ if (!x0) { waiting := false; cs1 := true; } ]]
+ [[ if (turn) { waiting := false; cs1 := true; } ]]
+ }
+ // critical section...
+ [[ cs1 := false; x1 := false; ]]
+ }
+ }
+}
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index 8a87d2f6..12a989d7 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -36,7 +36,7 @@ class Parser extends StandardTokenParsers { "seq", "nil", "result", "eval", "token",
"wait", "signal")
// todo: can we remove "nil"?
- lexical.delimiters += ("(", ")", "{", "}",
+ lexical.delimiters += ("(", ")", "{", "}", "[[", "]]",
"<==>", "==>", "&&", "||",
"==", "!=", "<", "<=", ">=", ">", "<<",
"+", "-", "*", "/", "%", "!", ".", "..",
@@ -114,8 +114,11 @@ class Parser extends StandardTokenParsers { | "lockchange" ~> expressionList <~ Semi ^^ LockChange
)
def blockStatement: Parser[List[Statement]] = {
+ "{" ~> blockStatementBody <~ "}"
+ }
+ def blockStatementBody: Parser[List[Statement]] = {
val prev = currentLocalVariables
- "{" ~> (statement*) <~ "}" ^^ {
+ (statement*) ^^ {
case x => currentLocalVariables = prev; x }
}
@@ -125,7 +128,7 @@ class Parser extends StandardTokenParsers { // statements
- def statement =
+ def statement: Parser[Statement] =
positioned( "assert" ~> expression <~ Semi ^^ Assert
| "assume" ~> expression <~ Semi ^^ Assume
| blockStatement ^^ BlockStmt
@@ -148,6 +151,8 @@ class Parser extends StandardTokenParsers { | "release" ~> expression <~ Semi ^^ Release
| "lock" ~> "(" ~> expression ~ ")" ~ blockStatement ^^ {
case e ~ _ ~ b => Lock(e, BlockStmt(b), false) }
+ | "[[" ~> blockStatementBody <~ "]]" ^^ {
+ case b => Lock(ExplicitThisExpr(), BlockStmt(b), false) }
| "rd" ~>
( "lock" ~> "(" ~> expression ~ ")" ~ blockStatement ^^ {
case e ~ _ ~ b => Lock(e, BlockStmt(b), true) }
diff --git a/Chalice/test.bat b/Chalice/test.bat index f7c933aa..7432a145 100644 --- a/Chalice/test.bat +++ b/Chalice/test.bat @@ -10,7 +10,8 @@ REM to do: Leaks -checkLeaks for %%f in (cell counter dining-philosophers ForkJoin HandOverHand
iterator iterator2 producer-consumer
prog0 prog1 prog2 prog3 prog4 ImplicitLocals
- RockBand swap OwickiGries ProdConsChannel LoopLockChange) do (
+ RockBand swap OwickiGries ProdConsChannel LoopLockChange
+ PetersonsAlgorithm) do (
echo Testing %%f.chalice ...
echo ------ Running regression test %%f.chalice >> Output
%CHALICE% %* examples\%%f.chalice >> Output 2>&1
diff --git a/Util/VS2010/Boogie/..svnbridge/BoogieLanguageService.suo b/Util/VS2010/Boogie/..svnbridge/BoogieLanguageService.suo new file mode 100644 index 00000000..08149303 --- /dev/null +++ b/Util/VS2010/Boogie/..svnbridge/BoogieLanguageService.suo @@ -0,0 +1 @@ +<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file diff --git a/Util/VS2010/Boogie/..svnbridge/DafnyLanguageService.suo b/Util/VS2010/Boogie/..svnbridge/DafnyLanguageService.suo new file mode 100644 index 00000000..08149303 --- /dev/null +++ b/Util/VS2010/Boogie/..svnbridge/DafnyLanguageService.suo @@ -0,0 +1 @@ +<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService.sln b/Util/VS2010/Boogie/BoogieLanguageService.sln new file mode 100644 index 00000000..0ad3f0e7 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService.sln @@ -0,0 +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
diff --git a/Util/VS2010/Boogie/BoogieLanguageService.suo b/Util/VS2010/Boogie/BoogieLanguageService.suo Binary files differnew file mode 100644 index 00000000..3e0480df --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService.suo diff --git a/Util/VS2010/Boogie/BoogieLanguageService/BoogieLanguageService.csproj b/Util/VS2010/Boogie/BoogieLanguageService/BoogieLanguageService.csproj new file mode 100644 index 00000000..86e0a2bc --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/BoogieLanguageService.csproj @@ -0,0 +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>
+ -->
+</Project>
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Configuration.cs b/Util/VS2010/Boogie/BoogieLanguageService/Configuration.cs new file mode 100644 index 00000000..97775fdf --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Configuration.cs @@ -0,0 +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);
+ }
+ }
+}
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/GlobalSuppressions.cs b/Util/VS2010/Boogie/BoogieLanguageService/GlobalSuppressions.cs new file mode 100644 index 00000000..f0857cbb --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/GlobalSuppressions.cs @@ -0,0 +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")]
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs new file mode 100644 index 00000000..583349ca --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs @@ -0,0 +1,453 @@ +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");
+
+ 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",
+ "else", "ensures", "exists", "extends",
+ "false", "forall", "free", "function",
+ "goto",
+ "havoc",
+ "if", "implementation", "int", "invariant",
+ "lambda",
+ "modifies",
+ "old",
+ "procedure",
+ "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("+") | "-" | "*" | "/" | "%" | "^" | "&" | "|"
+ | "&&" | "||" | "==" | "!=" | 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
+ | "if" + Condition + Statement + PreferShiftHere() + "else" + Statement
+ | "while" + Condition + loopSpec.Star() + Statement
+ | "for" + LParen + expression.Q() + Semi + expression.Q() + Semi + expression.Q() + RParen + Statement
+ | "foreach" + LParen + ident + "in" + expression + RParen + Statement
+ | blockStatement
+ | expression + Semi
+ | "break" + Semi
+ | "continue" + Semi
+ | "return" + expression + Semi
+ | QualifiedName + ":=" + Rhs
+
+ | "var" + localVarStmt
+ | "const" + localVarStmt
+
+ | "call" + identList + ":=" + FunctionExpression + Semi
+ | "call" + FunctionExpression + Semi
+ | "assert" + expression + Semi
+ | "assume" + expression + Semi
+ | "unshare" + expression + Semi
+ | "acquire" + expression + Semi
+ | "release" + expression + Semi
+ | "downgrade" + expression + Semi
+ | "free" + expression + Semi
+ | "fold" + expression + Semi
+ | "unfold" + expression + Semi
+ | "reorder" + expression + installBounds + Semi
+ | "reorder" + expression + Semi
+ | "share" + expression + installBounds + Semi
+ | "share" + expression + Semi
+ | "fork" + identList + ":=" + FunctionExpression + Semi
+ | "fork" + FunctionExpression + Semi
+ | "join" + identList + ":=" + expression + Semi
+ | "join" + expression + Semi
+ | "send" + expression + Semi
+ | "receive" + identList + ":=" + expression + Semi
+ | "receive" + expression + Semi
+
+ ;
+ Statements.Rule = MakeStarRule(Statements, null, Statement);
+ blockStatement.Rule = LCurly + Statements + RCurly;
+
+
+ #endregion
+
+ #region 3.4 Prog
+ Prog.Rule = anything.Star() + Eof;
+
+ anything.Rule
+ = ToTerm("class")
+ | "ghost"
+ | "static"
+ | "var"
+ | "const"
+ | "method"
+ | "datatype"
+ | "assert"
+ | "assume"
+ | "new"
+ | "this"
+ | "object"
+ | "call"
+ | "if"
+ | "then"
+ | "else"
+ | "while"
+ | "invariant"
+ | "break"
+ | "return"
+ | "foreach"
+ | "match"
+ | "case"
+ | "returns"
+ | "requires"
+ | "ensures"
+ | "modifies"
+ | "reads"
+ | "decreases"
+ | "int"
+ | "bool"
+ | "false"
+ | "true"
+ | "null"
+ | "function"
+ | "free"
+ | "in"
+ | "forall"
+ | "exists"
+ | "seq"
+ | "set"
+ | "array"
+ | "match"
+ | "case"
+ | "fresh"
+ | "old"
+ | ident
+ | "}"
+ | "{"
+ | "("
+ | ")"
+ | "["
+ | "]"
+ | ","
+ | ":"
+ | ";"
+ | "."
+ | "`"
+ | "=="
+ | "!="
+ | "<"
+ | "<="
+ | ">="
+ | ">"
+ | "=>"
+ | ":="
+ | "+"
+ | "-"
+ | "*"
+ | "/"
+ | "%"
+ | "!!"
+ | "|"
+ | "!"
+ | "&&"
+ | "||"
+ | "==>"
+ | "<==>"
+ | "#"
+ | n
+ ;
+
+ idType.Rule
+ = ident + ":" + typeDecl
+ | ident
+ ;
+
+ typeDecl.Rule
+ = (ToTerm("int") | "bool" | ident | "seq" | "set" | "array") + (("<" + MakePlusRule(typeDecl, ToTerm(","), typeDecl) + ">") | Empty)
+ | ToTerm("token") + "<" + (typeDecl + ".") + 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, "*", "/", "%", "!!");
+ 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 new file mode 100644 index 00000000..a09463fd --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Guids.cs @@ -0,0 +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);
+ };
+}
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/AuthoringScope.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/AuthoringScope.cs new file mode 100644 index 00000000..9a49dbe4 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/AuthoringScope.cs @@ -0,0 +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;
+ }
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Configuration.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Configuration.cs new file mode 100644 index 00000000..f7412393 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Configuration.cs @@ -0,0 +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
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declaration.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declaration.cs new file mode 100644 index 00000000..c0fda5ca --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declaration.cs @@ -0,0 +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
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declarations.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declarations.cs new file mode 100644 index 00000000..98a411ce --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declarations.cs @@ -0,0 +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;
+ }
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IASTResolver.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IASTResolver.cs new file mode 100644 index 00000000..8de1a454 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IASTResolver.cs @@ -0,0 +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);
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs new file mode 100644 index 00000000..1d1bdce4 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs @@ -0,0 +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;
+ }
+ }
+}
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyViewFilter.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyViewFilter.cs new file mode 100644 index 00000000..55c3509e --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyViewFilter.cs @@ -0,0 +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);
+ }
+ }
+}
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/LineScanner.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/LineScanner.cs new file mode 100644 index 00000000..966e9c43 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/LineScanner.cs @@ -0,0 +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);
+ }
+ }
+}
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Method.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Method.cs new file mode 100644 index 00000000..c5071612 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Method.cs @@ -0,0 +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;
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Methods.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Methods.cs new file mode 100644 index 00000000..1d7c124f --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Methods.cs @@ -0,0 +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;
+ }
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Package.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Package.cs new file mode 100644 index 00000000..ae9c00c4 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Package.cs @@ -0,0 +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 = 1000;
+ 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 new file mode 100644 index 00000000..9f6ddeba --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Resolver.cs @@ -0,0 +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
+ }
+}
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Source.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Source.cs new file mode 100644 index 00000000..418bec01 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Source.cs @@ -0,0 +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; }
+ }
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/IronyLanguageServicePackage.cs b/Util/VS2010/Boogie/BoogieLanguageService/IronyLanguageServicePackage.cs new file mode 100644 index 00000000..c13c099b --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/IronyLanguageServicePackage.cs @@ -0,0 +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), ".dfy")]
+
+ // 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/Key.snk b/Util/VS2010/Boogie/BoogieLanguageService/Key.snk Binary files differnew file mode 100644 index 00000000..f80a4ceb --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Key.snk diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Properties/AssemblyInfo.cs b/Util/VS2010/Boogie/BoogieLanguageService/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..118d4488 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Properties/AssemblyInfo.cs @@ -0,0 +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")]
+
+
+
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Resources.Designer.cs b/Util/VS2010/Boogie/BoogieLanguageService/Resources.Designer.cs new file mode 100644 index 00000000..1b30575c --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Resources.Designer.cs @@ -0,0 +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;
+ }
+ }
+ }
+}
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Resources.resx b/Util/VS2010/Boogie/BoogieLanguageService/Resources.resx new file mode 100644 index 00000000..03fef612 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Resources.resx @@ -0,0 +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" />
+</root>
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Resources/Irony.dll b/Util/VS2010/Boogie/BoogieLanguageService/Resources/Irony.dll Binary files differnew file mode 100644 index 00000000..e2021a72 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/Resources/Irony.dll diff --git a/Util/VS2010/Boogie/BoogieLanguageService/VSPackage.resx b/Util/VS2010/Boogie/BoogieLanguageService/VSPackage.resx new file mode 100644 index 00000000..17dae8cb --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/VSPackage.resx @@ -0,0 +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>
+</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 new file mode 100644 index 00000000..a6528172 --- /dev/null +++ b/Util/VS2010/Boogie/BoogieLanguageService/source.extension.vsixmanifest @@ -0,0 +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>
diff --git a/Util/VS2010/Boogie/DafnyLanguageService.suo b/Util/VS2010/Boogie/DafnyLanguageService.suo Binary files differnew file mode 100644 index 00000000..aef52746 --- /dev/null +++ b/Util/VS2010/Boogie/DafnyLanguageService.suo diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs index 8615eee7..2eb57f11 100644 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs @@ -7,9 +7,8 @@ namespace Demo {
public static partial class Configuration
{
- public const string Name = "My C";
-// public const string FormatList = "My C File (*.myc)\n*.myc";
- public const string FormatList = "My C File (*.chalice)\n*.chalice";
+ public const string Name = "Chalice";
+ public const string FormatList = "Chalice File (*.chalice)\n*.chalice";
static Configuration()
{
diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs index 56f53c28..7a856d36 100644 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs @@ -5,7 +5,7 @@ using Irony.Parsing; namespace Demo
{
- [Language("My C", "1.0", "My C Programming Language")]
+ [Language("Chalice", "1.0", "Chalice Programming Language")]
public class Grammar : Irony.Parsing.Grammar
{
public Grammar() {
@@ -74,10 +74,12 @@ namespace Demo NonTerminal NewStmt = new NonTerminal("NewStmt");
NonTerminal NewArrStmt = new NonTerminal("NewArrStmt");
NonTerminal QualifiedName = new NonTerminal("QualifiedName");
+ NonTerminal AccessQualName = new NonTerminal("AccessQualName");
NonTerminal GenericsPostfix = new NonTerminal("GenericsPostfix");
NonTerminal ArrayExpression = new NonTerminal("ArrayExpression");
NonTerminal FunctionExpression = new NonTerminal("FunctionExpression");
NonTerminal selectExpr = new NonTerminal("selectExpr");
+ NonTerminal accessExpr = new NonTerminal("accessExpr");
#endregion
#region 2.3 Statement
@@ -125,6 +127,7 @@ namespace Demo #region 3.1 Expressions
selectExpr.Rule = (ToTerm("this") + ".").Q() + QualifiedName;
+ accessExpr.Rule = (ToTerm("this") + ".").Q() + AccessQualName;
evalstate.Rule =
ident + ToTerm(".") +
(ToTerm("acquire")
@@ -159,7 +162,7 @@ namespace Demo | LMb + declaration.Star() + RMb
| LParen + expression + RParen
| ToTerm("unfolding") + expression + "in" + expression
- | ToTerm("acc") + "(" + selectExpr + (("," + expression) | Empty) + ")"
+ | ToTerm("acc") + "(" + accessExpr + (("," + expression) | Empty) + ")"
| ToTerm("old") + "(" + expression + ")"
| ToTerm("eval") + "(" + evalstate + "," + expression + ")"
| ToTerm("credit") + "(" + expression + "," + expression + ")"
@@ -167,7 +170,7 @@ namespace Demo | expression + PreferShiftHere() + "?" + expression + ":" + expression
| ToTerm("rd") +
(ToTerm("holds") + "(" + expression + ")"
- | "(" + selectExpr + rdPermArg.Q() + ")"
+ | "(" + accessExpr + rdPermArg.Q() + ")"
)
;
@@ -196,6 +199,7 @@ namespace Demo FunctionExpression.Rule = QualifiedName + LParen + expressionList.Q() + RParen;
QualifiedName.Rule = ident | QualifiedName + dot + ident;
+ AccessQualName.Rule = ident | "*" | QualifiedName + dot + (ident | "*");
GenericsPostfix.Rule = less + QualifiedName + greater;
@@ -256,6 +260,8 @@ namespace Demo | "assert" + expression + Semi
| "assume" + expression + Semi
| "unshare" + expression + Semi
+ | "lock" + Condition + Statement
+ | "[[" + Statements + "]]"
| "acquire" + expression + Semi
| "release" + expression + Semi
| "downgrade" + expression + Semi
diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs b/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs index 5c475d35..8b9cb825 100644 --- a/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs +++ b/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs @@ -53,7 +53,7 @@ namespace Demo // 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", "My C", "Demo", 104)]
+ [ProvideLoadKey("Standard", "1.0", "Chalice", "Demo", 104)]
[Guid(GuidList.guidIronyLanguageServicePkgString)]
public sealed class MyCLanguageService : IronyPackage
{
diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx b/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx index c4e76be7..4c4adabd 100644 --- a/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx +++ b/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx @@ -121,9 +121,9 @@ <value>Paste PLK Here</value>
</data>
<data name="110" xml:space="preserve">
- <value>My C</value>
+ <value>Chalice</value>
</data>
<data name="112" xml:space="preserve">
- <value>My C Programming Language</value>
+ <value>Chalice Programming Language</value>
</data>
</root>
\ No newline at end of file diff --git a/Util/VS2010/Chalice/StartChalice.bat b/Util/VS2010/Chalice/StartChalice.bat index 8e066298..d91322ba 100644 --- a/Util/VS2010/Chalice/StartChalice.bat +++ b/Util/VS2010/Chalice/StartChalice.bat @@ -3,7 +3,7 @@ echo ---------- Starting ------------ < nul >> c:\tmp\coo.out time < nul >> c:\tmp\coo.out
echo. < nul >> c:\tmp\coo.out
-call "c:\Program Files\Scala\bin\scala" -cp c:\boogie\Chalice\bin Chalice -nologo -vs -noDeadlockChecks %* 2>> c:\tmp\coo.out
+call "c:\Program Files\Scala\bin\scala" -cp c:\boogie\Chalice\bin Chalice -nologo -vs %* 2>> c:\tmp\coo.out
time < nul >> c:\tmp\coo.out
echo. < nul >> c:\tmp\coo.out
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 8853ca9c..0a45490f 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -14,7 +14,7 @@ namespace Demo IdentifierTerminal ident = new IdentifierTerminal("Identifier");
this.MarkReservedWords(
- "class", "ghost", "static", "var", "const", "method", "datatype",
+ "class", "ghost", "static", "var", "method", "datatype",
"assert", "assume", "new", "this", "object", "refines", "replaces", "by",
"unlimited", "module", "imports",
"call", "if", "then", "else", "while", "invariant",
@@ -244,7 +244,6 @@ namespace Demo | QualifiedName + ":=" + Rhs
| "var" + localVarStmt
- | "const" + localVarStmt
| "call" + identList + ":=" + FunctionExpression + Semi
| "call" + FunctionExpression + Semi
@@ -284,7 +283,6 @@ namespace Demo | "ghost"
| "static"
| "var"
- | "const"
| "method"
| "datatype"
| "assert"
|