diff options
Diffstat (limited to 'Source/Core/AbsyCmd.cs')
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index e4451807..cd7a8edd 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -957,9 +957,19 @@ namespace Microsoft.Boogie { {
tc.Error(this, "command assigns to an immutable variable: {0}", v.Name);
}
- else if (!CommandLineOptions.Clo.DoModSetAnalysis && v is GlobalVariable && !tc.InFrame(v))
+ else if (!CommandLineOptions.Clo.DoModSetAnalysis && v is GlobalVariable)
{
- tc.Error(this, "command assigns to a global variable that is not in the enclosing procedure's modifies clause: {0}", v.Name);
+ if (tc.Yields) {
+ // a yielding procedure is allowed to modify any global variable
+ }
+ else if (tc.Frame == null)
+ {
+ tc.Error(this, "update to a global variable allowed only inside an atomic action of a yielding procedure");
+ }
+ else if (!tc.InFrame(v))
+ {
+ tc.Error(this, "command assigns to a global variable that is not in the enclosing procedure's modifies clause: {0}", v.Name);
+ }
}
}
}
|