diff options
| author |  Unknown <akashl@akash-desk.fareast.corp.microsoft.com> | 2012-04-24 15:41:40 +0530 |
|---|---|---|
| committer | Unknown <akashl@akash-desk.fareast.corp.microsoft.com> | 2012-04-24 15:41:40 +0530 |
| commit | 9b20e96cc4ca31eff8128965def3284c650c572f (patch) | |
| tree | 66a0e3838e0fb3ae5408886873f200f399fbffed | |
| parent | 4c54cedf8a081499583be60f164dbbb29c6c73ac (diff) | |
Added test to stratified inlining.
Don't use UNSAT core for the refinement step.
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 3 | ||||
| -rw-r--r-- | Test/stratifiedinline/Answer | 21 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar11.bpl | 32 | ||||
| -rw-r--r-- | Test/stratifiedinline/runtest.bat | 3 |
4 files changed, 57 insertions, 2 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index ea17983f..420c24ab 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1371,7 +1371,6 @@ namespace VC private bool refinementLoopCheckPath(ApiChecker apiChecker, HashSet<VCExprVar> varsToSet, HashSet<VCExprVar> allVars)
{
var assumptions = new List<VCExpr>();
- List<int> temp = null;
var query = new HashSet<string>();
varsToSet.Iter(v => query.Add(v.Name));
@@ -1405,7 +1404,7 @@ namespace VC }
//Console.WriteLine();
- var o = apiChecker.CheckAssumptions(assumptions, out temp);
+ var o = apiChecker.CheckAssumptions(assumptions);
Debug.Assert(o == Outcome.Correct || o == Outcome.Errors);
//Console.WriteLine("Result = " + o.ToString());
apiChecker.LogComment("FindLeast: Query End");
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index 6e23c098..77b00b19 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -484,3 +484,24 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
+----- Running regression test bar11.bpl
+bar11.bpl(31,1): Error BP5003: A postcondition might not hold on this return path.
+bar11.bpl(26,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ bar11.bpl(30,3): anon0
+ Inlined call to procedure foo begins
+ bar11.bpl(15,3): anon0
+ value = 0
+ Inlined call to procedure bar begins
+ bar11.bpl(8,5): anon0
+ value = 1
+ Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar11.bpl(8,5): anon0
+ value = 2
+ Inlined call to procedure bar ends
+ value = 2
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
diff --git a/Test/stratifiedinline/bar11.bpl b/Test/stratifiedinline/bar11.bpl new file mode 100644 index 00000000..baad27a1 --- /dev/null +++ b/Test/stratifiedinline/bar11.bpl @@ -0,0 +1,32 @@ +var x: int;
+var y: int;
+procedure boogie_si_record_int(x:int);
+
+procedure {:inline 1} bar()
+modifies y;
+{
+ y := y + 1;
+ call boogie_si_record_int(y);
+}
+
+procedure {:inline 1} foo()
+modifies x, y;
+{
+ call boogie_si_record_int(x);
+ x := x + 1;
+ call bar();
+ call bar();
+ x := x + 1;
+ call boogie_si_record_int(x);
+}
+
+procedure main()
+requires x == 0;
+requires x == y;
+ensures x != y;
+modifies x, y;
+{
+
+ call foo();
+}
+
diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat index d731d605..3ba74096 100644 --- a/Test/stratifiedinline/runtest.bat +++ b/Test/stratifiedinline/runtest.bat @@ -31,4 +31,7 @@ echo ----- echo ----- Running regression test bar10.bpl
%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar10.bpl
echo -----
+echo ----- Running regression test bar11.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 bar11.bpl
+echo -----
|