From f08bf65f0c319ea266e75bf4ebb8448ab91d2ae8 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Thu, 2 Dec 2010 14:35:21 +0000 Subject: 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#. --- Binaries/..svnbridge/Microsoft.Contracts.dll | 1 + Binaries/Microsoft.Contracts.dll | Bin 0 -> 16384 bytes Source/AbsInt/AbsInt.csproj | 4 + Source/Boogie.sln | 20 ++ Source/BoogieDriver/BoogieDriver.csproj | 4 + .../CodeContractsExtender.csproj | 6 +- Source/Core/Core.csproj | 5 +- Source/Core/Makefile | 4 +- Source/Core/Parser.cs | 49 ++-- Source/Core/ParserHelper.cs | 250 --------------------- Source/Core/Scanner.cs | 102 +++++---- Source/Dafny/DafnyPipeline.csproj | 3 + Source/Dafny/Makefile | 4 +- Source/Dafny/Parser.cs | 49 ++-- Source/Dafny/Scanner.cs | 102 +++++---- Source/DafnyDriver/DafnyDriver.csproj | 4 + Source/ParserHelper/ParserHelper.cs | 250 +++++++++++++++++++++ Source/ParserHelper/ParserHelper.csproj | 92 ++++++++ Source/Provers/Isabelle/Isabelle.csproj | 4 + Source/Provers/Z3/Z3.csproj | 4 + Source/VCExpr/VCExpr.csproj | 4 + Source/VCGeneration/VCGeneration.csproj | 4 + 22 files changed, 565 insertions(+), 400 deletions(-) create mode 100644 Binaries/..svnbridge/Microsoft.Contracts.dll create mode 100644 Binaries/Microsoft.Contracts.dll delete mode 100644 Source/Core/ParserHelper.cs create mode 100644 Source/ParserHelper/ParserHelper.cs create mode 100644 Source/ParserHelper/ParserHelper.csproj diff --git a/Binaries/..svnbridge/Microsoft.Contracts.dll b/Binaries/..svnbridge/Microsoft.Contracts.dll new file mode 100644 index 00000000..08149303 --- /dev/null +++ b/Binaries/..svnbridge/Microsoft.Contracts.dll @@ -0,0 +1 @@ +svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/Microsoft.Contracts.dll b/Binaries/Microsoft.Contracts.dll new file mode 100644 index 00000000..fac85ccf Binary files /dev/null and b/Binaries/Microsoft.Contracts.dll differ diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj index 433195a6..1c416a97 100644 --- a/Source/AbsInt/AbsInt.csproj +++ b/Source/AbsInt/AbsInt.csproj @@ -130,6 +130,10 @@ {B230A69C-C466-4065-B9C1-84D80E76D802} Core + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + diff --git a/Source/Boogie.sln b/Source/Boogie.sln index afcb1262..3f459d16 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -35,6 +35,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ModelViewer", "ModelViewer\ EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "Model\Model.csproj", "{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}" EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ParserHelper", "ParserHelper\ParserHelper.csproj", "{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|.NET = Debug|.NET @@ -345,6 +347,24 @@ Global {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|x86.ActiveCfg = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|.NET.ActiveCfg = Debug|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.Build.0 = Debug|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|x86.ActiveCfg = Debug|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|.NET.ActiveCfg = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.ActiveCfg = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.Build.0 = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.Build.0 = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|x86.ActiveCfg = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|.NET.ActiveCfg = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.Build.0 = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.ActiveCfg = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index df548f1a..1becfe9e 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -132,6 +132,10 @@ {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} Graph + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + {435D5BD0-6F62-49F8-BB24-33E2257519AD} Isabelle diff --git a/Source/CodeContractsExtender/CodeContractsExtender.csproj b/Source/CodeContractsExtender/CodeContractsExtender.csproj index 48c5821e..d957cec7 100644 --- a/Source/CodeContractsExtender/CodeContractsExtender.csproj +++ b/Source/CodeContractsExtender/CodeContractsExtender.csproj @@ -10,7 +10,7 @@ Properties CodeContractsExtender CodeContractsExtender - v4.0 + v3.5 512 true ..\InterimKey.snk @@ -99,6 +99,10 @@ true + + False + ..\..\Binaries\Microsoft.Contracts.dll + 3.5 diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 625ab9b6..145d56e3 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -118,7 +118,6 @@ - @@ -146,6 +145,10 @@ {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} Graph + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + diff --git a/Source/Core/Makefile b/Source/Core/Makefile index a5061138..192a16db 100644 --- a/Source/Core/Makefile +++ b/Source/Core/Makefile @@ -1,11 +1,11 @@ -COCO = ..\..\Binaries\Coco.exe +COCO = Coco.exe # ############################################################################### # The frame files are no longer in this directory. They must be downloaded # from http://boogiepartners.codeplex.com/. Update the FRAME_DIR variable to # point to whatever directory you install that into. # ############################################################################### -FRAME_DIR = c:\BoogiePartners\CocoR\Modified +FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they # are both generated in one go and I don't know a better way to tell diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 0d906de4..7898e26f 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -30,7 +30,7 @@ public class Parser { const bool T = true; const bool x = false; const int minErrDist = 2; - + public Scanner/*!*/ scanner; public Errors/*!*/ errors; @@ -140,10 +140,10 @@ private class BvBounds : Expr { if (errDist >= minErrDist) errors.SemErr(t, msg); errDist = 0; } - - public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { - Contract.Requires(tok != null); - Contract.Requires(msg != null); + + public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); errors.SemErr(tok, msg); } @@ -156,15 +156,15 @@ private class BvBounds : Expr { la = t; } } - + void Expect (int n) { if (la.kind==n) Get(); else { SynErr(n); } } - + bool StartOf (int s) { return set[s, la.kind]; } - + void ExpectWeak (int n, int follow) { if (la.kind == n) Get(); else { @@ -188,7 +188,7 @@ private class BvBounds : Expr { } } - + void BoogiePL() { VariableSeq/*!*/ vs; DeclarationSeq/*!*/ ds; @@ -2004,13 +2004,13 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { public void Parse() { la = new Token(); - la.val = ""; + la.val = ""; Get(); BoogiePL(); - Expect(0); + Expect(0); } - + static readonly bool[,]/*!*/ set = { {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, @@ -2035,18 +2035,20 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { public class Errors { public int count = 0; // number of errors detected public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream - public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text - public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text - + public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text + public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text + public void SynErr(string filename, int line, int col, int n) { - SynErr(filename, line, col, GetSyntaxErrorString(n)); - } - public virtual void SynErr(string filename, int line, int col, string msg) { - Contract.Requires(msg != null); + SynErr(filename, line, col, GetSyntaxErrorString(n)); + } + + public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) { + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; - } - string GetSyntaxErrorString(int n) { + } + + string GetSyntaxErrorString(int n) { string s; switch (n) { case 0: s = "EOF expected"; break; @@ -2181,7 +2183,7 @@ public class Errors { default: s = "error " + n; break; } - return s; + return s; } public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors @@ -2189,8 +2191,9 @@ public class Errors { Contract.Requires(msg != null); SemErr(tok.filename, tok.line, tok.col, msg); } + public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) { - Contract.Requires(msg != null); + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; } diff --git a/Source/Core/ParserHelper.cs b/Source/Core/ParserHelper.cs deleted file mode 100644 index 465b9245..00000000 --- a/Source/Core/ParserHelper.cs +++ /dev/null @@ -1,250 +0,0 @@ -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/*!*/ 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/*!*/ defines) { - Contract.Requires(stream != null); - Contract.Requires(cce.NonNullElements(defines)); - Contract.Ensures(Contract.Result() != null); - StreamReader/*!*/ reader = new StreamReader(stream); - return Fill(reader, defines); - } - public static string Fill(TextReader reader, List/*!*/ defines) { - Contract.Requires(reader != null); - Contract.Requires(cce.NonNullElements(defines)); - Contract.Ensures(Contract.Result() != null); - StringBuilder sb = new StringBuilder(); - List/*!*/ readState = new List(); // 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/Core/Scanner.cs b/Source/Core/Scanner.cs index faab5837..7c3522ca 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -19,7 +19,7 @@ public class Buffer { // a) whole stream in buffer // b) part of stream in buffer // 2) non seekable stream (network, console) - + public const int EOF = 65535 + 1; // char.MaxValue + 1; const int MIN_BUFFER_LENGTH = 1024; // 1KB const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB @@ -31,15 +31,17 @@ public class Buffer { Stream/*!*/ stream; // input stream (seekable) bool isUserStream; // was the stream opened by the user? -[ContractInvariantMethod] -void ObjectInvariant(){ - Contract.Invariant(buf != null); - Contract.Invariant(stream != null);} - [NotDelayed] - public Buffer (Stream/*!*/ s, bool isUserStream) :base() { + [ContractInvariantMethod] + void ObjectInvariant(){ + Contract.Invariant(buf != null); + Contract.Invariant(stream != null); + } + +// [NotDelayed] + public Buffer (Stream/*!*/ s, bool isUserStream) : base() { Contract.Requires(s != null); stream = s; this.isUserStream = isUserStream; - + int fl, bl; if (s.CanSeek) { fl = (int) s.Length; @@ -51,12 +53,12 @@ void ObjectInvariant(){ buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH]; fileLen = fl; bufLen = bl; - + if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start) else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid if (bufLen == fileLen && s.CanSeek) Close(); } - + protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor Contract.Requires(b != null); buf = b.buf; @@ -73,14 +75,14 @@ void ObjectInvariant(){ } ~Buffer() { Close(); } - + protected void Close() { if (!isUserStream && stream != null) { stream.Close(); //stream = null; } } - + public virtual int Read () { if (bufPos < bufLen) { return buf[bufPos++]; @@ -100,7 +102,7 @@ void ObjectInvariant(){ Pos = curPos; return ch; } - + public string/*!*/ GetString (int beg, int end) { Contract.Ensures(Contract.Result() != null); int len = 0; @@ -139,7 +141,7 @@ void ObjectInvariant(){ } } } - + // Read the next chunk of bytes from the stream, increases the buffer // if needed and updates the fields fileLen and bufLen. // Returns the number of bytes read. @@ -213,19 +215,20 @@ public class Scanner { const int noSym = 88; -[ContractInvariantMethod] -void objectInvariant(){ - Contract.Invariant(buffer!=null); - Contract.Invariant(t != null); - Contract.Invariant(start != null); - Contract.Invariant(tokens != null); - Contract.Invariant(pt != null); - Contract.Invariant(tval != null); - Contract.Invariant(Filename != null); - Contract.Invariant(errorHandler != null); -} + [ContractInvariantMethod] + void objectInvariant(){ + Contract.Invariant(buffer!=null); + Contract.Invariant(t != null); + Contract.Invariant(start != null); + Contract.Invariant(tokens != null); + Contract.Invariant(pt != null); + Contract.Invariant(tval != null); + Contract.Invariant(Filename != null); + Contract.Invariant(errorHandler != null); + } + public Buffer/*!*/ buffer; // scanner buffer - + Token/*!*/ t; // current token int ch; // current input character int pos; // byte position of current character @@ -236,13 +239,13 @@ void objectInvariant(){ Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy) Token/*!*/ pt; // current peek token - + char[]/*!*/ tval = new char[128]; // text of current token int tlen; // length of current token - + private string/*!*/ Filename; private Errors/*!*/ errorHandler; - + static Scanner() { start = new Hashtable(128); for (int i = 35; i <= 36; ++i) start[i] = 2; @@ -291,9 +294,9 @@ void objectInvariant(){ start[Buffer.EOF] = -1; } - - [NotDelayed] - public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){ + +// [NotDelayed] + public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() { Contract.Requires(fileName != null); Contract.Requires(errorHandler != null); this.errorHandler = errorHandler; @@ -303,15 +306,14 @@ void objectInvariant(){ Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read); buffer = new Buffer(stream, false); Filename = fileName; - Init(); } catch (IOException) { throw new FatalError("Cannot open file " + fileName); } } - - [NotDelayed] - public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){ + +// [NotDelayed] + public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() { Contract.Requires(s != null); Contract.Requires(errorHandler != null); Contract.Requires(fileName != null); @@ -320,10 +322,9 @@ void objectInvariant(){ buffer = new Buffer(s, true); this.errorHandler = errorHandler; this.Filename = fileName; - Init(); } - + void Init() { pos = -1; line = 1; col = 0; oldEols = 0; @@ -344,11 +345,11 @@ void objectInvariant(){ Contract.Ensures(Contract.Result() != null); int p = buffer.Pos; int ch = buffer.Read(); - // replace isolated '\r' by '\n' in order to make + // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; while (ch != EOL && ch != Buffer.EOF){ - ch = buffer.Read(); + ch = buffer.Read(); // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; @@ -359,7 +360,7 @@ void objectInvariant(){ } void NextCh() { - if (oldEols > 0) { ch = EOL; oldEols--; } + if (oldEols > 0) { ch = EOL; oldEols--; } else { // pos = buffer.Pos; // ch = buffer.Read(); col++; @@ -367,9 +368,9 @@ void objectInvariant(){ // // eol handling uniform across Windows, Unix and Mac // if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; // if (ch == EOL) { line++; col = 0; } - + while (true) { - pos = buffer.Pos; + pos = buffer.Pos; ch = buffer.Read(); col++; // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac @@ -419,7 +420,7 @@ void objectInvariant(){ return; } - + } } @@ -539,10 +540,13 @@ void objectInvariant(){ t.pos = pos; t.col = col; t.line = line; t.filename = this.Filename; int state; - if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); } + if (start.ContainsKey(ch)) { + Contract.Assert(start[ch] != null); + state = (int) start[ch]; + } else { state = 0; } tlen = 0; AddCh(); - + switch (state) { case -1: { t.kind = eofSym; break; } // NextCh already done case 0: { @@ -711,14 +715,14 @@ void objectInvariant(){ t.val = new String(tval, 0, tlen); return t; } - + private void SetScannerBehindT() { buffer.Pos = t.pos; NextCh(); line = t.line; col = t.col; for (int i = 0; i < tlen; i++) NextCh(); } - + // get the next token (possibly a token already seen during peeking) public Token/*!*/ Scan () { Contract.Ensures(Contract.Result() != null); @@ -739,7 +743,7 @@ void objectInvariant(){ } pt = pt.next; } while (pt.kind > maxT); // skip pragmas - + return pt; } diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj index a4206998..7f063c2c 100644 --- a/Source/Dafny/DafnyPipeline.csproj +++ b/Source/Dafny/DafnyPipeline.csproj @@ -98,6 +98,9 @@ False ..\..\Binaries\Core.dll + + ..\..\Binaries\ParserHelper.dll + 3.5 diff --git a/Source/Dafny/Makefile b/Source/Dafny/Makefile index 3fc283a0..cc36590c 100644 --- a/Source/Dafny/Makefile +++ b/Source/Dafny/Makefile @@ -1,11 +1,11 @@ -COCO = ..\..\Binaries\Coco.exe +COCO = Coco.exe # ############################################################################### # The frame files are no longer in this directory. They must be downloaded # from http://boogiepartners.codeplex.com/. Update the FRAME_DIR variable to # point to whatever directory you install that into. # ############################################################################### -FRAME_DIR = c:\BoogiePartners\CocoR\Modified +FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they # are both generated in one go and I don't know a better way to tell diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 2dc77103..ff6f2690 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -25,7 +25,7 @@ public class Parser { const bool T = true; const bool x = false; const int minErrDist = 2; - + public Scanner/*!*/ scanner; public Errors/*!*/ errors; @@ -161,10 +161,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List= minErrDist) errors.SemErr(t, msg); errDist = 0; } - - public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { - Contract.Requires(tok != null); - Contract.Requires(msg != null); + + public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); errors.SemErr(tok, msg); } @@ -177,15 +177,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List theImports; @@ -2052,13 +2052,13 @@ List/*!*/ decreases) { public void Parse() { la = new Token(); - la.val = ""; + la.val = ""; Get(); Dafny(); - Expect(0); + Expect(0); } - + static readonly bool[,]/*!*/ set = { {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, @@ -2086,18 +2086,20 @@ List/*!*/ decreases) { public class Errors { public int count = 0; // number of errors detected public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream - public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text - public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text - + public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text + public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text + public void SynErr(string filename, int line, int col, int n) { - SynErr(filename, line, col, GetSyntaxErrorString(n)); - } - public virtual void SynErr(string filename, int line, int col, string msg) { - Contract.Requires(msg != null); + SynErr(filename, line, col, GetSyntaxErrorString(n)); + } + + public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) { + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; - } - string GetSyntaxErrorString(int n) { + } + + string GetSyntaxErrorString(int n) { string s; switch (n) { case 0: s = "EOF expected"; break; @@ -2249,7 +2251,7 @@ public class Errors { default: s = "error " + n; break; } - return s; + return s; } public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors @@ -2257,8 +2259,9 @@ public class Errors { Contract.Requires(msg != null); SemErr(tok.filename, tok.line, tok.col, msg); } + public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) { - Contract.Requires(msg != null); + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; } diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index de87c6ad..42c4f661 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -19,7 +19,7 @@ public class Buffer { // a) whole stream in buffer // b) part of stream in buffer // 2) non seekable stream (network, console) - + public const int EOF = 65535 + 1; // char.MaxValue + 1; const int MIN_BUFFER_LENGTH = 1024; // 1KB const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB @@ -31,15 +31,17 @@ public class Buffer { Stream/*!*/ stream; // input stream (seekable) bool isUserStream; // was the stream opened by the user? -[ContractInvariantMethod] -void ObjectInvariant(){ - Contract.Invariant(buf != null); - Contract.Invariant(stream != null);} - [NotDelayed] - public Buffer (Stream/*!*/ s, bool isUserStream) :base() { + [ContractInvariantMethod] + void ObjectInvariant(){ + Contract.Invariant(buf != null); + Contract.Invariant(stream != null); + } + +// [NotDelayed] + public Buffer (Stream/*!*/ s, bool isUserStream) : base() { Contract.Requires(s != null); stream = s; this.isUserStream = isUserStream; - + int fl, bl; if (s.CanSeek) { fl = (int) s.Length; @@ -51,12 +53,12 @@ void ObjectInvariant(){ buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH]; fileLen = fl; bufLen = bl; - + if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start) else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid if (bufLen == fileLen && s.CanSeek) Close(); } - + protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor Contract.Requires(b != null); buf = b.buf; @@ -73,14 +75,14 @@ void ObjectInvariant(){ } ~Buffer() { Close(); } - + protected void Close() { if (!isUserStream && stream != null) { stream.Close(); //stream = null; } } - + public virtual int Read () { if (bufPos < bufLen) { return buf[bufPos++]; @@ -100,7 +102,7 @@ void ObjectInvariant(){ Pos = curPos; return ch; } - + public string/*!*/ GetString (int beg, int end) { Contract.Ensures(Contract.Result() != null); int len = 0; @@ -139,7 +141,7 @@ void ObjectInvariant(){ } } } - + // Read the next chunk of bytes from the stream, increases the buffer // if needed and updates the fields fileLen and bufLen. // Returns the number of bytes read. @@ -213,19 +215,20 @@ public class Scanner { const int noSym = 103; -[ContractInvariantMethod] -void objectInvariant(){ - Contract.Invariant(buffer!=null); - Contract.Invariant(t != null); - Contract.Invariant(start != null); - Contract.Invariant(tokens != null); - Contract.Invariant(pt != null); - Contract.Invariant(tval != null); - Contract.Invariant(Filename != null); - Contract.Invariant(errorHandler != null); -} + [ContractInvariantMethod] + void objectInvariant(){ + Contract.Invariant(buffer!=null); + Contract.Invariant(t != null); + Contract.Invariant(start != null); + Contract.Invariant(tokens != null); + Contract.Invariant(pt != null); + Contract.Invariant(tval != null); + Contract.Invariant(Filename != null); + Contract.Invariant(errorHandler != null); + } + public Buffer/*!*/ buffer; // scanner buffer - + Token/*!*/ t; // current token int ch; // current input character int pos; // byte position of current character @@ -236,13 +239,13 @@ void objectInvariant(){ Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy) Token/*!*/ pt; // current peek token - + char[]/*!*/ tval = new char[128]; // text of current token int tlen; // length of current token - + private string/*!*/ Filename; private Errors/*!*/ errorHandler; - + static Scanner() { start = new Hashtable(128); for (int i = 39; i <= 39; ++i) start[i] = 1; @@ -291,9 +294,9 @@ void objectInvariant(){ start[Buffer.EOF] = -1; } - - [NotDelayed] - public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){ + +// [NotDelayed] + public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() { Contract.Requires(fileName != null); Contract.Requires(errorHandler != null); this.errorHandler = errorHandler; @@ -303,15 +306,14 @@ void objectInvariant(){ Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read); buffer = new Buffer(stream, false); Filename = fileName; - Init(); } catch (IOException) { throw new FatalError("Cannot open file " + fileName); } } - - [NotDelayed] - public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){ + +// [NotDelayed] + public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() { Contract.Requires(s != null); Contract.Requires(errorHandler != null); Contract.Requires(fileName != null); @@ -320,10 +322,9 @@ void objectInvariant(){ buffer = new Buffer(s, true); this.errorHandler = errorHandler; this.Filename = fileName; - Init(); } - + void Init() { pos = -1; line = 1; col = 0; oldEols = 0; @@ -344,11 +345,11 @@ void objectInvariant(){ Contract.Ensures(Contract.Result() != null); int p = buffer.Pos; int ch = buffer.Read(); - // replace isolated '\r' by '\n' in order to make + // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; while (ch != EOL && ch != Buffer.EOF){ - ch = buffer.Read(); + ch = buffer.Read(); // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; @@ -359,7 +360,7 @@ void objectInvariant(){ } void NextCh() { - if (oldEols > 0) { ch = EOL; oldEols--; } + if (oldEols > 0) { ch = EOL; oldEols--; } else { // pos = buffer.Pos; // ch = buffer.Read(); col++; @@ -367,9 +368,9 @@ void objectInvariant(){ // // eol handling uniform across Windows, Unix and Mac // if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; // if (ch == EOL) { line++; col = 0; } - + while (true) { - pos = buffer.Pos; + pos = buffer.Pos; ch = buffer.Read(); col++; // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac @@ -419,7 +420,7 @@ void objectInvariant(){ return; } - + } } @@ -555,10 +556,13 @@ void objectInvariant(){ t.pos = pos; t.col = col; t.line = line; t.filename = this.Filename; int state; - if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); } + if (start.ContainsKey(ch)) { + Contract.Assert(start[ch] != null); + state = (int) start[ch]; + } else { state = 0; } tlen = 0; AddCh(); - + switch (state) { case -1: { t.kind = eofSym; break; } // NextCh already done case 0: { @@ -765,14 +769,14 @@ void objectInvariant(){ t.val = new String(tval, 0, tlen); return t; } - + private void SetScannerBehindT() { buffer.Pos = t.pos; NextCh(); line = t.line; col = t.col; for (int i = 0; i < tlen; i++) NextCh(); } - + // get the next token (possibly a token already seen during peeking) public Token/*!*/ Scan () { Contract.Ensures(Contract.Result() != null); @@ -793,7 +797,7 @@ void objectInvariant(){ } pt = pt.next; } while (pt.kind > maxT); // skip pragmas - + return pt; } diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index 1ec5abb0..d577c048 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -97,6 +97,10 @@ False ..\Core\bin\Debug\Core.dll + + False + ..\..\Binaries\ParserHelper.dll + 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/*!*/ 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/*!*/ defines) { + Contract.Requires(stream != null); + Contract.Requires(cce.NonNullElements(defines)); + Contract.Ensures(Contract.Result() != null); + StreamReader/*!*/ reader = new StreamReader(stream); + return Fill(reader, defines); + } + public static string Fill(TextReader reader, List/*!*/ defines) { + Contract.Requires(reader != null); + Contract.Requires(cce.NonNullElements(defines)); + Contract.Ensures(Contract.Result() != null); + StringBuilder sb = new StringBuilder(); + List/*!*/ readState = new List(); // 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 @@ + + + + Debug + AnyCPU + 8.0.30703 + 2.0 + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + Library + Properties + ParserHelper + ParserHelper + v3.5 + 512 + + 1 + + + true + full + false + ..\..\Binaries\ + TRACE;DEBUG + prompt + 4 + False + True + False + True + False + True + True + True + True + True + True + True + False + False + + + + + + ..\..\baseline.xml + Full + %28none%29 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + + + true + + + ..\InterimKey.snk + + + + False + ..\..\Binaries\Microsoft.Contracts.dll + + + + + + + + + + + + + + {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} + CodeContractsExtender + + + + + \ No newline at end of file diff --git a/Source/Provers/Isabelle/Isabelle.csproj b/Source/Provers/Isabelle/Isabelle.csproj index b4087878..5279883a 100644 --- a/Source/Provers/Isabelle/Isabelle.csproj +++ b/Source/Provers/Isabelle/Isabelle.csproj @@ -124,6 +124,10 @@ {B230A69C-C466-4065-B9C1-84D80E76D802} Core + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} VCExpr diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj index 33b8ba7b..e67d7fb2 100644 --- a/Source/Provers/Z3/Z3.csproj +++ b/Source/Provers/Z3/Z3.csproj @@ -130,6 +130,10 @@ {B230A69C-C466-4065-B9C1-84D80E76D802} Core + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} VCExpr diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj index 116112a0..c712d6a1 100644 --- a/Source/VCExpr/VCExpr.csproj +++ b/Source/VCExpr/VCExpr.csproj @@ -135,6 +135,10 @@ {B230A69C-C466-4065-B9C1-84D80E76D802} Core + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj index 9906070a..1697156f 100644 --- a/Source/VCGeneration/VCGeneration.csproj +++ b/Source/VCGeneration/VCGeneration.csproj @@ -141,6 +141,10 @@ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} Model + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} VCExpr -- cgit v1.2.3