diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-09 18:26:38 -0800 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-09 18:26:38 -0800 |
| commit | a7272a59b64944f0d9b288c0d36f346499906c18 (patch) | |
| tree | 208748907b59643b98365ce79e117ca29a0fa0d5 /Source | |
| parent | 68f2b9caf8b5d64399eb8e74daf75788bec74e4f (diff) | |
Boogie: map the given filename stdin.bpl to standard input
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/BoogiePL.atg | 32 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 33 |
2 files changed, 36 insertions, 29 deletions
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 33172e7f..c7465d81 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -35,26 +35,30 @@ static StructuredCmd/*!*/ dummyStructuredCmd = new BreakCmd(Token.NoToken, null) ///the parsed program.
///</summary>
public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
-Contract.Requires(filename != null);
-Contract.Requires(cce.NonNullElements(defines,true));
+ Contract.Requires(filename != null);
+ Contract.Requires(cce.NonNullElements(defines,true));
+ if (defines == null) {
+ defines = new List<string/*!*/>();
+ }
- FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);
- var ret = Parse(stream, filename, defines, out program);
- stream.Close();
- return ret;
+ if (filename == "stdin.bpl") {
+ var s = ParserHelper.Fill(Console.In, defines);
+ return Parse(s, filename, out program);
+ } else {
+ FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);
+ var s = ParserHelper.Fill(stream, defines);
+ var ret = Parse(s, filename, out program);
+ stream.Close();
+ return ret;
+ }
}
-public static int Parse (Stream stream, string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
-Contract.Requires(stream != null);
-Contract.Requires(filename != null);
-Contract.Requires(cce.NonNullElements(defines,true));
+public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
+ Contract.Requires(s != null);
+ Contract.Requires(filename != null);
- if (defines == null) {
- defines = new List<string/*!*/>();
- }
- string s = ParserHelper.Fill(stream, defines);
byte[]/*!*/ buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Errors errors = new Errors();
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index fe77bcc1..331a7cb9 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -54,26 +54,30 @@ static StructuredCmd/*!*/ dummyStructuredCmd = new BreakCmd(Token.NoToken, null) ///the parsed program.
///</summary>
public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
-Contract.Requires(filename != null);
-Contract.Requires(cce.NonNullElements(defines,true));
+ Contract.Requires(filename != null);
+ Contract.Requires(cce.NonNullElements(defines,true));
+ if (defines == null) {
+ defines = new List<string/*!*/>();
+ }
- FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);
- var ret = Parse(stream, filename, defines, out program);
- stream.Close();
- return ret;
+ if (filename == "stdin.bpl") {
+ var s = ParserHelper.Fill(Console.In, defines);
+ return Parse(s, filename, out program);
+ } else {
+ FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);
+ var s = ParserHelper.Fill(stream, defines);
+ var ret = Parse(s, filename, out program);
+ stream.Close();
+ return ret;
+ }
}
-public static int Parse (Stream stream, string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
-Contract.Requires(stream != null);
-Contract.Requires(filename != null);
-Contract.Requires(cce.NonNullElements(defines,true));
+public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
+ Contract.Requires(s != null);
+ Contract.Requires(filename != null);
- if (defines == null) {
- defines = new List<string/*!*/>();
- }
- string s = ParserHelper.Fill(stream, defines);
byte[]/*!*/ buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Errors errors = new Errors();
@@ -85,7 +89,6 @@ Contract.Requires(cce.NonNullElements(defines,true)); if (parser.errors.count == 0)
{
program = Pgm;
- program.ProcessDatatypeConstructors();
return 0;
}
else
|