summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/ConditionGeneration.cs
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-10-18 12:28:58 +0200
committerGravatar wuestholz <unknown>2014-10-18 12:28:58 +0200
commit46fa485c2ad3736f1428e748b53cef917ae2afb8 (patch)
tree4a8a908d4fc9cd6fcf6d9c8cbbec2f9f71499512 /Source/VCGeneration/ConditionGeneration.cs
parent657c04b52dfbd2ab0323cd481fc6745fd51a05de (diff)
Did some refactoring.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs49
1 files changed, 23 insertions, 26 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 6fa26967..64a85171 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1336,10 +1336,10 @@ namespace VC {
Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);
var end = DateTime.UtcNow;
+
if (3 <= CommandLineOptions.Clo.TraceCaching)
{
- Console.Out.WriteLine("\nTurned implementation into passive commands within {0:F0} ms.\n", end.Subtract(start).TotalMilliseconds);
-
+ Console.Out.WriteLine("Turned implementation into passive commands within {0:F0} ms.\n", end.Subtract(start).TotalMilliseconds);
}
if (2 <= CommandLineOptions.Clo.TraceCaching)
@@ -1470,22 +1470,23 @@ namespace VC {
return Substituter.SubstitutionFromHashtable(oldFrameMap);
}
- void TraceCachingTransformation(Cmd from, string message, Cmd to = null)
+ void TraceCaching(Cmd from, string message, Cmd to = null)
{
if (1 <= CommandLineOptions.Clo.TraceCaching)
{
- Console.WriteLine("");
using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))
{
+ var loc = from.tok != null && from.tok != Token.NoToken ? string.Format("{0}({1},{2})", from.tok.filename, from.tok.line, from.tok.col) : "<unknown location>";
+ Console.Write("Processing command (at {0}) ", loc);
from.Emit(tokTxtWr, 0);
- Console.Write(message);
+ Console.Out.Write(" {0}", message);
if (to != null)
{
to.Emit(tokTxtWr, 0);
}
else
{
- Console.WriteLine("");
+ Console.Out.WriteLine();
}
}
}
@@ -1538,11 +1539,11 @@ namespace VC {
&& !currentImplementation.AnyErrorsInCachedSnapshot
&& currentImplementation.InjectedAssumptionVariables.Count == 1)
{
- TraceCachingTransformation(pc, "==> did nothing\n");
+ TraceCaching(pc, ">>> did nothing");
}
else if (relevantDoomedAssumpVars.Any())
{
- TraceCachingTransformation(pc, "==> did nothing\n");
+ TraceCaching(pc, ">>> did nothing");
}
else if (currentImplementation != null
&& currentImplementation.HasCachedSnapshot
@@ -1561,19 +1562,17 @@ namespace VC {
ac.IncarnationMap[incarnation] = identExpr;
passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));
copy = identExpr;
- var a = new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr));
- passiveCmds.Add(a);
- TraceCachingTransformation(pc, "== marked as partially verified ==> ", a);
+ passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr)));
+ TraceCaching(pc, string.Format(">>> added assume statement for assertion that has been partially verified under \"{0}\"", assmVars));
}
else if (isTrue)
{
if (alwaysUseSubsumption)
{
// Turn it into an assume statement.
- var a = new AssumeCmd(ac.tok, copy);
- a.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), a.Attributes);
- TraceCachingTransformation(pc, "== marked as fully verified ==> ", a);
- pc = a;
+ TraceCaching(pc, ">>> turned assertion into assume statement");
+ pc = new AssumeCmd(ac.tok, copy);
+ pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
}
dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;
}
@@ -1588,10 +1587,9 @@ namespace VC {
if (alwaysUseSubsumption)
{
// Turn it into an assume statement.
- var a = new AssumeCmd(ac.tok, copy);
- a.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), a.Attributes);
- TraceCachingTransformation(pc, "== recycled error ==> ", a);
- pc = a;
+ TraceCaching(pc, ">>> recycled error and turned assertion into assume statement");
+ pc = new AssumeCmd(ac.tok, copy);
+ pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);
}
dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;
if (dropCmd || alwaysUseSubsumption)
@@ -1601,7 +1599,7 @@ namespace VC {
}
else
{
- TraceCachingTransformation(pc, "==> did nothing\n");
+ TraceCaching(pc, ">>> did nothing");
}
}
else if (pc is AssumeCmd
@@ -1618,11 +1616,11 @@ namespace VC {
if (!isTrue)
{
copy = LiteralExpr.Imp(assmVars, copy);
- TraceCachingTransformation(pc, "==> marked as partially verified\n");
+ TraceCaching(pc, string.Format(">>> marked as partially verified under \"{0}\"", assmVars));
}
else
{
- TraceCachingTransformation(pc, "==> marked as full verified\n");
+ TraceCaching(pc, ">>> marked as full verified");
}
}
else
@@ -1637,7 +1635,7 @@ namespace VC {
}
else
{
- TraceCachingTransformation(pc, "==> dropped\n");
+ TraceCaching(pc, ">>> dropped");
}
}
#endregion
@@ -1720,9 +1718,8 @@ namespace VC {
Expr incarnation;
if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption") && incarnationMap.TryGetValue(identExpr.Decl, out incarnation))
{
- var a = new AssumeCmd(c.tok, Expr.Not(incarnation));
- TraceCachingTransformation(assign, "== assumed negation of single assumption variable ==> ", a);
- passiveCmds.Add(a);
+ TraceCaching(assign, string.Format(">>> added assume statement for negation of single assumption variable \"{0}\"", identExpr.Decl.Name));
+ passiveCmds.Add(new AssumeCmd(c.tok, Expr.Not(incarnation)));
}
}
}