diff options
| -rw-r--r-- | Source/Core/BoogiePL.atg | 6 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 8 |
2 files changed, 10 insertions, 4 deletions
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index f65b7ca7..aed741d8 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -786,6 +786,7 @@ WhileCmd<out WhileCmd/*!*/ wcmd> Expr guard; Expr/*!*/ e; bool isFree;
List<PredicateCmd/*!*/> invariants = new List<PredicateCmd/*!*/>();
StmtList/*!*/ body;
+ QKeyValue kv = null;
.)
"while" (. x = t; .)
Guard<out guard> (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
@@ -793,10 +794,11 @@ WhileCmd<out WhileCmd/*!*/ wcmd> [ "free" (. isFree = true; .)
]
"invariant"
+ { 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));
}
.)
";"
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 8a63294c..5a6f8098 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -1093,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;
@@ -1105,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);
|