diff options
| author |  Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-08-24 13:34:36 +0530 |
|---|---|---|
| committer | Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-08-24 13:34:36 +0530 |
| commit | 2464129db73236adf010b480eeac5bf14a681de0 (patch) | |
| tree | 4b36022d6a27cf288ae9f0641b6f14a20e2e8ce8 /Source | |
| parent | 64b57a073afe03ab57d99c96ef6994b77f786d0e (diff) | |
Fixed a bug with "don't care" return value on an async call
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 5 |
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;
|