summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2010-03-07 05:40:08 +0000
committerGravatar qadeer <unknown>2010-03-07 05:40:08 +0000
commit6f2decb05072bd5eb8df120434ba322d60ed4f61 (patch)
treefeff2739de9d4c86acd98fccc2b09153bef5cd68
parent32cbfecc4c0c69d94fc5972ddc97f4c5972a23c4 (diff)
added attributes to CallForallCmd as well
-rw-r--r--Source/Core/AbsyCmd.ssc9
-rw-r--r--Source/Core/BoogiePL.atg2
-rw-r--r--Source/Core/Parser.ssc2
3 files changed, 11 insertions, 2 deletions
diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc
index 72ffba95..a546d9c7 100644
--- a/Source/Core/AbsyCmd.ssc
+++ b/Source/Core/AbsyCmd.ssc
@@ -1755,12 +1755,21 @@ namespace Microsoft.Boogie
// actual non-wildcard arguments
public TypeSeq InstantiatedTypes;
+ public QKeyValue Attributes;
+
public CallForallCmd(IToken! tok, string! callee, List<Expr>! ins)
: base(tok)
{
this.callee = callee;
this.Ins = ins;
}
+ public CallForallCmd(IToken! tok, string! callee, List<Expr>! ins, QKeyValue kv)
+ : base(tok)
+ {
+ this.callee = callee;
+ this.Ins = ins;
+ this.Attributes = kv;
+ }
public override void Emit(TokenTextWriter! stream, int level)
{
stream.Write(this, level, "call forall ");
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 495b1263..aded331b 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -953,7 +953,7 @@ CallCmd<out Cmd! c>
{ "," CallForallArg<out en> (. args.Add(en); .)
}
]
- ")" (. c = new CallForallCmd(x, first.val, args); .)
+ ")" (. c = new CallForallCmd(x, first.val, args, kv); .)
| "*"
(. ids.Add(null); .)
[ "," CallOutIdent<out p> (.
diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc
index 9202e204..60b441cf 100644
--- a/Source/Core/Parser.ssc
+++ b/Source/Core/Parser.ssc
@@ -1244,7 +1244,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
}
}
Expect(9);
- c = new CallForallCmd(x, first.val, args);
+ c = new CallForallCmd(x, first.val, args, kv);
} else if (t.kind == 44) {
Get();
ids.Add(null);