summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore6
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs2
-rw-r--r--Source/Core/CommandLineOptions.cs7
-rw-r--r--Source/Provers/Z3/Prover.cs2
-rw-r--r--Source/VCGeneration/Check.cs7
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs31
-rw-r--r--Source/VCGeneration/Model.cs10
-rw-r--r--Source/VCGeneration/VC.cs1
8 files changed, 46 insertions, 20 deletions
diff --git a/.gitignore b/.gitignore
index c6ee95ca..3ac7f5b0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,8 +1,4 @@
-Source/AIFramework/bin/
-Source/AIFramework/obj/
-Source/AbsInt/bin/
-Source/AbsInt/obj/
-Source/Basetypes/bin/
+Source/t
Source/_ReSharper.Boogie
Source/Provers/*/*.user
Source/*/*.user
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 33b9146c..0fc67e15 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -642,7 +642,7 @@ namespace Microsoft.Boogie {
Console.WriteLine("Execution trace:");
error.Print(4);
}
- if (CommandLineOptions.Clo.ModelView == 1) {
+ if (CommandLineOptions.Clo.ModelViewFile != null) {
error.PrintModel();
}
errorCount++;
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4196670f..b63b82cc 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -192,7 +192,6 @@ namespace Microsoft.Boogie {
Contract.Invariant(-1 <= LoopFrameConditions && LoopFrameConditions < 3);
Contract.Invariant(0 <= ModifiesDefault && ModifiesDefault < 7);
Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4);
- Contract.Invariant(0 <= ModelView && ModelView < 2);
Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);
Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);
Contract.Invariant(-1 <= BracketIdsInVC && BracketIdsInVC <= 1);
@@ -230,7 +229,7 @@ namespace Microsoft.Boogie {
public int PrintErrorModel = 0;
public string PrintErrorModelFile = null;
public bool CEVPrint = false;
- public int ModelView = 1;
+ public string/*?*/ ModelViewFile = null;
public int EnhancedErrorMessages = 0;
public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present
public enum BvHandling {
@@ -922,7 +921,9 @@ namespace Microsoft.Boogie {
case "-mv":
case "/mv":
- ps.GetNumericArgument(ref ModelView, 2);
+ if (ps.ConfirmArgumentCount(1)) {
+ ModelViewFile = args[ps.i];
+ }
break;
case "-printModelToFile":
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 33e622ba..f218d3b6 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -70,7 +70,7 @@ namespace Microsoft.Boogie.Z3
{
return CommandLineOptions.Clo.PrintErrorModel >= 1 ||
CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
- CommandLineOptions.Clo.ModelView > 0 ||
+ CommandLineOptions.Clo.ModelViewFile != null ||
CommandLineOptions.Clo.ContractInfer ||
CommandLineOptions.Clo.LazyInlining > 0 ||
CommandLineOptions.Clo.StratifiedInlining > 0;
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index c128bec8..ef2501de 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -374,9 +374,12 @@ namespace Microsoft.Boogie {
}
foreach (var t in definedFunctions) {
- var f = m.MkFunc(t.Key, t.Value.Count - 1);
+ var tuples = t.Value;
+ if (tuples.Count == 0) continue;
+
+ var f = m.MkFunc(t.Key, tuples[0].Count - 1);
var args = new Model.Element[f.Arity];
- foreach (var l in t.Value) {
+ foreach (var l in tuples) {
if (l.Count == 1) continue;
for (int i = 0; i < f.Arity; ++i)
args[i] = elts[l[i]];
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 55cfa650..eda5cfda 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -177,7 +177,26 @@ namespace Microsoft.Boogie {
}
}
- public void PrintModel() {
+ static bool firstModelFile = true;
+
+ public void PrintModel()
+ {
+ var filename = CommandLineOptions.Clo.ModelViewFile;
+ if (Model == null || filename == null) return;
+
+ var m = this.GetModelWithStates();
+
+ if (filename == "-") {
+ m.Write(Console.Out);
+ Console.Out.Flush();
+ } else {
+ using (var wr = new StreamWriter(filename, !firstModelFile)) {
+ firstModelFile = false;
+ m.Write(wr);
+ }
+ }
+
+ /*
if (Model == null || MvInfo == null) {
return;
}
@@ -267,6 +286,7 @@ namespace Microsoft.Boogie {
Console.WriteLine(" undefined captured-state ID {0}", s);
}
}
+ */
}
public Model GetModelWithStates()
@@ -307,7 +327,12 @@ namespace Microsoft.Boogie {
if (e is IdentifierExpr) {
IdentifierExpr ide = (IdentifierExpr)e;
- elt = m.GetFunc(ide.Decl.Name).GetConstant();
+
+ var f = m.TryGetFunc(ide.Decl.Name);
+ if (f == null) {
+ f = m.MkFunc(ide.Decl.Name, 0);
+ }
+ elt = f.GetConstant();
} else if (e is LiteralExpr) {
LiteralExpr lit = (LiteralExpr)e;
elt = m.MkElement(lit.Val.ToString());
@@ -1397,7 +1422,7 @@ namespace VC {
Contract.Assert(pc != null);
Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
- if (0 < CommandLineOptions.Clo.ModelView && pc is AssumeCmd) {
+ if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) {
string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");
if (description != null) {
Expr mv = new NAryExpr(pc.tok, new FunctionCall(mvInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Literal(mvInfo.CapturePoints.Count)));
diff --git a/Source/VCGeneration/Model.cs b/Source/VCGeneration/Model.cs
index 331d287a..d2d9cc24 100644
--- a/Source/VCGeneration/Model.cs
+++ b/Source/VCGeneration/Model.cs
@@ -21,7 +21,7 @@ namespace Microsoft.Boogie
abstract public class Element
{
- protected readonly Model parent;
+ public readonly Model Model;
internal List<FuncTuple> references = new List<FuncTuple>();
public readonly int Id;
@@ -48,7 +48,7 @@ namespace Microsoft.Boogie
}
}
- protected Element(Model p) { parent = p; }
+ protected Element(Model p) { Model = p; }
public abstract ElementKind Kind { get; }
public virtual int AsInt() { throw new NotImplementedException(); }
}
@@ -94,13 +94,13 @@ namespace Microsoft.Boogie
public class Func
{
- private readonly Model Parent;
+ public readonly Model Model;
public readonly string Name;
public readonly int Arity;
internal readonly List<FuncTuple> apps = new List<FuncTuple>();
public IEnumerable<FuncTuple> Apps { get { return apps; } }
- internal Func(Model p, string n, int a) { Parent = p; Name = n; Arity = a; }
+ internal Func(Model p, string n, int a) { Model = p; Name = n; Arity = a; }
public void SetConstant(Element res)
{
@@ -116,7 +116,7 @@ namespace Microsoft.Boogie
if (Arity != 0)
throw new ArgumentException();
if (apps.Count == 0)
- SetConstant(Parent.MkElement("**" + Name));
+ SetConstant(Model.MkElement("**" + Name));
return apps[0].Result;
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 304130ef..9e8b2dc8 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -3021,6 +3021,7 @@ namespace VC {
errModel.Print(ErrorReporter.ModelWriter);
ErrorReporter.ModelWriter.Flush();
}
+
Hashtable traceNodes = new Hashtable();
foreach (string s in labels) {
Contract.Assert(s != null);
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 10:22:44 +0000