1 files changed, 24 insertions, 16 deletions
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index fe77bcc1..5a6f8098 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();
@@ -1089,6 +1093,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		Expr guard;  Expr/*!*/ e;  bool isFree;
 		List<PredicateCmd/*!*/> invariants = new List<PredicateCmd/*!*/>();
 		StmtList/*!*/ body;
+		QKeyValue kv = null;
 		
 		Expect(40);
 		x = t; 
@@ -1101,11 +1106,14 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				isFree = true;  
 			}
 			Expect(41);
+			while (la.kind == 25) {
+				Attribute(ref kv);
+			}
 			Expression(out e);
 			if (isFree) {
-			 invariants.Add(new AssumeCmd(z, e));
+			 invariants.Add(new AssumeCmd(z, e, kv));
 			} else {
-			 invariants.Add(new AssertCmd(z, e));
+			 invariants.Add(new AssertCmd(z, e, kv));
 			}
 			
 			Expect(7);