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/Core/OOLongUtil.cs | 420 +++++++++++++++++++++++----------------------- 1 file changed, 210 insertions(+), 210 deletions(-) (limited to 'Source/Core/OOLongUtil.cs') diff --git a/Source/Core/OOLongUtil.cs b/Source/Core/OOLongUtil.cs index 0d7bfc35..767b64a1 100644 --- a/Source/Core/OOLongUtil.cs +++ b/Source/Core/OOLongUtil.cs @@ -1,210 +1,210 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Collections.Generic; -using System.IO; -using System.Diagnostics.Contracts; - -namespace Boogie.Util { - public class TeeWriter : TextWriter { - readonly TextWriter/*!*/ a; - readonly TextWriter/*!*/ b; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(a != null); - Contract.Invariant(b != null); - } - - - public TeeWriter(TextWriter a, TextWriter b) { - Contract.Requires(b != null); - Contract.Requires(a != null); - this.a = a; - this.b = b; - } - - public override System.Text.Encoding Encoding { - get { - return a.Encoding; - } - } - - public override void Close() { - a.Close(); - b.Close(); - } - - public override void Flush() { - a.Flush(); - b.Flush(); - } - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - return ""; - } - - public override void Write(char ch) { - a.Write(ch); - b.Write(ch); - } - - public override void Write(string s) { - a.Write(s); - b.Write(s); - } - } - - /// - /// A LineReader is a class that allows further subclasses to just override the ReadLine() method. - /// It simply reads from the given "reader". - /// - public class LineReader : TextReader { - [Rep] - readonly TextReader/*!*/ reader; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(reader != null); - Contract.Invariant(readAhead == null || (0 <= readAheadConsumed && readAheadConsumed < readAhead.Length)); - } - - string readAhead; - int readAheadConsumed; - - - public LineReader([Captured] TextReader reader) { - Contract.Requires(reader != null); - this.reader = reader; - } - public override void Close() { - cce.BeginExpose(this); - { - reader.Close(); - } - cce.EndExpose(); - } - public override int Read() { - cce.BeginExpose(this); - try { - while (readAhead == null) { - readAhead = reader.ReadLine(); - if (readAhead == null) { - // we're at EOF - return -1; - } else if (readAhead.Length > 0) { - readAheadConsumed = 0; - break; - } - } - int res = readAhead[readAheadConsumed++]; - if (readAheadConsumed == readAhead.Length) { - readAhead = null; - } - return res; - } finally { - cce.EndExpose(); - } - } - public override int Read(char[] buffer, int index, int count) { - - int n = 0; - for (; n < count; n++) { - int ch = Read(); - if (ch == -1) { - break; - } - buffer[index + n] = (char)ch; - } - return n; - } - public override string ReadLine() { - string res; - if (readAhead != null) { - cce.BeginExpose(this); - { - res = readAhead.Substring(readAheadConsumed); - readAhead = null; - } - cce.EndExpose(); - } else { - res = reader.ReadLine(); - } - return res; - } - } - - public class IfdefReader : LineReader { - [Rep] - readonly List/*!*/ defines; - [Rep] - readonly List/*!*/ readState = new List(); - int ignoreCutoff = 0; // 0 means we're not ignoring - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(readState != null); - Contract.Invariant(cce.NonNullElements(defines)); - Contract.Invariant(0 <= ignoreCutoff && ignoreCutoff <= readState.Count); - } - - - - public IfdefReader([Captured] TextReader reader, [Captured] List/*!*/ defines) - : base(reader) { - Contract.Requires(reader != null); - Contract.Requires(cce.NonNullElements(defines)); - this.defines = defines; - } - - public override string ReadLine() { - while (true) { - string s = base.ReadLine(); - if (s == null) { - return s; - } - string t = s.Trim(); - if (t.StartsWith("#if")) { - string arg = t.Substring(3).TrimStart(); - bool sense = true; - while (t.StartsWith("!")) { - sense = !sense; - t = t.Substring(1).TrimStart(); - } - // push "true", since we're in a "then" branch - readState.Add(true); - if (ignoreCutoff == 0 && defines.Contains(arg) != sense) { - ignoreCutoff = readState.Count; // start ignoring - } - } else if (t == "#else") { - if (readState.Count == 0 || !readState[readState.Count - 1]) { - return s; // malformed input; return the read line as if it were not special - } - // change the "true" to a "false" on top of the state, since we're now going into the "else" branch - readState[readState.Count - 1] = false; - if (ignoreCutoff == 0) { - // the "then" branch had been included, so we'll ignore the "else" branch - ignoreCutoff = readState.Count; - } else if (ignoreCutoff == readState.Count) { - // we had ignored the "then" branch, so we'll include the "else" branch - ignoreCutoff = 0; - } - } else if (t == "#endif") { - if (readState.Count == 0) { - return s; // malformed input; return the read line as if it were not special - } - if (ignoreCutoff == readState.Count) { - // we had ignored the branch that ends here; so, now we start including again - ignoreCutoff = 0; - } - // pop - readState.RemoveAt(readState.Count - 1); - } else if (ignoreCutoff == 0) { - return s; - } - } - } - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Collections.Generic; +using System.IO; +using System.Diagnostics.Contracts; + +namespace Boogie.Util { + public class TeeWriter : TextWriter { + readonly TextWriter/*!*/ a; + readonly TextWriter/*!*/ b; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(a != null); + Contract.Invariant(b != null); + } + + + public TeeWriter(TextWriter a, TextWriter b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + this.a = a; + this.b = b; + } + + public override System.Text.Encoding Encoding { + get { + return a.Encoding; + } + } + + public override void Close() { + a.Close(); + b.Close(); + } + + public override void Flush() { + a.Flush(); + b.Flush(); + } + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result() != null); + return ""; + } + + public override void Write(char ch) { + a.Write(ch); + b.Write(ch); + } + + public override void Write(string s) { + a.Write(s); + b.Write(s); + } + } + + /// + /// A LineReader is a class that allows further subclasses to just override the ReadLine() method. + /// It simply reads from the given "reader". + /// + public class LineReader : TextReader { + [Rep] + readonly TextReader/*!*/ reader; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(reader != null); + Contract.Invariant(readAhead == null || (0 <= readAheadConsumed && readAheadConsumed < readAhead.Length)); + } + + string readAhead; + int readAheadConsumed; + + + public LineReader([Captured] TextReader reader) { + Contract.Requires(reader != null); + this.reader = reader; + } + public override void Close() { + cce.BeginExpose(this); + { + reader.Close(); + } + cce.EndExpose(); + } + public override int Read() { + cce.BeginExpose(this); + try { + while (readAhead == null) { + readAhead = reader.ReadLine(); + if (readAhead == null) { + // we're at EOF + return -1; + } else if (readAhead.Length > 0) { + readAheadConsumed = 0; + break; + } + } + int res = readAhead[readAheadConsumed++]; + if (readAheadConsumed == readAhead.Length) { + readAhead = null; + } + return res; + } finally { + cce.EndExpose(); + } + } + public override int Read(char[] buffer, int index, int count) { + + int n = 0; + for (; n < count; n++) { + int ch = Read(); + if (ch == -1) { + break; + } + buffer[index + n] = (char)ch; + } + return n; + } + public override string ReadLine() { + string res; + if (readAhead != null) { + cce.BeginExpose(this); + { + res = readAhead.Substring(readAheadConsumed); + readAhead = null; + } + cce.EndExpose(); + } else { + res = reader.ReadLine(); + } + return res; + } + } + + public class IfdefReader : LineReader { + [Rep] + readonly List/*!*/ defines; + [Rep] + readonly List/*!*/ readState = new List(); + int ignoreCutoff = 0; // 0 means we're not ignoring + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(readState != null); + Contract.Invariant(cce.NonNullElements(defines)); + Contract.Invariant(0 <= ignoreCutoff && ignoreCutoff <= readState.Count); + } + + + + public IfdefReader([Captured] TextReader reader, [Captured] List/*!*/ defines) + : base(reader) { + Contract.Requires(reader != null); + Contract.Requires(cce.NonNullElements(defines)); + this.defines = defines; + } + + public override string ReadLine() { + while (true) { + string s = base.ReadLine(); + if (s == null) { + return s; + } + string t = s.Trim(); + if (t.StartsWith("#if")) { + string arg = t.Substring(3).TrimStart(); + bool sense = true; + while (t.StartsWith("!")) { + sense = !sense; + t = t.Substring(1).TrimStart(); + } + // push "true", since we're in a "then" branch + readState.Add(true); + if (ignoreCutoff == 0 && defines.Contains(arg) != sense) { + ignoreCutoff = readState.Count; // start ignoring + } + } else if (t == "#else") { + if (readState.Count == 0 || !readState[readState.Count - 1]) { + return s; // malformed input; return the read line as if it were not special + } + // change the "true" to a "false" on top of the state, since we're now going into the "else" branch + readState[readState.Count - 1] = false; + if (ignoreCutoff == 0) { + // the "then" branch had been included, so we'll ignore the "else" branch + ignoreCutoff = readState.Count; + } else if (ignoreCutoff == readState.Count) { + // we had ignored the "then" branch, so we'll include the "else" branch + ignoreCutoff = 0; + } + } else if (t == "#endif") { + if (readState.Count == 0) { + return s; // malformed input; return the read line as if it were not special + } + if (ignoreCutoff == readState.Count) { + // we had ignored the branch that ends here; so, now we start including again + ignoreCutoff = 0; + } + // pop + readState.RemoveAt(readState.Count - 1); + } else if (ignoreCutoff == 0) { + return s; + } + } + } + } +} -- cgit v1.2.3