diff options
author | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-19 11:13:36 +0100 |
---|---|---|
committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-19 11:13:36 +0100 |
commit | 5f26d6075b8493f3e240c5d356b5fc588c5d7985 (patch) | |
tree | 834d1be7b2127bb49b4da949e523ca291a1e6144 /Source/VCGeneration/ConditionGeneration.cs | |
parent | 3c5116cd8a4b58bc220f0d1ff068564556c7ab07 (diff) | |
parent | 51f2fa80a101ffae855c848ed83b889f1becbdd3 (diff) |
merge
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index ad2b7e68..0d6e2aab 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -203,15 +203,18 @@ namespace Microsoft.Boogie { var filename = CommandLineOptions.Clo.ModelViewFile;
if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return;
- var m = ModelHasStatesAlready ? Model : this.GetModelWithStates();
+ if (!ModelHasStatesAlready) {
+ PopulateModelWithStates();
+ ModelHasStatesAlready = true;
+ }
if (filename == "-") {
- m.Write(tw);
+ Model.Write(tw);
tw.Flush();
} else {
using (var wr = new StreamWriter(filename, !firstModelFile)) {
firstModelFile = false;
- m.Write(wr);
+ Model.Write(wr);
}
}
}
@@ -227,16 +230,16 @@ namespace Microsoft.Boogie { m.Substitute(mapping);
}
- public Model GetModelWithStates()
+ public void PopulateModelWithStates()
{
- if (Model == null) return null;
+ Contract.Requires(Model != null);
Model m = Model;
ApplyRedirections(m);
var mvstates = m.TryGetFunc("$mv_state");
if (MvInfo == null || mvstates == null)
- return m;
+ return;
Contract.Assert(mvstates.Arity == 2);
@@ -282,8 +285,6 @@ namespace Microsoft.Boogie { Contract.Assume(false);
}
}
-
- return m;
}
private Model.Element GetModelValue(Model m, Variable v) {
|