diff options
Diffstat (limited to 'Source/Core/ParserHelper.ssc')
| -rw-r--r-- | Source/Core/ParserHelper.ssc | 188 |
1 files changed, 0 insertions, 188 deletions
diff --git a/Source/Core/ParserHelper.ssc b/Source/Core/ParserHelper.ssc deleted file mode 100644 index 67cd261a..00000000 --- a/Source/Core/ParserHelper.ssc +++ /dev/null @@ -1,188 +0,0 @@ -using System.Text;
-using System.Collections.Generic;
-using System.IO;
-using Microsoft.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();
-
- public Token() {
- this._val = "anything so that it is nonnull";
- }
- public Token(int linenum, int colnum) {
- 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) {
- 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) {
- StreamReader! reader = new StreamReader(stream);
- return Fill(reader, defines);
- }
- public static string! Fill(TextReader! reader, List<string!>! defines) {
- 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
- //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
- //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 |