summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/ConditionGeneration.cs
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-12-07 15:58:48 +0100
committerGravatar wuestholz <unknown>2014-12-07 15:58:48 +0100
commit575d226a8e15efc111bfaf57f188261e12f7ef95 (patch)
tree2a57a6b29c7dcddc1a01bb8b750c0b2500134a70 /Source/VCGeneration/ConditionGeneration.cs
parenteceff3c25df3be34a5abafbb9dcb9ad550a11d33 (diff)
Optimized the VC generation for assumption variables.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs27
1 files changed, 27 insertions, 0 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 178f8ddb..aca9d3f8 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1684,6 +1684,15 @@ namespace VC {
dropCmd = true;
}
}
+ else if (pc is AssumeCmd && QKeyValue.FindBoolAttribute(pc.Attributes, "assumption_variable_initialization"))
+ {
+ var identExpr = pc.Expr as IdentifierExpr;
+ if (identExpr != null && identExpr.Decl != null && !incarnationMap.ContainsKey(identExpr.Decl))
+ {
+ incarnationMap[identExpr.Decl] = LiteralExpr.True;
+ dropCmd = true;
+ }
+ }
pc.Expr = copy;
if (!dropCmd)
{
@@ -1739,6 +1748,24 @@ namespace VC {
newIncarnationMappings[lhs] = x_prime_exp;
}
#endregion
+
+ var nAryExpr = copies[i] as NAryExpr;
+ if (nAryExpr != null)
+ {
+ var binOp = nAryExpr.Fun as BinaryOperator;
+ if (binOp != null
+ && binOp.Op == BinaryOperator.Opcode.And)
+ {
+ var arg0 = nAryExpr.Args[0] as LiteralExpr;
+ var arg1 = nAryExpr.Args[1] as LiteralExpr;
+ if ((arg0 != null && arg0.IsTrue) || (arg1 != null && arg1.IsFalse))
+ {
+ // Replace the expressions "true && arg1" or "arg0 && false" by "arg1".
+ copies[i] = nAryExpr.Args[1];
+ }
+ }
+ }
+
#region Create an assume command with the new variable
assumptions.Add(TypedExprEq(x_prime_exp, copies[i]));
#endregion