diff options
| author |  qadeer <unknown> | 2014-07-11 14:00:32 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-07-11 14:00:32 -0700 |
| commit | 5ef33fad3a4d6438d7e3c38388639eff7f08533d (patch) | |
| tree | 5b44085b51ba2aa44dd965c62818c2ca74b97d96 /Source/Concurrency/LinearSets.cs | |
| parent | 9abbf5e9060e152fb13c0cd5c9fbbdc3aba19f30 (diff) | |
fixed some tests in og
added another test in linear (based on bug reported by Chris)
removed the QED build configuration
Diffstat (limited to 'Source/Concurrency/LinearSets.cs')
| -rw-r--r-- | Source/Concurrency/LinearSets.cs | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs index 08354ae6..fc44468c 100644 --- a/Source/Concurrency/LinearSets.cs +++ b/Source/Concurrency/LinearSets.cs @@ -466,9 +466,14 @@ namespace Microsoft.Boogie Error(node, "Only local linear variable can be an actual input parameter of a procedure call");
continue;
}
- if (FindLinearKind(formal) == LinearKind.LINEAR && FindLinearKind(actual.Decl) == LinearKind.CONST)
+ if (FindLinearKind(actual.Decl) == LinearKind.CONST && FindLinearKind(formal) == LinearKind.LINEAR)
{
- Error(node, "Only non-const linear variable can be an actual parameter to a non-const input parameter of a procedure call");
+ Error(node, "Const linear variable cannot be an argument for a linear input parameter of a procedure call");
+ continue;
+ }
+ if (FindLinearKind(actual.Decl) == LinearKind.CONST && FindLinearKind(formal) == LinearKind.CONST && node.IsAsync)
+ {
+ Error(node, "Const linear variable cannot be an argument for a const parameter of an async procedure call");
continue;
}
if (inVars.Contains(actual.Decl))
|