Factored out the ParserHelper class into a separate project and updated the files generated by Coco/R.

This was done to support sharing of the Coco/R .frame files with Spec#.

2 files changed, 342 insertions, 0 deletions

diff --git a/Source/ParserHelper/ParserHelper.cs b/Source/ParserHelper/ParserHelper.cs
new file mode 100644
index 00000000..465b9245
--- /dev/null
+++ b/Source/ParserHelper/ParserHelper.cs
@@ -0,0 +1,250 @@
+using System.Text;

+using System.Collections.Generic;

+using System.IO;

+using System.Diagnostics.Contracts;

+

+namespace Microsoft.Boogie {

+

+  [Immutable]

+  public interface IToken {

+    int kind {

+      get;

+      set;

+    }         // token kind

+    string filename {

+      get;

+      set;

+    }  // token file

+    int pos {

+      get;

+      set;

+    }          // token position in the source text (starting at 0)

+    int col {

+      get;

+      set;

+    }          // token column (starting at 0)

+    int line {

+      get;

+      set;

+    }         // token line (starting at 1)

+    string/*!*/ val {

+      get;

+      set;

+    }  // token value

+

+    bool IsValid {

+      get;

+    }

+  }

+

+  [Immutable]

+  public class Token : IToken {

+    public int _kind;    // token kind

+    string _filename;  // token file

+    public int _pos;     // token position in the source text (starting at 0)

+    public int _col;     // token column (starting at 1)

+    public int _line;    // token line (starting at 1)

+    public string/*!*/ _val;  // token value

+    public Token next;  // ML 2005-03-11 Tokens are kept in linked list

+

+    public static IToken/*!*/ NoToken = new Token();

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(NoToken != null);

+    }

+

+

+    public Token() {

+      this._val = "anything so that it is nonnull";

+    }

+    public Token(int linenum, int colnum)

+      : base() {//BASEMOVE DANGER

+      this._line = linenum;

+      this._col = colnum;

+      this._val = "anything so that it is nonnull";

+      //:base();

+    }

+

+    public int kind {

+      get {

+        return this._kind;

+      }

+      set {

+        this._kind = value;

+      }

+    }

+

+    public string filename {

+      get {

+        return this._filename;

+      }

+      set {

+        this._filename = value;

+      }

+    }

+

+    public int pos {

+      get {

+        return this._pos;

+      }

+      set {

+        this._pos = value;

+      }

+    }

+

+    public int col {

+      get {

+        return this._col;

+      }

+      set {

+        this._col = value;

+      }

+    }

+

+    public int line {

+      get {

+        return this._line;

+      }

+      set {

+        this._line = value;

+      }

+    }

+

+    public string/*!*/ val {

+      get {

+        return this._val;

+      }

+      set {

+        this._val = value;

+      }

+    }

+

+    public bool IsValid {

+      get {

+        return this._filename != null;

+      }

+    }

+

+

+  }

+

+  public static class ParserHelper {

+    struct ReadState {

+      public bool hasSeenElse;

+      public bool mayStillIncludeAnotherAlternative;

+      public ReadState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative) {

+        this.hasSeenElse = hasSeenElse;

+        this.mayStillIncludeAnotherAlternative = mayStillIncludeAnotherAlternative;

+      }

+    }

+    // "arg" is assumed to be trimmed

+    private static bool IfdefConditionSaysToInclude(string arg, List<string/*!*/>/*!*/ defines) {

+      Contract.Requires(arg != null);

+      Contract.Requires(cce.NonNullElements(defines));

+      bool sense = true;

+      while (arg.StartsWith("!")) {

+        sense = !sense;

+        arg = arg.Substring(1).TrimStart();

+      }

+      return defines.Contains(arg) == sense;

+    }

+

+    public static string Fill(Stream stream, List<string/*!*/>/*!*/ defines) {

+      Contract.Requires(stream != null);

+      Contract.Requires(cce.NonNullElements(defines));

+      Contract.Ensures(Contract.Result<string>() != null);

+      StreamReader/*!*/ reader = new StreamReader(stream);

+      return Fill(reader, defines);

+    }

+    public static string Fill(TextReader reader, List<string/*!*/>/*!*/ defines) {

+      Contract.Requires(reader != null);

+      Contract.Requires(cce.NonNullElements(defines));

+      Contract.Ensures(Contract.Result<string>() != null);

+      StringBuilder sb = new StringBuilder();

+      List<ReadState>/*!*/ readState = new List<ReadState>();  // readState.Count is the current nesting level of #if's

+      int ignoreCutoff = -1;  // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n

+      while (true)

+      //invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count;

+    {

+        string s = reader.ReadLine();

+        if (s == null) {

+          if (readState.Count != 0) {

+            sb.AppendLine("#MalformedInput: missing #endif");

+          }

+          break;

+        }

+        string t = s.Trim();

+        if (t.StartsWith("#if")) {

+          ReadState rs = new ReadState(false, false);

+          if (ignoreCutoff != -1) {

+            // we're already in a state of ignoring, so continue to ignore

+          } else if (IfdefConditionSaysToInclude(t.Substring(3).TrimStart(), defines)) {

+            // include this branch

+          } else {

+            ignoreCutoff = readState.Count;  // start ignoring

+            rs.mayStillIncludeAnotherAlternative = true;  // allow some later "elsif" or "else" branch to be included

+          }

+          readState.Add(rs);

+          sb.AppendLine();  // ignore the #if line

+

+        } else if (t.StartsWith("#elsif")) {

+          ReadState rs;

+          if (readState.Count == 0 || (rs = readState[readState.Count - 1]).hasSeenElse) {

+            sb.AppendLine("#MalformedInput: misplaced #elsif");  // malformed input

+            break;

+          }

+          if (ignoreCutoff == -1) {

+            // we had included the previous branch

+            //Contract.Assert(!rs.mayStillIncludeAnotherAlternative);

+            ignoreCutoff = readState.Count - 1;  // start ignoring

+          } else if (rs.mayStillIncludeAnotherAlternative && IfdefConditionSaysToInclude(t.Substring(6).TrimStart(), defines)) {

+            // include this branch, but no subsequent branch at this level

+            ignoreCutoff = -1;

+            rs.mayStillIncludeAnotherAlternative = false;

+            readState[readState.Count - 1] = rs;

+          }

+          sb.AppendLine();  // ignore the #elsif line

+

+        } else if (t == "#else") {

+          ReadState rs;

+          if (readState.Count == 0 || (rs = readState[readState.Count - 1]).hasSeenElse) {

+            sb.AppendLine("#MalformedInput: misplaced #else");  // malformed input

+            break;

+          }

+          rs.hasSeenElse = true;

+          if (ignoreCutoff == -1) {

+            // we had included the previous branch

+            //Contract.Assert(!rs.mayStillIncludeAnotherAlternative);

+            ignoreCutoff = readState.Count - 1;  // start ignoring

+          } else if (rs.mayStillIncludeAnotherAlternative) {

+            // include this branch

+            ignoreCutoff = -1;

+            rs.mayStillIncludeAnotherAlternative = false;

+          }

+          readState[readState.Count - 1] = rs;

+          sb.AppendLine();  // ignore the #else line

+

+        } else if (t == "#endif") {

+          if (readState.Count == 0) {

+            sb.AppendLine("#MalformedInput: misplaced #endif");  // malformed input

+            break;

+          }

+          readState.RemoveAt(readState.Count - 1);  // pop

+          if (ignoreCutoff == readState.Count) {

+            // we had ignored the branch that ends here; so, now we start including again

+            ignoreCutoff = -1;

+          }

+          sb.AppendLine();  // ignore the #endif line

+

+        } else if (ignoreCutoff == -1) {

+          sb.AppendLine(s);  // included line

+

+        } else {

+          sb.AppendLine();  // ignore the line

+        }

+      }

+

+      return sb.ToString();

+    }

+  }

+}
\ No newline at end of file
diff --git a/Source/ParserHelper/ParserHelper.csproj b/Source/ParserHelper/ParserHelper.csproj
new file mode 100644
index 00000000..405a3d75
--- /dev/null
+++ b/Source/ParserHelper/ParserHelper.csproj
@@ -0,0 +1,92 @@
+<?xml version="1.0" encoding="utf-8"?>

+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

+  <PropertyGroup>

+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

+    <ProductVersion>8.0.30703</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>ParserHelper</RootNamespace>

+    <AssemblyName>ParserHelper</AssemblyName>

+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+    <TargetFrameworkProfile />

+    <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>..\..\Binaries\</OutputPath>

+    <DefineConstants>TRACE;DEBUG</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>True</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>False</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>True</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>

+    <CodeContractsContainerAnalysis>True</CodeContractsContainerAnalysis>

+    <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly />

+    <CodeContractsCustomRewriterClass />

+    <CodeContractsLibPaths />

+    <CodeContractsExtraRewriteOptions />

+    <CodeContractsExtraAnalysisOptions />

+    <CodeContractsBaseLineFile>..\..\baseline.xml</CodeContractsBaseLineFile>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

+  </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>

+  </PropertyGroup>

+  <PropertyGroup>

+    <SignAssembly>true</SignAssembly>

+  </PropertyGroup>

+  <PropertyGroup>

+    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\Microsoft.Contracts.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

+    <Reference Include="System.Core" />

+    <Reference Include="System.Xml.Linq" />

+    <Reference Include="System.Data.DataSetExtensions" />

+    <Reference Include="System.Data" />

+    <Reference Include="System.Xml" />

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="ParserHelper.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.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