summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/ConditionGeneration.cs
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2016-06-05 15:01:52 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2016-06-05 15:01:52 -0400
commit41082463d783d6f8d8a5aaf69bf459b57bca6000 (patch)
tree8b9dca4b583b9cb1ea7ed220fe34d611217eb6cc /Source/VCGeneration/ConditionGeneration.cs
parent64e8b33656140b87137d0662d9e6835e004d13c2 (diff)
parent8ed5dab22d8377924ee6282b83c1b1f8aa8f3573 (diff)
Merge branch 'upstream' into dfsg_free
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs36
1 files changed, 34 insertions, 2 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 1f010757..19438924 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -85,6 +85,7 @@ namespace Microsoft.Boogie {
public string RequestId;
public abstract byte[] Checksum { get; }
public byte[] SugaredCmdChecksum;
+ public bool IsAuxiliaryCexForDiagnosingTimeouts;
public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
@@ -313,7 +314,7 @@ namespace Microsoft.Boogie {
public abstract int GetLocation();
}
- public class CounterexampleComparer : IComparer<Counterexample> {
+ public class CounterexampleComparer : IComparer<Counterexample>, IEqualityComparer<Counterexample> {
private int Compare(List<Block> bs1, List<Block> bs2)
{
@@ -375,6 +376,16 @@ namespace Microsoft.Boogie {
}
return -1;
}
+
+ public bool Equals(Counterexample x, Counterexample y)
+ {
+ return Compare(x, y) == 0;
+ }
+
+ public int GetHashCode(Counterexample obj)
+ {
+ return 0;
+ }
}
public class AssertCounterexample : Counterexample {
@@ -1122,7 +1133,8 @@ namespace VC {
}
if (returnBlocks > 1) {
string unifiedExitLabel = "GeneratedUnifiedExit";
- Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(Token.NoToken));
+ Block unifiedExit;
+ unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken));
Contract.Assert(unifiedExit != null);
foreach (Block b in impl.Blocks) {
if (b.TransferCmd is ReturnCmd) {
@@ -1528,6 +1540,26 @@ namespace VC {
PredicateCmd pc = (PredicateCmd)c.Clone();
Contract.Assert(pc != null);
+ QKeyValue current = pc.Attributes;
+ while (current != null)
+ {
+ if (current.Key == "minimize" || current.Key == "maximize") {
+ Contract.Assume(current.Params.Count == 1);
+ var param = current.Params[0] as Expr;
+ Contract.Assume(param != null && (param.Type.IsInt || param.Type.IsReal || param.Type.IsBv));
+ current.ClearParams();
+ current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+ }
+ if (current.Key == "verified_under") {
+ Contract.Assume(current.Params.Count == 1);
+ var param = current.Params[0] as Expr;
+ Contract.Assume(param != null && param.Type.IsBool);
+ current.ClearParams();
+ current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+ }
+ current = current.Next;
+ }
+
Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) {
string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");