diff options
| -rw-r--r-- | Source/Core/OwickiGries.cs | 11 | ||||
| -rw-r--r-- | Test/og/Answer | 40 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 2 |
3 files changed, 47 insertions, 6 deletions
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index dd76c376..83509361 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -268,7 +268,7 @@ namespace Microsoft.Boogie // Collect the yield predicates and desugar yields
HashSet<CmdSeq> yields = new HashSet<CmdSeq>();
CmdSeq cmds = new CmdSeq();
- if (procNameToInfo[impl.Name].isThreadStart && impl.Proc.Requires.Length > 0)
+ if (info.isThreadStart && impl.Proc.Requires.Length > 0)
{
foreach (Requires r in impl.Proc.Requires)
{
@@ -332,13 +332,14 @@ namespace Microsoft.Boogie yields.Add(cmds);
cmds = new CmdSeq();
}
- if (b.TransferCmd is ReturnCmd)
+ if (b.TransferCmd is ReturnCmd && (!info.isAtomic || info.isEntrypoint || info.isThreadStart))
{
AddCallsToYieldCheckers(newCmds);
}
b.Cmds = newCmds;
}
+ if (!info.isAtomic)
{
// Loops
impl.PruneUnreachableBlocks();
@@ -405,10 +406,10 @@ namespace Microsoft.Boogie yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), new GotoCmd(Token.NoToken, labels, labelTargets)));
// Create the yield checker implementation
- var yieldCheckerImpl = new Implementation(Token.NoToken, procNameToInfo[impl.Name].yieldCheckerProc.Name, impl.TypeParameters, new VariableSeq(), new VariableSeq(), locals, yieldCheckerBlocks);
- yieldCheckerImpl.Proc = procNameToInfo[impl.Name].yieldCheckerProc;
+ var yieldCheckerImpl = new Implementation(Token.NoToken, info.yieldCheckerProc.Name, impl.TypeParameters, new VariableSeq(), new VariableSeq(), locals, yieldCheckerBlocks);
+ yieldCheckerImpl.Proc = info.yieldCheckerProc;
yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- procNameToInfo[impl.Name].yieldCheckerImpl = yieldCheckerImpl;
+ info.yieldCheckerImpl = yieldCheckerImpl;
}
foreach (Variable v in ogOldGlobalMap.Keys)
diff --git a/Test/og/Answer b/Test/og/Answer new file mode 100644 index 00000000..712ebfd8 --- /dev/null +++ b/Test/og/Answer @@ -0,0 +1,40 @@ +
+-------------------- foo.bpl --------------------
+OwickiGriesDesugared.bpl(179,4): Error BP5001: This assertion might not hold.
+Execution trace:
+ OwickiGriesDesugared.bpl(17,0): anon0
+ OwickiGriesDesugared.bpl(177,0): inline$YieldChecker_PC$0$L1
+
+Boogie program verifier finished with 3 verified, 1 error
+
+-------------------- bar.bpl --------------------
+OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.
+Execution trace:
+ OwickiGriesDesugared.bpl(17,0): anon0
+ OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1
+OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.
+Execution trace:
+ OwickiGriesDesugared.bpl(68,0): anon0
+ OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1
+
+Boogie program verifier finished with 2 verified, 2 errors
+
+-------------------- one.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- linear-set.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- linear-set2.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- FlanaganQadeer.bpl --------------------
+
+Boogie program verifier finished with 3 verified, 0 errors
+
+-------------------- DeviceCacheSimplified.bpl --------------------
+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index 839ac09b..197f33f7 100644 --- a/Test/og/runtest.bat +++ b/Test/og/runtest.bat @@ -3,7 +3,7 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (foo.bpl bar.bpl) do (
+for %%f in (foo.bpl bar.bpl one.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
|