diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-07-09 19:54:24 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-07-09 19:54:24 -0700 |
| commit | 7b48f00c8170cb1f5e83851754efbf667d5a5883 (patch) | |
| tree | f9bb83158db97639f7aa4991cad054c72764bf43 /Source | |
| parent | d96c9e3ca3eca81e35821261bdb1fee446f8013e (diff) | |
async call return value is either int or bv32
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 825efa21..def13f7d 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1915,8 +1915,8 @@ namespace Microsoft.Boogie { if (QKeyValue.FindBoolAttribute(this.Attributes, "async") && Outs.Count > 0) {
Type returnType = cce.NonNull(Outs[0]).ShallowType;
- if (!returnType.Equals(Type.Int)) {
- tc.Error(this.tok, "the return from an asynchronous call should be an integer");
+ 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;
}
}
|