diff options
| -rw-r--r-- | Source/Core/OwickiGries.cs | 12 | ||||
| -rw-r--r-- | Test/og/Answer | 4 | ||||
| -rw-r--r-- | Test/og/parallel5.bpl | 36 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 2 |
4 files changed, 51 insertions, 3 deletions
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index fd97c20e..f11ff45a 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -319,15 +319,23 @@ namespace Microsoft.Boogie {
Variable inParam = impl.Proc.InParams[i];
var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
+ var ie = new IdentifierExpr(Token.NoToken, copy);
locals.Add(copy);
- map[impl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);
+ // substitute for both implementation and procedure parameters because yield predicates can be generated
+ // either by assertions in the implementation or preconditions and postconditions in the procedure
+ map[impl.InParams[i]] = ie;
+ map[impl.Proc.InParams[i]] = ie;
}
for (int i = 0; i < impl.Proc.OutParams.Length; i++)
{
Variable outParam = impl.Proc.OutParams[i];
var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type), outParam.Attributes);
+ var ie = new IdentifierExpr(Token.NoToken, copy);
locals.Add(copy);
- map[impl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy);
+ // substitute for both implementation and procedure parameters because yield predicates can be generated
+ // either by assertions in the implementation or preconditions and postconditions in the procedure
+ map[impl.OutParams[i]] = ie;
+ map[impl.Proc.OutParams[i]] = ie;
}
foreach (Variable local in impl.LocVars)
{
diff --git a/Test/og/Answer b/Test/og/Answer index 1b341ee4..154b0193 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -68,3 +68,7 @@ Execution trace: parallel4.bpl(12,3): anon0$2
Boogie program verifier finished with 2 verified, 1 error
+
+-------------------- parallel5.bpl --------------------
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl new file mode 100644 index 00000000..8ee5e436 --- /dev/null +++ b/Test/og/parallel5.bpl @@ -0,0 +1,36 @@ +var a:[int]int;
+
+procedure {:entrypoint} main()
+{
+ var {:linear "tid"} i: int;
+ var {:linear "tid"} j: int;
+ call i := t(i) | j := Yield(j);
+ call i := u(i) | j := u(j);
+}
+
+procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+{
+ assume i == i';
+
+ a[i] := 42;
+ call i := Yield(i);
+ assert a[i] == 42;
+}
+
+procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+{
+ assume i == i';
+
+ a[i] := 42;
+ yield;
+ assert a[i] == 42;
+}
+
+procedure Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+ensures i == i';
+ensures old(a)[i] == a[i];
+{
+ assume i == i';
+ yield;
+ assert old(a)[i] == a[i];
+}
\ No newline at end of file diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index a1cbfba0..64c21618 100644 --- a/Test/og/runtest.bat +++ b/Test/og/runtest.bat @@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do ( %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
|