diff options
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 25 | ||||
| -rw-r--r-- | Test/og/ghost.bpl | 27 | ||||
| -rw-r--r-- | Test/og/ghost.bpl.expect | 2 |
3 files changed, 52 insertions, 2 deletions
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 907f7397..c407a7b9 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -474,6 +474,15 @@ namespace Microsoft.Boogie }
if (errorCount > 0) return;
this.VisitProgram(program);
+ foreach (Procedure proc in program.Procedures)
+ {
+ if (procToActionInfo.ContainsKey(proc)) continue;
+ foreach (var ie in proc.Modifies)
+ {
+ if (!SharedVariables.Contains(ie.Decl)) continue;
+ Error(proc, "A ghost procedure must not modify a global variable with layer annotation");
+ }
+ }
if (errorCount > 0) return;
YieldTypeChecker.PerformYieldSafeCheck(this);
new LayerEraser().VisitProgram(program);
@@ -549,12 +558,24 @@ namespace Microsoft.Boogie {
Error(node, "The callee is not available in the caller procedure");
}
+ return base.VisitCallCmd(node);
}
else
{
- Error(node, "Yielding procedure can call only a yielding procedure");
+ foreach (var ie in node.Outs)
+ {
+ if (ghostVars.Contains(ie.Decl)) continue;
+ Error(node, "The output of a ghost procedure must be assigned to a ghost variable");
+ }
+ bool savedCanAccessSharedVars = canAccessSharedVars;
+ bool savedCanAccessAuxVars = canAccessGhostVars;
+ canAccessSharedVars = true;
+ canAccessGhostVars = true;
+ var retVal = base.VisitCallCmd(node);
+ canAccessSharedVars = savedCanAccessSharedVars;
+ canAccessGhostVars = savedCanAccessAuxVars;
+ return retVal;
}
- return base.VisitCallCmd(node);
}
public override Cmd VisitParCallCmd(ParCallCmd node)
diff --git a/Test/og/ghost.bpl b/Test/og/ghost.bpl new file mode 100644 index 00000000..ef40a232 --- /dev/null +++ b/Test/og/ghost.bpl @@ -0,0 +1,27 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0} x: int; + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:right} |{ A: x := x + 1; return true; }|; + +procedure ghost(y: int) returns (z: int) +requires y == 1; +ensures z == 2; +{ + z := y + 1; +} + +procedure {:yields} {:layer 1,2} Incr2() +ensures {:right} |{ A: x := x + 2; return true; }|; +{ + var {:ghost} a: int; + var {:ghost} b: int; + + yield; + call a := ghost(1); + assert {:layer 1} a == 2; + par Incr() | Incr(); + yield; +} + diff --git a/Test/og/ghost.bpl.expect b/Test/og/ghost.bpl.expect new file mode 100644 index 00000000..41374b00 --- /dev/null +++ b/Test/og/ghost.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors |