diff options
| author |  qadeer <unknown> | 2013-08-21 13:22:20 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2013-08-21 13:22:20 -0700 |
| commit | ac0249195d337ae55a87789261380be179364843 (patch) | |
| tree | 2f427543f481e92c96b566c40a76338317b7e415 | |
| parent | f1f3d32ba043c0468dd04dfcfa7ac02c3fa1876c (diff) | |
some minor fixes
| -rw-r--r-- | Source/Core/Absy.cs | 7 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 3 |
2 files changed, 7 insertions, 3 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 009fb071..33c4e91a 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2354,9 +2354,10 @@ namespace Microsoft.Boogie { public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
bool isAtomicSpecification =
- QKeyValue.FindIntAttribute(this.Attributes, "atomic", -1) != -1 ||
- QKeyValue.FindIntAttribute(this.Attributes, "rightmover", -1) != -1 ||
- QKeyValue.FindIntAttribute(this.Attributes, "leftmover", -1) != -1;
+ QKeyValue.FindBoolAttribute(this.Attributes, "atomic") ||
+ QKeyValue.FindBoolAttribute(this.Attributes, "right") ||
+ QKeyValue.FindBoolAttribute(this.Attributes, "left") ||
+ QKeyValue.FindBoolAttribute(this.Attributes, "both");
bool oldYields = tc.Yields;
tc.Yields = isAtomicSpecification;
this.Condition.Typecheck(tc);
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index ed4d8dbb..92529f8f 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -708,8 +708,11 @@ namespace Microsoft.Boogie if (proc == null) continue;
if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
{
+ HashSet<Variable> modifiedVars = new HashSet<Variable>();
+ proc.Modifies.Iter(x => modifiedVars.Add(x.Decl));
foreach (GlobalVariable g in program.GlobalVariables())
{
+ if (modifiedVars.Contains(g)) continue;
proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g));
}
}
|