summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
authorGravatar Michal Moskal <michal@moskal.me>2011-08-29 13:33:41 -0700
committerGravatar Michal Moskal <michal@moskal.me>2011-08-29 13:33:41 -0700
commita05a61954d80ea118242c66d333fc14395e37fcf (patch)
treedb12ac0063e4d4afbb0ced10287343b1d5ea089b /Source/Core
parentebe61ada7635676fafa7d751e2472d69bd46afa8 (diff)
parentcc5adc60a5142e9381576238d2b8ba2e5d525dbd (diff)
Merge
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/AbsyCmd.cs5
1 files changed, 4 insertions, 1 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 7a79dfe7..b0c7cdb6 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1916,7 +1916,10 @@ namespace Microsoft.Boogie {
}
if (QKeyValue.FindBoolAttribute(this.Attributes, "async") && Outs.Count > 0) {
- Type returnType = cce.NonNull(Outs[0]).ShallowType;
+ Type returnType = null;
+ if (Outs[0] == null && Proc.OutParams.Length > 0) returnType = Proc.OutParams[0].TypedIdent.Type;
+ else returnType = Outs[0].ShallowType;
+ //Type returnType = cce.NonNull(Outs[0]).ShallowType;
if (!returnType.Equals(Type.Int) && !returnType.Equals(Type.GetBvType(32))) {
tc.Error(this.tok, "the return from an asynchronous call should be either int or bv32");
return;