summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Unknown <afd@afd-THINK.doc.ic.ac.uk>2012-04-05 09:23:19 +0100
committerGravatar Unknown <afd@afd-THINK.doc.ic.ac.uk>2012-04-05 09:23:19 +0100
commit562ea75667e8eabf6703eb62b8716a920b2c02c6 (patch)
tree88ec4979ab1a22bee350381e363d163389012cb5
parentb5af82dc559738906d5342ee5614d632c03a2c68 (diff)
parent659491fddae2ee457100b6fa4c27afef3340621e (diff)
Merge
Diffstat
-rw-r--r--Source/Core/AbsyCmd.cs2
-rw-r--r--Source/Core/CommandLineOptions.cs9
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs75
-rw-r--r--Source/VCGeneration/Check.cs4
-rw-r--r--Source/VCGeneration/StratifiedVC.cs142
-rw-r--r--Test/aitest9/TestIntervals.bpl16
-rw-r--r--Test/aitest9/answer2
-rw-r--r--Test/stratifiedinline/Answer422
-rw-r--r--Test/stratifiedinline/bar10.bpl41
-rw-r--r--Test/stratifiedinline/bar7.bpl2
-rw-r--r--Test/stratifiedinline/bar8.bpl2
-rw-r--r--Test/stratifiedinline/bar9.bpl45
-rw-r--r--Test/stratifiedinline/runtest.bat12
13 files changed, 677 insertions, 97 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 62ebc77f..1367a08d 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1472,7 +1472,7 @@ namespace Microsoft.Boogie {
NAryExpr/*!*/ res = Expr.Select(Map.AsExpr, Indexes);
Contract.Assert(res != null);
res.TypeParameters = this.TypeParameters;
- res.Type = Map.AsExpr.Type.AsMap.Result;
+ res.Type = this.Type;
return res;
}
}
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 1a2d7fda..ed80f6ac 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -564,8 +564,8 @@ namespace Microsoft.Boogie {
public int StratifiedInliningOption = 0;
public bool StratifiedInliningWithoutModels = false; // disable model generation for SI
public int StratifiedInliningVerbose = 0; // verbosity level
- public bool UseUnsatCoreForInlining = false;
public int RecursionBound = 500;
+ public bool NonUniformUnfolding = false;
public string inferLeastForUnsat = null;
public string CoverageReporterPath = null;
public Process coverageReporter = null; // used internally for debugging
@@ -1027,10 +1027,6 @@ namespace Microsoft.Boogie {
}
return true;
- case "useUnsatCoreForInlining":
- UseUnsatCoreForInlining = true;
- return true;
-
case "inferLeastForUnsat":
if (ps.ConfirmArgumentCount(1)) {
inferLeastForUnsat = args[ps.i];
@@ -1228,7 +1224,8 @@ namespace Microsoft.Boogie {
ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||
ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||
ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||
- ps.CheckBooleanFlag("printAssignment", ref PrintAssignment)
+ ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
+ ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding)
) {
// one of the boolean flags matched
return true;
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 509f81ce..08322ebb 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -85,7 +85,7 @@ namespace Microsoft.Boogie.SMTLib
{
currentLogFile = OpenOutputFile("");
}
- if (CommandLineOptions.Clo.ProcedureCopyBound > 0 || CommandLineOptions.Clo.UseUnsatCoreForInlining)
+ if (CommandLineOptions.Clo.ProcedureCopyBound > 0)
{
SendThisVC("(set-option :produce-unsat-cores true)");
this.usingUnsatCore = true;
@@ -835,6 +835,79 @@ namespace Microsoft.Boogie.SMTLib
DeclCollector.Push();
}
+ public override Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions, out List<int> unsatisfiedSoftAssumptions, ErrorHandler handler) {
+ unsatisfiedSoftAssumptions = new List<int>();
+
+ // First, convert both hard and soft assumptions to SMTLIB strings
+ List<string> hardAssumptionStrings = new List<string>();
+ foreach (var a in hardAssumptions) {
+ hardAssumptionStrings.Add(VCExpr2String(a, 1));
+ }
+ List<string> currAssumptionStrings = new List<string>();
+ foreach (var a in softAssumptions) {
+ currAssumptionStrings.Add(VCExpr2String(a, 1));
+ }
+
+ Push();
+ AssertAxioms();
+ foreach (var a in hardAssumptionStrings) {
+ SendThisVC("(assert " + a + ")");
+ }
+ Check();
+ Outcome outcome = GetResponse();
+ if (outcome != Outcome.Invalid) {
+ Pop();
+ return outcome;
+ }
+
+ int k = 0;
+ List<string> relaxVars = new List<string>();
+ while (true) {
+ Push();
+ foreach (var a in currAssumptionStrings) {
+ SendThisVC("(assert " + a + ")");
+ }
+ Check();
+ outcome = CheckOutcomeCore(handler);
+ if (outcome != Outcome.Valid)
+ break;
+ Pop();
+ string relaxVar = "relax_" + k;
+ relaxVars.Add(relaxVar);
+ SendThisVC("(declare-fun " + relaxVar + " () Int)");
+ List<string> nextAssumptionStrings = new List<string>();
+ for (int i = 0; i < currAssumptionStrings.Count; i++) {
+ string constraint = "(= " + relaxVar + " " + i + ")";
+ nextAssumptionStrings.Add("(or " + currAssumptionStrings[i] + " " + constraint + ")");
+ }
+ currAssumptionStrings = nextAssumptionStrings;
+ k++;
+ }
+
+ if (outcome == Outcome.Invalid) {
+ foreach (var relaxVar in relaxVars) {
+ SendThisVC("(get-value (" + relaxVar + "))");
+ FlushLogFile();
+ var resp = Process.GetProverResponse();
+ if (resp == null) break;
+ if (!(resp.Name == "" && resp.ArgCount == 1)) break;
+ resp = resp.Arguments[0];
+ if (!(resp.Name == "" && resp.ArgCount == 2)) break;
+ resp = resp.Arguments[1];
+ if (resp.ArgCount != 0)
+ break;
+ int v;
+ if (int.TryParse(resp.Name, out v))
+ unsatisfiedSoftAssumptions.Add(v);
+ else
+ break;
+ }
+ Pop();
+ }
+
+ Pop();
+ return outcome;
+ }
}
public class SMTLibProverContext : DeclFreeProverContext
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index a1b9e38d..f9999a74 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -829,6 +829,10 @@ namespace Microsoft.Boogie {
throw new NotImplementedException();
}
+ public virtual Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions, out List<int> unsatisfiedSoftAssumptions, ErrorHandler handler) {
+ throw new NotImplementedException();
+ }
+
public virtual Outcome CheckOutcomeCore(ErrorHandler handler)
{
throw new NotImplementedException();
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 9e55b3d6..98f20d21 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1039,8 +1039,6 @@ namespace VC
private List<int> numAxiomsPushed;
// Api-based theorem prover
private ProverInterface TheoremProver;
- // Use checkAssumptions?
- public static bool UseCheckAssumptions = true;
private FCallHandler calls;
// Underlying checker
public Checker underlyingChecker;
@@ -1108,33 +1106,44 @@ namespace VC
checker.TheoremProver.LogComment(str);
}
- public Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore) {
- if (!UseCheckAssumptions) {
- Outcome ret;
-
- unsatCore = new List<int>();
- for (int i = 0; i < assumptions.Count; i++)
- unsatCore.Add(i);
+ public Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions) {
+ List<int> unsatisfiedSoftAssumptions;
+ ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, reporter);
+ switch (outcome) {
+ case ProverInterface.Outcome.Valid:
+ return Outcome.Correct;
+ case ProverInterface.Outcome.Invalid:
+ return Outcome.Errors;
+ case ProverInterface.Outcome.OutOfMemory:
+ return Outcome.OutOfMemory;
+ case ProverInterface.Outcome.TimeOut:
+ return Outcome.TimedOut;
+ case ProverInterface.Outcome.Undetermined:
+ return Outcome.Inconclusive;
+ default:
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ }
- if (assumptions.Count == 0)
- {
- return CheckVC();
- }
+ public Outcome CheckAssumptions(List<VCExpr> assumptions) {
+ if (assumptions.Count == 0) {
+ return CheckVC();
+ }
- Push();
+ Push();
- foreach (var a in assumptions)
- {
- AddAxiom(a);
- }
- ret = CheckVC();
+ foreach (var a in assumptions) {
+ AddAxiom(a);
+ }
+ Outcome ret = CheckVC();
- Pop();
+ Pop();
- return ret;
+ return ret;
+ }
- }
-
+ public Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore) {
if (assumptions.Count == 0) {
unsatCore = new List<int>();
return CheckVC();
@@ -1605,13 +1614,13 @@ namespace VC
// bool underApproxNeeded = true;
// The recursion bound for stratified search
- int bound = 1;
+ int bound = CommandLineOptions.Clo.NonUniformUnfolding ? CommandLineOptions.Clo.RecursionBound : 1;
int done = 0;
int iters = 0;
- // for blocking candidates (and focussing on a counterexample)
+ // for blocking candidates (and focusing on a counterexample)
var block = new HashSet<int>();
// Process tasks while not done. We're done when:
@@ -1712,14 +1721,7 @@ namespace VC
if (block.Count == 0)
{
// Increment bound
- var minRecReached = CommandLineOptions.Clo.RecursionBound + 1;
- foreach (var id in calls.currCandidates)
- {
- var rb = calls.getRecursionBound(id);
- if (rb <= bound) continue;
- if (rb < minRecReached) minRecReached = rb;
- }
- bound = minRecReached;
+ bound++;
if (useSummary) summaryComputation.boundChanged();
if (bound > CommandLineOptions.Clo.RecursionBound)
@@ -1911,6 +1913,7 @@ namespace VC
calleeToCallSites[callee].Remove(cs);
}
+#if SuperAwesomeMethod
private Outcome FindUnsatCoreInMainCallees(Implementation impl, ApiChecker checker, VCExpressionGenerator Gen, PCBErrorReporter reporter, List<VCExpr> assumptions, out HashSet<VCExprVar> unsatCore)
{
Debug.Assert(checker is ApiChecker);
@@ -1932,7 +1935,7 @@ namespace VC
}
return Outcome.Correct;
}
-
+
private Outcome FindUnsatCore(Implementation impl, ApiChecker checker, VCExpressionGenerator Gen, PCBErrorReporter reporter, List<VCExpr> assumptions, out HashSet<VCExprVar> unsatCore)
{
Helpers.ExtraTraceInformation("Number of assumptions = " + assumptions.Count);
@@ -2156,74 +2159,38 @@ namespace VC
InlineIntoMain(checker, impl, unsatCore);
}
}
-
-
+#endif
// A step of the stratified inlining algorithm: both under-approx and over-approx queries
private Outcome stratifiedStep(int bound, VerificationState vState, HashSet<int> block)
{
- Outcome ret;
- List<int> unsatCore;
-
- // No need of computing Unsat cores for stratified inlining
- if (!CommandLineOptions.Clo.UseUnsatCoreForInlining && CommandLineOptions.Clo.ProverName == "SMTLIB")
- ApiChecker.UseCheckAssumptions = false;
-
var reporter = vState.reporter as StratifiedInliningErrorReporter;
var calls = vState.calls;
var checker = vState.checker;
reporter.underapproximationMode = true;
checker.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");
- List<VCExpr> assumptions;
- List<int> ids;
-
- while (true)
+ List<VCExpr> assumptions = new List<VCExpr>();
+ List<int> ids = new List<int>();
+ foreach (int id in calls.currCandidates)
{
- assumptions = new List<VCExpr>();
- ids = new List<int>();
- foreach (int id in calls.currCandidates)
- {
- assumptions.Add(calls.getFalseExpr(id));
- ids.Add(id);
- }
- ret = checker.CheckAssumptions(assumptions, out unsatCore);
- if (!CommandLineOptions.Clo.UseUnsatCoreForInlining) break;
- if (ret != Outcome.Correct) break;
- Debug.Assert(unsatCore.Count <= assumptions.Count);
- if (unsatCore.Count == assumptions.Count)
- break;
-
- var unsatCoreIds = new List<int>();
- foreach (int i in unsatCore)
- unsatCoreIds.Add(ids[i]);
- vState.checker.LogComment(";;;;;;;;;;;; Expansion begin ;;;;;;;;;;");
- bool incrementalSearch =
- CommandLineOptions.Clo.StratifiedInliningOption == 0 ||
- CommandLineOptions.Clo.StratifiedInliningOption == 2;
- DoExpansion(incrementalSearch, unsatCoreIds, vState);
- vState.calls.forcedCandidates.UnionWith(unsatCoreIds);
- vState.checker.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;");
+ assumptions.Add(calls.getFalseExpr(id));
+ ids.Add(id);
}
-
+ Outcome ret = checker.CheckAssumptions(assumptions);
checker.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");
- if (ret == Outcome.Errors)
- {
- return ret;
- }
-
if (ret != Outcome.Correct)
{
- // The query ran out of memory or time, that's it,
- // we cannot do better. Give up!
+ // Either the query returned an error or it ran out of memory or time.
+ // In all cases, we are done.
return ret;
}
- // If we didn't underapproximate, then we're done
if (calls.currCandidates.Count == 0)
{
- return ret;
+ // If we didn't underapproximate, then we're done
+ return ret;
}
checker.LogComment(";;;;;;;;;;;; Overapprox mode begin ;;;;;;;;;;");
@@ -2237,31 +2204,32 @@ namespace VC
bool allTrue = true;
bool allFalse = true;
+ List<VCExpr> softAssumptions = new List<VCExpr>();
assumptions = new List<VCExpr>();
procsThatReachedRecBound.Clear();
foreach (int id in calls.currCandidates)
{
- if (calls.getRecursionBound(id) <= bound)
+ int idBound = calls.getRecursionBound(id);
+ if (idBound <= bound)
{
+ if (idBound > 1)
+ softAssumptions.Add(calls.getFalseExpr(id));
if (block.Contains(id))
{
Contract.Assert(useSummary);
- //checker.AddAxiom(calls.getFalseExpr(id));
assumptions.Add(calls.getFalseExpr(id));
allTrue = false;
}
else
{
- //checker.TheoremProver.PushVCExpression(calls.getTrueExpr(id));
allFalse = false;
}
}
else
{
procsThatReachedRecBound.Add(calls.getProc(id));
- //checker.AddAxiom(calls.getFalseExpr(id));
assumptions.Add(calls.getFalseExpr(id));
allTrue = false;
}
@@ -2275,7 +2243,9 @@ namespace VC
}
else
{
- ret = checker.CheckAssumptions(assumptions, out unsatCore);
+ ret = CommandLineOptions.Clo.NonUniformUnfolding
+ ? checker.CheckAssumptions(assumptions, softAssumptions)
+ : checker.CheckAssumptions(assumptions);
}
if (ret != Outcome.Correct && ret != Outcome.Errors)
diff --git a/Test/aitest9/TestIntervals.bpl b/Test/aitest9/TestIntervals.bpl
index b989e16c..bee73a57 100644
--- a/Test/aitest9/TestIntervals.bpl
+++ b/Test/aitest9/TestIntervals.bpl
@@ -22,3 +22,19 @@ procedure P()
assert -3 <= c;
assert c <= 0; // error (there was once an error in the Intervals which thought this assertion to be true)
}
+
+// The following tests a triply nested array, where the innermost array is a polymorphic map.
+// There was once an error in Boogie's handling of such things in the AI code.
+
+type ref;
+type teflon;
+
+type Field a;
+type HeapType = <a>[Field a]a;
+var Heap: HeapType;
+
+procedure Q(myField: Field [ref][teflon]bool, r: ref, t: teflon)
+ modifies Heap;
+{
+ Heap[myField][r][t] := true;
+}
diff --git a/Test/aitest9/answer b/Test/aitest9/answer
index 27e18ca4..d68508af 100644
--- a/Test/aitest9/answer
+++ b/Test/aitest9/answer
@@ -18,4 +18,4 @@ Execution trace:
TestIntervals.bpl(14,14): anon12_Then
TestIntervals.bpl(17,5): anon8
-Boogie program verifier finished with 0 verified, 1 error
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
index aee2722e..6e23c098 100644
--- a/Test/stratifiedinline/Answer
+++ b/Test/stratifiedinline/Answer
@@ -62,3 +62,425 @@ Boogie program verifier finished with 1 verified, 0 errors
Boogie program verifier finished with 1 verified, 0 errors
-----
+----- Running regression test bar7.bpl
+bar7.bpl(42,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar7.bpl(35,5): anon0
+ bar7.bpl(37,5): anon4_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(7,3): anon2_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ bar7.bpl(42,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar8.bpl
+bar8.bpl(41,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar8.bpl(34,5): anon0
+ bar8.bpl(36,5): anon4_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(7,3): anon2_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ bar8.bpl(41,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar9.bpl
+bar9.bpl(44,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar9.bpl(35,5): anon0
+ bar9.bpl(41,5): anon4_Else
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(16,3): anon2_Else
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(26,3): anon2_Else
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ bar9.bpl(44,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar10.bpl
+bar10.bpl(40,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar10.bpl(35,5): anon0
+ Inlined call to procedure bar1 begins
+ bar10.bpl(16,3): anon0
+ bar10.bpl(16,3): anon2_Else
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar2 begins
+ bar10.bpl(26,3): anon0
+ bar10.bpl(26,3): anon2_Else
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(7,3): anon2_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
diff --git a/Test/stratifiedinline/bar10.bpl b/Test/stratifiedinline/bar10.bpl
new file mode 100644
index 00000000..8cfcfc13
--- /dev/null
+++ b/Test/stratifiedinline/bar10.bpl
@@ -0,0 +1,41 @@
+var i: int;
+var m: int;
+
+procedure {:inline 1} foo()
+modifies i;
+{
+ if (i < 20) {
+ i := i + 1;
+ call foo();
+ }
+}
+
+procedure {:inline 1} bar1(j: int)
+modifies i;
+{
+ if (j < 2*m)
+ {
+ i := i + 1;
+ call bar1(j+1);
+ }
+}
+
+procedure {:inline 1} bar2(j: int)
+modifies i;
+{
+ if (j < m) {
+ i := i - 1;
+ call bar2(j+1);
+ }
+}
+
+procedure main()
+modifies i;
+{
+ i := 0;
+ call bar1(0);
+ call bar2(0);
+ i := 0;
+ call foo();
+ assert i < 10;
+} \ No newline at end of file
diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl
index 747510de..b28777bd 100644
--- a/Test/stratifiedinline/bar7.bpl
+++ b/Test/stratifiedinline/bar7.bpl
@@ -4,7 +4,7 @@ var m: int;
procedure {:inline 1} foo()
modifies i;
{
- if (i < 80) {
+ if (i < 20) {
i := i + 1;
call foo();
}
diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl
index d447e3a7..e96655f3 100644
--- a/Test/stratifiedinline/bar8.bpl
+++ b/Test/stratifiedinline/bar8.bpl
@@ -4,7 +4,7 @@ var m: int;
procedure {:inline 1} foo()
modifies i;
{
- if (i < 80) {
+ if (i < 20) {
i := i + 1;
call foo();
}
diff --git a/Test/stratifiedinline/bar9.bpl b/Test/stratifiedinline/bar9.bpl
new file mode 100644
index 00000000..12de78ad
--- /dev/null
+++ b/Test/stratifiedinline/bar9.bpl
@@ -0,0 +1,45 @@
+var i: int;
+var m: int;
+
+procedure {:inline 1} foo(x: int)
+modifies i;
+{
+ if (i < x) {
+ i := i + 1;
+ call foo(x);
+ }
+}
+
+procedure {:inline 1} bar1(j: int)
+modifies i;
+{
+ if (j < 2*m)
+ {
+ i := i + 1;
+ call bar1(j+1);
+ }
+}
+
+procedure {:inline 1} bar2(j: int)
+modifies i;
+{
+ if (j < m) {
+ i := i - 1;
+ call bar2(j+1);
+ }
+}
+
+procedure main()
+modifies i;
+{
+ i := 0;
+ if (*) {
+ call foo(20);
+ i := 0;
+ call foo(4);
+ } else {
+ call bar1(0);
+ call bar2(0);
+ }
+ assert i < 10;
+} \ No newline at end of file
diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat
index 194570d0..d731d605 100644
--- a/Test/stratifiedinline/runtest.bat
+++ b/Test/stratifiedinline/runtest.bat
@@ -19,4 +19,16 @@ echo -----
echo ----- Running regression test bar6.bpl
%BGEXE% %* /noinfer /stratifiedInline:1 bar6.bpl
echo -----
+echo ----- Running regression test bar7.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar7.bpl
+echo -----
+echo ----- Running regression test bar8.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar8.bpl
+echo -----
+echo ----- Running regression test bar9.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar9.bpl
+echo -----
+echo ----- Running regression test bar10.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar10.bpl
+echo -----
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 22:00:17 +0000