diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 14 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 23 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 5 | ||||
| -rw-r--r-- | Source/VCGeneration/VCDoomed.cs | 9 |
5 files changed, 29 insertions, 24 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 0911cbd3..44adce15 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -701,7 +701,7 @@ namespace Microsoft.Boogie { Console.WriteLine();
}
else {
- outcome = vcgen.VerifyImplementation(impl, program, out errors);
+ outcome = vcgen.VerifyImplementation(impl, out errors);
if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null) {
for (int i = 0; i < errors.Count; i++) {
errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index dd898c36..ba58a5de 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -447,9 +447,8 @@ namespace VC { }
[ContractClassFor(typeof(ConditionGeneration))]
public abstract class ConditionGenerationContracts : ConditionGeneration {
- public override Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback) {
+ public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) {
Contract.Requires(impl != null);
- Contract.Requires(program != null);
Contract.Requires(callback != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
throw new NotImplementedException();
@@ -522,9 +521,8 @@ namespace VC { /// each counterexample consisting of an array of labels.
/// </summary>
/// <param name="impl"></param>
- public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample>/*?*/ errors) {
+ public Outcome VerifyImplementation(Implementation impl, out List<Counterexample>/*?*/ errors) {
Contract.Requires(impl != null);
- Contract.Requires(program != null);
Contract.Ensures(Contract.ValueAtReturn(out errors) == null || Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));
Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);
@@ -532,7 +530,7 @@ namespace VC { Helpers.ExtraTraceInformation("Starting implementation verification");
CounterexampleCollector collector = new CounterexampleCollector();
- Outcome outcome = VerifyImplementation(impl, program, collector);
+ Outcome outcome = VerifyImplementation(impl, collector);
if (outcome == Outcome.Errors) {
errors = collector.examples;
} else {
@@ -550,7 +548,7 @@ namespace VC { /// each counterexample consisting of an array of labels.
/// </summary>
/// <param name="impl"></param>
- public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample> errors, out List<Model> errorsModel)
+ public Outcome VerifyImplementation(Implementation impl, out List<Counterexample> errors, out List<Model> errorsModel)
{
Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || Contract.ValueAtReturn(out errors) != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
@@ -558,14 +556,14 @@ namespace VC { Outcome outcome;
errorModelList = new List<Model>();
- outcome = VerifyImplementation(impl, program, out errorsOut);
+ outcome = VerifyImplementation(impl, out errorsOut);
errors = errorsOut;
errorsModel = errorModelList;
return outcome;
}
- public abstract Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback);
+ public abstract Outcome VerifyImplementation(Implementation impl, VerifierCallback callback);
/////////////////////////////////// Common Methods and Classes //////////////////////////////////////////
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 65aa8486..058b5de9 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -367,10 +367,26 @@ namespace VC { private bool useSummary;
private SummaryComputation summaryComputation;
private HashSet<string> procsThatReachedRecBound;
- public int boundUsedInLastQuery { get; private set; }
public HashSet<string> procsToSkip;
public Dictionary<string, int> extraRecBound;
+ public StratifiedVCGen(bool usePrevCallTree, Dictionary<string, int> prevCallTree,
+ HashSet<string> procsToSkip, Dictionary<string, int> extraRecBound,
+ Program program, string/*?*/ logFilePath, bool appendLogFile)
+ : this(program, logFilePath, appendLogFile)
+ {
+ this.procsToSkip = new HashSet<string>(procsToSkip);
+ this.extraRecBound = new Dictionary<string, int>(extraRecBound);
+
+ if (usePrevCallTree) {
+ callTree = prevCallTree;
+ PersistCallTree = true;
+ }
+ else {
+ PersistCallTree = false;
+ }
+ }
+
public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
: base(program, logFilePath, appendLogFile) {
this.GenerateRecordFunctions();
@@ -379,7 +395,6 @@ namespace VC { procsThatReachedRecBound = new HashSet<string>();
procsToSkip = new HashSet<string>();
extraRecBound = new Dictionary<string, int>();
- boundUsedInLastQuery = -1;
}
// Is this procedure to be "skipped"
@@ -1189,7 +1204,7 @@ namespace VC { }
}
- public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) {
+ public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) {
Debug.Assert(QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"));
Debug.Assert(this.program == program);
@@ -1318,8 +1333,6 @@ namespace VC { // case 2: (bug) We find a bug
// case 3: (internal error) The theorem prover TimesOut of runs OutOfMemory
while (true) {
- boundUsedInLastQuery = bound;
-
// Check timeout
if (CommandLineOptions.Clo.ProverKillTime != -1) {
if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime) {
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 7e3e3f17..373b685a 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1384,10 +1384,7 @@ namespace VC { }
}
- public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) {
- //Contract.Requires(impl != null);
- //Contract.Requires(program != null);
- //Contract.Requires(callback != null);
+ public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) {
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
if (impl.SkipVerification) {
diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs index 4d2e0775..15c6e2aa 100644 --- a/Source/VCGeneration/VCDoomed.cs +++ b/Source/VCGeneration/VCDoomed.cs @@ -101,10 +101,7 @@ namespace VC { /// - check if |= (reach=false) => wlp.S.false holds for each reach
///
/// </summary>
- public override Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback) {
- //Contract.Requires(impl != null);
- //Contract.Requires(program != null);
- //Contract.Requires(callback != null);
+ public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) {
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
Console.WriteLine();
@@ -115,7 +112,7 @@ namespace VC { //Impl2Dot(impl, String.Format("c:/dot/{0}_orig.dot", impl.Name));
- Transform4DoomedCheck(impl, program);
+ Transform4DoomedCheck(impl);
//Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));
@@ -694,7 +691,7 @@ namespace VC { // this might be redundant, but I didn't find a better place to get this information.
private Dictionary<Variable, Expr> m_LastReachVarIncarnation = new Dictionary<Variable, Expr>();
- private void Transform4DoomedCheck(Implementation impl, Program program)
+ private void Transform4DoomedCheck(Implementation impl)
{
variable2SequenceNumber = new Hashtable/*Variable -> int*/();
incarnationOriginMap = new Dictionary<Incarnation, Absy>();
|