summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r--Source/VCGeneration/Check.cs9
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs36
-rw-r--r--Source/VCGeneration/StratifiedVC.cs11
-rw-r--r--Source/VCGeneration/VC.cs259
-rw-r--r--Source/VCGeneration/Wlp.cs39
5 files changed, 329 insertions, 25 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 3c3b5cae..7bda0022 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -356,7 +356,7 @@ namespace Microsoft.Boogie {
hasOutput = false;
outputExn = null;
this.handler = handler;
-
+
thmProver.Reset(gen);
SetTimeout();
proverStart = DateTime.UtcNow;
@@ -386,6 +386,7 @@ namespace Microsoft.Boogie {
// -----------------------------------------------------------------------------------------------
public abstract class ProverInterface {
+
public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
Contract.Requires(prog != null);
@@ -452,6 +453,10 @@ namespace Microsoft.Boogie {
Undetermined,
Bounded
}
+
+ public readonly ISet<VCExprVar> NamedAssumes = new HashSet<VCExprVar>();
+ public ISet<string> UsedNamedAssumes { get; protected set; }
+
public class ErrorHandler {
// Used in CheckOutcomeCore
public virtual int StartingProcId()
@@ -542,7 +547,7 @@ namespace Microsoft.Boogie {
}
// (assert vc)
- public virtual void Assert(VCExpr vc, bool polarity)
+ public virtual void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1)
{
throw new NotImplementedException();
}
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");
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 0e598267..789f86f5 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -584,9 +584,6 @@ namespace VC {
vcgen.ConvertCFG2DAG(impl);
vcgen.PassifyImpl(impl, out mvInfo);
- if (PassiveImplInstrumentation != null)
- PassiveImplInstrumentation(impl);
-
VCExpressionGenerator gen = proverInterface.VCExprGen;
var exprGen = proverInterface.Context.ExprGen;
var translator = proverInterface.Context.BoogieExprTranslator;
@@ -599,6 +596,9 @@ namespace VC {
vcgen.InstrumentCallSites(impl);
+ if (PassiveImplInstrumentation != null)
+ PassiveImplInstrumentation(impl);
+
label2absy = new Dictionary<int, Absy>();
VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, proverInterface.Context);
translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition);
@@ -639,6 +639,7 @@ namespace VC {
public abstract class StratifiedVCGenBase : VCGen {
public readonly static string recordProcName = "boogie_si_record";
+ public readonly static string callSiteVarAttr = "callSiteVar";
public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
public ProverInterface prover;
@@ -699,7 +700,9 @@ namespace VC {
if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue;
Variable callSiteVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "SICS" + callSiteId, Microsoft.Boogie.Type.Bool));
implementation.LocVars.Add(callSiteVar);
- newCmds.Add(new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar)));
+ var toInsert = new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar),
+ new QKeyValue(Token.NoToken, callSiteVarAttr, new List<object>(), null));
+ newCmds.Add(toInsert);
callSiteId++;
}
block.Cmds = newCmds;
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index bf25e042..6e43e917 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1519,7 +1519,7 @@ namespace VC {
}
}
- public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext)
+ public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null)
{
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
@@ -1527,10 +1527,10 @@ namespace VC {
Contract.Ensures(Contract.Result<VCExpr>() != null);
label2absy = new Dictionary<int, Absy>();
- return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);
+ return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext, namedAssumeVars: namedAssumeVars);
}
- public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {
+ public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null) {
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -1632,7 +1632,7 @@ namespace VC {
//use Duplicator and Substituter rather than new
//nested IToken?
//document expand attribute (search for {:ignore}, for example)
- //fix up new CallCmd, new Requires, new Ensures in OwickiGries.cs
+ //fix up new CallCmd, new Requires, new Ensures in CivlRefinement.cs
Func<Expr,Expr,Expr> withType = (Expr from, Expr to) =>
{
NAryExpr nFrom = from as NAryExpr;
@@ -1763,9 +1763,18 @@ namespace VC {
{
var checksum = a.Checksum;
var oldCex = impl.ErrorChecksumToCachedError[checksum] as Counterexample;
- if (oldCex != null)
- {
- callback.OnCounterexample(oldCex, null);
+ if (oldCex != null) {
+ if (CommandLineOptions.Clo.VerifySnapshots < 3) {
+ callback.OnCounterexample(oldCex, null);
+ } else {
+ // If possible, we use the old counterexample, but with the location information of "a"
+ var cex = AssertCmdToCloneCounterexample(a, oldCex);
+ callback.OnCounterexample(cex, null);
+ // OnCounterexample may have had side effects on the RequestId and OriginalRequestId fields. We make
+ // any such updates available in oldCex. (Is this really a good design? --KRML)
+ oldCex.RequestId = cex.RequestId;
+ oldCex.OriginalRequestId = cex.OriginalRequestId;
+ }
}
}
}
@@ -2012,6 +2021,16 @@ namespace VC {
protected ProverContext/*!*/ context;
Program/*!*/ program;
+ public IEnumerable<string> NecessaryAssumes
+ {
+ get { return program.NecessaryAssumes; }
+ }
+
+ public void AddNecessaryAssume(string id)
+ {
+ program.NecessaryAssumes.Add(id);
+ }
+
public ErrorReporter(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,
Dictionary<int, Absy>/*!*/ label2absy,
List<Block/*!*/>/*!*/ blocks,
@@ -2104,6 +2123,7 @@ namespace VC {
foreach (var cmd in assertCmds)
{
Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List<Block>(), null, null, context);
+ cex.IsAuxiliaryCexForDiagnosingTimeouts = true;
callback.OnCounterexample(cex, msg);
}
}
@@ -2219,10 +2239,11 @@ namespace VC {
impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] })));
ResetPredecessors(impl.Blocks);
- if(CommandLineOptions.Clo.KInductionDepth < 0) {
+ var k = Math.Max(CommandLineOptions.Clo.KInductionDepth, QKeyValue.FindIntAttribute(impl.Attributes, "kInductionDepth", -1));
+ if(k < 0) {
ConvertCFG2DAGStandard(impl, edgesCut, taskID);
} else {
- ConvertCFG2DAGKInduction(impl, edgesCut, taskID);
+ ConvertCFG2DAGKInduction(impl, edgesCut, taskID, k);
}
#region Debug Tracing
@@ -2487,14 +2508,12 @@ namespace VC {
return referencedVars;
}
- private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID) {
+ private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID, int inductionK) {
// K-induction has not been adapted to be aware of these parameters which standard CFG to DAG transformation uses
Contract.Requires(edgesCut == null);
Contract.Requires(taskID == -1);
-
- int inductionK = CommandLineOptions.Clo.KInductionDepth;
- Contract.Assume(inductionK >= 0);
+ Contract.Requires(0 <= inductionK);
bool contRuleApplication = true;
while (contRuleApplication) {
@@ -2809,6 +2828,11 @@ namespace VC {
mvInfo = new ModelViewInfo(program, impl);
Convert2PassiveCmd(impl, mvInfo);
+ if (QKeyValue.FindBoolAttribute(impl.Attributes, "may_unverified_instrumentation"))
+ {
+ InstrumentWithMayUnverifiedConditions(impl, exitBlock);
+ }
+
#region Peep-hole optimizations
if (CommandLineOptions.Clo.RemoveEmptyBlocks){
#region Get rid of empty blocks
@@ -2844,6 +2868,190 @@ namespace VC {
return gotoCmdOrigins;
}
+ #region Simplified May-Unverified Analysis and Instrumentation
+
+ static void InstrumentWithMayUnverifiedConditions(Implementation impl, Block unifiedExitBlock)
+ {
+ var q = new Queue<Block>();
+ q.Enqueue(unifiedExitBlock);
+ var conditionOnBlockEntry = new Dictionary<Block, HashSet<Variable>>();
+ while (q.Any())
+ {
+ var block = q.Dequeue();
+
+ if (conditionOnBlockEntry.ContainsKey(block))
+ {
+ continue;
+ }
+
+ var gotoCmd = block.TransferCmd as GotoCmd;
+ if (gotoCmd != null && gotoCmd.labelTargets.Any(b => !conditionOnBlockEntry.ContainsKey(b)))
+ {
+ q.Enqueue(block);
+ continue;
+ }
+
+ HashSet<Variable> cond = new HashSet<Variable>();
+ if (gotoCmd != null)
+ {
+ var mayInstrs = new List<Block>();
+ bool noInstr = true;
+ foreach (var succ in gotoCmd.labelTargets)
+ {
+ var c = conditionOnBlockEntry[succ];
+ if (c != null)
+ {
+ mayInstrs.Add(succ);
+ }
+ else
+ {
+ noInstr = false;
+ }
+ cond = JoinVariableSets(cond, c);
+ }
+ if (!noInstr)
+ {
+ foreach (var instr in mayInstrs)
+ {
+ InstrumentWithCondition(instr, 0, conditionOnBlockEntry[instr]);
+ }
+ }
+ }
+
+ for (int i = block.Cmds.Count - 1; 0 <= i; i--)
+ {
+ var cmd = block.Cmds[i];
+ if (cond == null) { break; }
+
+ var assertCmd = cmd as AssertCmd;
+ if (assertCmd != null)
+ {
+ var litExpr = assertCmd.Expr as LiteralExpr;
+ if (litExpr != null && litExpr.IsTrue)
+ {
+ continue;
+ }
+
+ HashSet<Variable> vu = null;
+ if (assertCmd.VerifiedUnder == null)
+ {
+ vu = null;
+ }
+ else
+ {
+ HashSet<Variable> vars;
+ if (IsConjunctionOfAssumptionVariables(assertCmd.VerifiedUnder, out vars))
+ {
+ vu = vars;
+ // TODO(wuestholz): Maybe drop the :verified_under attribute.
+ }
+ else
+ {
+ vu = null;
+ }
+ }
+
+ if (vu == null)
+ {
+ InstrumentWithCondition(block, i + 1, cond);
+ }
+
+ cond = JoinVariableSets(cond, vu);
+ }
+ }
+
+ if (cond != null && block.Predecessors.Count == 0)
+ {
+ // TODO(wuestholz): Should we rather instrument each block?
+ InstrumentWithCondition(block, 0, cond);
+ }
+
+ foreach (var pred in block.Predecessors)
+ {
+ q.Enqueue(pred);
+ }
+
+ conditionOnBlockEntry[block] = cond;
+ }
+ }
+
+ private static void InstrumentWithCondition(Block block, int idx, HashSet<Variable> condition)
+ {
+ var conj = Expr.BinaryTreeAnd(condition.Select(v => (Expr)new IdentifierExpr(Token.NoToken, v)).ToList());
+ block.Cmds.Insert(idx, new AssumeCmd(Token.NoToken, Expr.Not(conj)));
+ }
+
+ static HashSet<Variable> JoinVariableSets(HashSet<Variable> c0, HashSet<Variable> c1)
+ {
+ // We use the following lattice:
+ // - Top: null (i.e., true)
+ // - Bottom: new HashSet<Variable>() (i.e., false)
+ // - Other Elements: new HashSet<Variable>(...) (i.e., conjunctions of assumption variables)
+
+ if (c0 == null || c1 == null)
+ {
+ return null;
+ }
+ var result = new HashSet<Variable>(c0);
+ result.UnionWith(c1);
+ return result;
+ }
+
+ static bool IsAssumptionVariableOrIncarnation(Variable v)
+ {
+ if (QKeyValue.FindBoolAttribute(v.Attributes, "assumption")) { return true; }
+ var incar = v as Incarnation;
+ return incar == null || QKeyValue.FindBoolAttribute(incar.OriginalVariable.Attributes, "assumption");
+ }
+
+ static bool IsConjunctionOfAssumptionVariables(Expr expr, out HashSet<Variable> variables)
+ {
+ Contract.Requires(expr != null);
+
+ variables = null;
+ var litExpr = expr as LiteralExpr;
+ if (litExpr != null && (litExpr.IsFalse || litExpr.IsTrue))
+ {
+ if (litExpr.IsTrue)
+ {
+ variables = new HashSet<Variable>();
+ }
+ return true;
+ }
+
+ var idExpr = expr as IdentifierExpr;
+ if (idExpr != null && IsAssumptionVariableOrIncarnation(idExpr.Decl))
+ {
+ variables = new HashSet<Variable>();
+ variables.Add(idExpr.Decl);
+ return true;
+ }
+
+ var andExpr = expr as NAryExpr;
+ if (andExpr != null)
+ {
+ var fun = andExpr.Fun as BinaryOperator;
+ if (fun != null && fun.Op == BinaryOperator.Opcode.And && andExpr.Args != null)
+ {
+ bool res = true;
+ variables = new HashSet<Variable>();
+ foreach (var op in andExpr.Args)
+ {
+ HashSet<Variable> vars;
+ var r = IsConjunctionOfAssumptionVariables(op, out vars);
+ res &= r;
+ variables = JoinVariableSets(variables, vars);
+ if (!res) { break; }
+ }
+ return res;
+ }
+ }
+
+ return false;
+ }
+
+ #endregion
+
private static void HandleSelectiveChecking(Implementation impl)
{
if (QKeyValue.FindBoolAttribute(impl.Attributes, "selective_checking") ||
@@ -3137,6 +3345,31 @@ namespace VC {
}
}
+ /// <summary>
+ /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt".
+ /// </summary>
+ public static Counterexample AssertCmdToCloneCounterexample(AssertCmd assrt, Counterexample cex) {
+ Contract.Requires(assrt != null);
+ Contract.Requires(cex != null);
+ Contract.Ensures(Contract.Result<Counterexample>() != null);
+
+ List<string> relatedInformation = new List<string>();
+
+ Counterexample cc;
+ if (assrt is AssertRequiresCmd) {
+ var aa = (AssertRequiresCmd)assrt;
+ cc = new CallCounterexample(cex.Trace, aa.Call, aa.Requires, cex.Model, cex.MvInfo, cex.Context, aa.Checksum);
+ } else if (assrt is AssertEnsuresCmd && cex is ReturnCounterexample) {
+ var aa = (AssertEnsuresCmd)assrt;
+ var oldCex = (ReturnCounterexample)cex;
+ cc = new ReturnCounterexample(cex.Trace, oldCex.FailingReturn, aa.Ensures, cex.Model, cex.MvInfo, cex.Context, aa.Checksum);
+ } else {
+ cc = new AssertCounterexample(cex.Trace, assrt, cex.Model, cex.MvInfo, cex.Context);
+ }
+ cc.relatedInformation = relatedInformation;
+ return cc;
+ }
+
static VCExpr LetVC(Block startBlock,
VCExpr controlFlowVariableExpr,
Dictionary<int, Absy> label2absy,
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index b4ee4c09..cad5914b 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -87,7 +87,7 @@ namespace VC {
/// <summary>
/// Computes the wlp for an assert or assume command "cmd".
/// </summary>
- public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
+ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
Contract.Requires(cmd != null);
Contract.Requires(N != null);
Contract.Requires(ctxt != null);
@@ -186,17 +186,48 @@ namespace VC {
if (naryExpr.Fun is FunctionCall) {
int id = ac.UniqueId;
ctxt.Label2absy[id] = ac;
- return gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
+ return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N));
}
}
}
- return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
+ var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
+
+ var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id");
+ if (aid != null)
+ {
+ var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try");
+ var v = gen.Variable((isTry ? "try$$" : "assume$$") + aid, Microsoft.Boogie.Type.Bool);
+ expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr));
+ }
+ var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft");
+ var softWeight = QKeyValue.FindIntAttribute(ac.Attributes, "soft", 0);
+ if ((soft || 0 < softWeight) && aid != null)
+ {
+ var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool);
+ expr = gen.Function(new VCExprSoftOp(Math.Max(softWeight, 1)), v, gen.ImpliesSimp(v, expr));
+ }
+ return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N));
} else {
Console.WriteLine(cmd.ToString());
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command
}
}
-
+
+ private static VCExpr MaybeWrapWithOptimization(VCContext ctxt, VCExpressionGenerator gen, QKeyValue attrs, VCExpr expr)
+ {
+ var min = QKeyValue.FindExprAttribute(attrs, "minimize");
+ if (min != null)
+ {
+ expr = gen.Function(VCExpressionGenerator.MinimizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(min), expr);
+ }
+ var max = QKeyValue.FindExprAttribute(attrs, "maximize");
+ if (max != null)
+ {
+ expr = gen.Function(VCExpressionGenerator.MaximizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(max), expr);
+ }
+ return expr;
+ }
+
public static CommandLineOptions.SubsumptionOption Subsumption(AssertCmd ac) {
Contract.Requires(ac != null);
int n = QKeyValue.FindIntAttribute(ac.Attributes, "subsumption", -1);
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 10:58:15 +0000