1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
using System.Text;
using System.Collections.Generic;
using System.IO;
namespace Microsoft.Boogie {
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(FileStream! fileStream, List<string!>! defines) {
StreamReader! reader = new StreamReader(fileStream);
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();
}
}
}
|
