From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/ParserHelper/ParserHelper.cs | 486 ++++++++++++++++++------------------ 1 file changed, 243 insertions(+), 243 deletions(-) (limited to 'Source/ParserHelper/ParserHelper.cs') diff --git a/Source/ParserHelper/ParserHelper.cs b/Source/ParserHelper/ParserHelper.cs index 111b836b..81644b7f 100644 --- a/Source/ParserHelper/ParserHelper.cs +++ b/Source/ParserHelper/ParserHelper.cs @@ -1,244 +1,244 @@ -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 readonly IToken/*!*/ NoToken = new Token(); - - public Token() { - this._val = "anything so that it is nonnull"; - } - public Token(int linenum, int colnum) - : base() { - this._line = linenum; - this._col = colnum; - this._val = "anything so that it is nonnull"; - } - - 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(); - } - } +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 readonly IToken/*!*/ NoToken = new Token(); + + public Token() { + this._val = "anything so that it is nonnull"; + } + public Token(int linenum, int colnum) + : base() { + this._line = linenum; + this._col = colnum; + this._val = "anything so that it is nonnull"; + } + + 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 -- cgit v1.2.3