diff options
| -rw-r--r-- | Source/Dafny/Translator.cs | 224 | ||||
| -rw-r--r-- | Test/dafny0/Fuel.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/Fuel.dfy.expect | 10 | ||||
| -rw-r--r-- | Test/dafny4/Bug93.dfy | 37 | ||||
| -rw-r--r-- | Test/dafny4/Bug93.dfy.expect | 8 |
5 files changed, 249 insertions, 34 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 28077842..9466f18a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -113,6 +113,7 @@ namespace Microsoft.Dafny { readonly Dictionary<TopLevelDecl, string>/*!*/ classConstants = new Dictionary<TopLevelDecl, string>();
readonly Dictionary<int, string> functionConstants = new Dictionary<int, string>();
readonly Dictionary<Function, string> functionHandles = new Dictionary<Function, string>();
+ readonly static List<FuelConstant> FunctionFuel = new List<FuelConstant>();
readonly Dictionary<Field/*!*/,Bpl.Constant/*!*/>/*!*/ fields = new Dictionary<Field/*!*/,Bpl.Constant/*!*/>();
readonly Dictionary<Field/*!*/, Bpl.Function/*!*/>/*!*/ fieldFunctions = new Dictionary<Field/*!*/, Bpl.Function/*!*/>();
readonly Dictionary<string, Bpl.Constant> fieldConstants = new Dictionary<string,Constant>();
@@ -488,6 +489,9 @@ namespace Microsoft.Dafny { return new Bpl.Program();
}
+ // compute which function needs fuel constants.
+ ComputeFunctionFuel();
+
foreach (TopLevelDecl d in program.BuiltIns.SystemModule.TopLevelDecls) {
currentDeclaration = d;
if (d is OpaqueTypeDecl) {
@@ -577,6 +581,37 @@ namespace Microsoft.Dafny { return sink;
}
+ private void ComputeFunctionFuel() {
+ foreach (ModuleDefinition m in program.Modules) {
+ foreach (TopLevelDecl d in m.TopLevelDecls) {
+ if (d is ClassDecl) {
+ ClassDecl c = (ClassDecl)d;
+ foreach (MemberDecl member in c.Members) {
+ if (member is Function) {
+ Function f = (Function)member;
+ // declare the fuel constant
+ if (f.IsFueled) {
+ // const BaseFuel_FunctionA : LayerType
+ Bpl.Constant baseFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "BaseFuel_" + f.FullName, predef.LayerType), false);
+ sink.AddTopLevelDeclaration(baseFuel);
+ Bpl.Expr baseFuel_expr = new Bpl.IdentifierExpr(f.tok, baseFuel);
+ // const StartFuel_FunctionA : LayerType
+ Bpl.Constant startFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuel_" + f.FullName, predef.LayerType), false);
+ sink.AddTopLevelDeclaration(startFuel);
+ Bpl.Expr startFuel_expr = new Bpl.IdentifierExpr(f.tok, startFuel);
+ // const StartFuelAssert_FunctionA : LayerType
+ Bpl.Constant startFuelAssert = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuelAssert_" + f.FullName, predef.LayerType), false);
+ sink.AddTopLevelDeclaration(startFuelAssert);
+ Bpl.Expr startFuelAssert_expr = new Bpl.IdentifierExpr(f.tok, startFuelAssert);
+ Translator.FunctionFuel.Add(new FuelConstant(f, baseFuel_expr, startFuel_expr, startFuelAssert_expr));
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
/// <summary>
/// adding TraitParent axioms
/// if a class A extends trait J and B does not extend anything, then this method adds the followings to the sink:
@@ -2755,6 +2790,7 @@ namespace Microsoft.Dafny { Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
builder.Add(new CommentCmd("AddMethodImpl: " + m + ", " + proc));
ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
+ InitializeFuelConstant(m.tok, builder, etran);
List<Variable> localVariables = new List<Variable>();
GenerateImplPrelude(m, wellformednessProc, inParams, outParams, builder, localVariables);
@@ -2934,6 +2970,52 @@ namespace Microsoft.Dafny { Reset();
}
+ void InitializeFuelConstant(IToken tok, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {
+ builder.Add(new CommentCmd("initialize fuel constant"));
+ FuelContext fuelContext = this.fuelContext;
+ foreach (FuelConstant fuelConstant in Translator.FunctionFuel) {
+ Function f = fuelConstant.f;
+ Bpl.Expr baseFuel = fuelConstant.baseFuel;
+ Bpl.Expr startFuel = fuelConstant.startFuel;
+ Bpl.Expr startFuelAssert = fuelConstant.startFuelAssert;
+ // find out what the initial value should be
+ FuelSettingPair settings;
+ var found = fuelContext.TryGetValue(f, out settings);
+ if (!found) {
+ // If the context doesn't define fuel for this function, check for a fuel attribute (which supplies a default value if none is found)
+ settings = FuelSetting.FuelAttrib(f, out found);
+ }
+
+ Bpl.Expr layer = etran.layerInterCluster.LayerN(settings.low, baseFuel);
+ Bpl.Expr layerAssert = etran.layerInterCluster.LayerN(settings.high, baseFuel);
+ builder.Add(TrAssumeCmd(tok, Bpl.Expr.Eq(startFuel, layer)));
+ builder.Add(TrAssumeCmd(tok, Bpl.Expr.Eq(startFuelAssert, layerAssert)));
+ }
+ }
+
+ bool DefineFuelConstant(IToken tok, Attributes attribs, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {
+ bool defineFuel = false;
+ builder.Add(new CommentCmd("Assume Fuel Constant"));
+ FuelContext fuelContext = new FuelContext();
+ FuelSetting.FindFuelAttributes(attribs, fuelContext);
+ foreach (KeyValuePair<Function, FuelSettingPair> fuel in fuelContext) {
+ Function f = fuel.Key;
+ FuelSettingPair settings = fuel.Value;
+ FuelConstant fuelConstant = Translator.FunctionFuel.Find(x => x.f == f);
+ if (fuelConstant != null) {
+ Bpl.Expr startFuel = fuelConstant.startFuel;
+ Bpl.Expr startFuelAssert = fuelConstant.startFuelAssert;
+ Bpl.Expr moreFuel_expr = fuelConstant.MoreFuel(sink, predef, f.IdGenerator);
+ Bpl.Expr layer = etran.layerInterCluster.LayerN(settings.low, moreFuel_expr);
+ Bpl.Expr layerAssert = etran.layerInterCluster.LayerN(settings.high, moreFuel_expr);
+ builder.Add(TrAssumeCmd(tok, Bpl.Expr.Eq(startFuel, layer)));
+ builder.Add(TrAssumeCmd(tok, Bpl.Expr.Eq(startFuelAssert, layerAssert)));
+ defineFuel = true;
+ }
+ }
+ return defineFuel;
+ }
+
internal static AssumeCmd optimizeExpr(bool minimize, Expression expr, IToken tok, ExpressionTranslator etran)
{
Contract.Requires(expr != null);
@@ -4032,7 +4114,7 @@ namespace Microsoft.Dafny { builder.Add(CaptureState(f.tok, false, "initial state"));
DefineFrame(f.tok, f.Reads, builder, locals, null);
-
+ InitializeFuelConstant(f.tok, builder, etran);
// Check well-formedness of the preconditions (including termination), and then
// assume each one of them. After all that (in particular, after assuming all
// of them), do the postponed reads checks.
@@ -7113,11 +7195,14 @@ namespace Microsoft.Dafny { Contract.Requires(codeContext != null && predef != null);
Contract.Ensures(fuelContext == Contract.OldValue(fuelContext));
if (stmt is PredicateStmt) {
- this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);
+ var stmtBuilder = new Bpl.StmtListBuilder();
+ this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, stmt.Tok, this.fuelContext, this.reporter);
+ var defineFuel = DefineFuelConstant(stmt.Tok, stmt.Attributes, stmtBuilder, etran);
+ var b = defineFuel ? stmtBuilder : builder;
if (stmt is AssertStmt || DafnyOptions.O.DisallowSoundnessCheating) {
- AddComment(builder, stmt, "assert statement");
+ AddComment(b, stmt, "assert statement");
PredicateStmt s = (PredicateStmt)stmt;
- TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
+ TrStmt_CheckWellformed(s.Expr, b, locals, etran, false);
IToken enclosingToken = null;
if (Attributes.Contains(stmt.Attributes, "prependAssertToken")) {
enclosingToken = stmt.Tok;
@@ -7126,14 +7211,21 @@ namespace Microsoft.Dafny { var ss = TrSplitExpr(s.Expr, etran, true, out splitHappened);
if (!splitHappened) {
var tok = enclosingToken == null ? s.Expr.tok : new NestedToken(enclosingToken, s.Expr.tok);
- builder.Add(Assert(tok, etran.TrExpr(s.Expr), "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null)));
+ b.Add(Assert(tok, etran.TrExpr(s.Expr), "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null)));
} else {
foreach (var split in ss) {
if (split.IsChecked) {
var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.E.tok);
- builder.Add(AssertNS(tok, split.E, "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split
+ b.Add(AssertNS(tok, split.E, "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split
}
}
+ if (!defineFuel) {
+ b.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));
+ }
+ }
+ if (defineFuel) {
+ var ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), null, null);
+ builder.Add(ifCmd);
builder.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));
}
} else if (stmt is AssumeStmt) {
@@ -7381,7 +7473,8 @@ namespace Microsoft.Dafny { } else if (stmt is WhileStmt) {
AddComment(builder, stmt, "while statement");
- this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);
+ this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, stmt.Tok, this.fuelContext, this.reporter);
+ DefineFuelConstant(stmt.Tok, stmt.Attributes, builder, etran);
var s = (WhileStmt)stmt;
BodyTranslator bodyTr = null;
if (s.Body != null) {
@@ -7434,7 +7527,8 @@ namespace Microsoft.Dafny { } else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
- this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);
+ this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, stmt.Tok, this.fuelContext, this.reporter);
+
if (s.Kind == ForallStmt.ParBodyKind.Assign) {
AddComment(builder, stmt, "forall statement (assign)");
Contract.Assert(s.Ens.Count == 0);
@@ -7444,6 +7538,7 @@ namespace Microsoft.Dafny { var s0 = (AssignStmt)s.S0;
var definedness = new Bpl.StmtListBuilder();
var updater = new Bpl.StmtListBuilder();
+ DefineFuelConstant(stmt.Tok, stmt.Attributes, definedness, etran);
TrForallAssign(s, s0, definedness, updater, locals, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, updater.Collect(s.Tok)));
@@ -7459,6 +7554,7 @@ namespace Microsoft.Dafny { } else {
var s0 = (CallStmt)s.S0;
var definedness = new Bpl.StmtListBuilder();
+ DefineFuelConstant(stmt.Tok, stmt.Attributes, definedness, etran);
var exporter = new Bpl.StmtListBuilder();
TrForallStmtCall(s.Tok, s.BoundVars, s.Range, null, s.ForallExpressions, s0, definedness, exporter, locals, etran);
// All done, so put the two pieces together
@@ -7470,6 +7566,7 @@ namespace Microsoft.Dafny { AddComment(builder, stmt, "forall statement (proof)");
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
+ DefineFuelConstant(stmt.Tok, stmt.Attributes, definedness, etran);
TrForallProof(s, definedness, exporter, locals, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, exporter.Collect(s.Tok)));
@@ -7504,7 +7601,8 @@ namespace Microsoft.Dafny { var s = (CalcStmt)stmt;
Contract.Assert(s.Steps.Count == s.Hints.Count); // established by the resolver
AddComment(builder, stmt, "calc statement");
- this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);
+ this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, stmt.Tok, this.fuelContext, this.reporter);
+ DefineFuelConstant(stmt.Tok, stmt.Attributes, builder, etran);
CurrentIdGenerator.Push(); // put the entire calc statement within its own sub-branch
if (s.Lines.Count > 0) {
Bpl.IfCmd ifCmd = null;
@@ -10312,31 +10410,58 @@ namespace Microsoft.Dafny { // C#'s version of a type alias
internal class FuelContext : Dictionary<Function, FuelSettingPair> { }
+ internal class FuelConstant
+ {
+ public Function f;
+ public Bpl.Expr baseFuel;
+ public Bpl.Expr startFuel;
+ public Bpl.Expr startFuelAssert;
+
+ public FuelConstant(Function f, Bpl.Expr baseFuel, Bpl.Expr startFuel, Bpl.Expr startFuelAssert) {
+ this.f = f;
+ this.baseFuel = baseFuel;
+ this.startFuel = startFuel;
+ this.startFuelAssert = startFuelAssert;
+ }
+
+ public Bpl.Expr MoreFuel(Bpl.Program sink, PredefinedDecls predef, FreshIdGenerator idGen) {
+ string uniqueId = idGen.FreshId("MoreFuel_" + f.FullName);
+ Bpl.Constant moreFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, uniqueId, predef.LayerType), false);
+ sink.AddTopLevelDeclaration(moreFuel);
+ Bpl.Expr moreFuel_expr = new Bpl.IdentifierExpr(f.tok, moreFuel);
+ return moreFuel_expr;
+ }
+ }
+
internal class FuelSetting
{
public enum FuelAmount { NONE, LOW, HIGH };
public static Stack<FuelContext> SavedContexts = new Stack<FuelContext>();
- private static FuelSettingPair FuelAttrib(Function f) {
+ public static FuelSettingPair FuelAttrib(Function f, out bool found) {
Contract.Requires(f != null);
Contract.Ensures(Contract.Result<FuelSettingPair>() != null);
FuelSettingPair setting = new FuelSettingPair();
+ found = false;
if (f.Attributes != null) {
List<Expression> args = Attributes.FindExpressions(f.Attributes, "fuel");
- if (args != null && args.Count >= 2) {
- LiteralExpr literalLow = args[0] as LiteralExpr;
- LiteralExpr literalHigh = args[1] as LiteralExpr;
-
- if (literalLow != null && literalLow.Value is BigInteger && literalHigh != null && literalHigh.Value is BigInteger) {
- setting.low = (int)((BigInteger)literalLow.Value);
- setting.high = (int)((BigInteger)literalHigh.Value);
- }
- } else if (args != null && args.Count >= 1) {
- LiteralExpr literal = args[0] as LiteralExpr;
- if (literal != null && literal.Value is BigInteger) {
- setting.low = (int)((BigInteger)literal.Value);
- setting.high = setting.low + 1;
+ if (args != null) {
+ found = true;
+ if (args.Count >= 2) {
+ LiteralExpr literalLow = args[0] as LiteralExpr;
+ LiteralExpr literalHigh = args[1] as LiteralExpr;
+
+ if (literalLow != null && literalLow.Value is BigInteger && literalHigh != null && literalHigh.Value is BigInteger) {
+ setting.low = (int)((BigInteger)literalLow.Value);
+ setting.high = (int)((BigInteger)literalHigh.Value);
+ }
+ } else if (args.Count >= 1) {
+ LiteralExpr literal = args[0] as LiteralExpr;
+ if (literal != null && literal.Value is BigInteger) {
+ setting.low = (int)((BigInteger)literal.Value);
+ setting.high = setting.low + 1;
+ }
}
}
}
@@ -10369,6 +10494,12 @@ namespace Microsoft.Dafny { return translator.LayerSucc(LayerZero(), n);
}
+ public Bpl.Expr LayerN(int n, Bpl.Expr baseLayer) {
+ Contract.Requires(0 <= n);
+ Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
+ return translator.LayerSucc(baseLayer, n);
+ }
+
private Bpl.Expr ToExpr(int amount) {
if (start == null) {
return LayerN(amount);
@@ -10394,13 +10525,14 @@ namespace Microsoft.Dafny { var found = translator.fuelContext.TryGetValue(f, out setting);
if (!found) { // If the context doesn't define fuel for this function, check for a fuel attribute (which supplies a default value if none is found)
- setting = FuelAttrib(f);
+ setting = FuelAttrib(f, out found);
}
+ FuelConstant fuelConstant = Translator.FunctionFuel.Find(x => x.f == f);
if (this.amount == (int)FuelAmount.LOW) {
- return ToExpr(setting.low);
+ return GetFunctionFuel(setting.low, found, fuelConstant);
} else if (this.amount == (int)FuelAmount.HIGH) {
- return ToExpr(setting.high);
+ return GetFunctionFuel(setting.high, found, fuelConstant);
} else {
Contract.Assert(false); // Should not reach here
return null;
@@ -10408,13 +10540,30 @@ namespace Microsoft.Dafny { }
}
+ private Bpl.Expr GetFunctionFuel(int amount, bool hasFuel, FuelConstant fuelConstant) {
+ if (fuelConstant != null) {
+ if (hasFuel) {
+ // it has fuel context
+ return LayerN(amount, fuelConstant.baseFuel);
+ } else {
+ // startfuel
+ if (amount == (int)FuelAmount.LOW) {
+ return fuelConstant.startFuel;
+ } else {
+ return fuelConstant.startFuelAssert;
+ }
+ }
+ } else {
+ return ToExpr(amount);
+ }
+ }
/// <summary>
/// Finds all fuel related attributes of the form {:fuel function low [high]}
/// Adds the setting to the context _if_ the context does not already have a setting for that function.
/// In other words, it should be called in order from most to least specific contenxt scope.
/// </summary>
- private static void FindFuelAttributes(Attributes attribs, FuelContext fuelContext) {
+ public static void FindFuelAttributes(Attributes attribs, FuelContext fuelContext) {
Function f = null;
FuelSettingPair setting = null;
@@ -10495,20 +10644,35 @@ namespace Microsoft.Dafny { /// <summary>
/// Extends the given fuel context with any new fuel settings found in attribs
/// </summary>
- public static FuelContext ExpandFuelContext(Attributes attribs, FuelContext oldFuelContext) {
+ public static FuelContext ExpandFuelContext(Attributes attribs, IToken tok, FuelContext oldFuelContext, ErrorReporter reporter) {
Contract.Ensures(SavedContexts.Count == Contract.OldValue(SavedContexts.Count) + 1);
FuelContext newContext = new FuelContext();
FindFuelAttributes(attribs, newContext);
if (newContext.Count > 0) {
+ // first make sure that the fuel only increase relative to the oldContext
+ foreach (var pair in newContext) {
+ FuelSettingPair newSetting = pair.Value;
+ FuelSettingPair oldSetting;
+ var found = oldFuelContext.TryGetValue(pair.Key, out oldSetting);
+ if (!found) { // the default is {:fuel, 1, 2}
+ oldSetting = new FuelSettingPair();
+ }
+ // make sure that the fuel can only increase within a given scope
+ if (newSetting.low < oldSetting.low || newSetting.high < oldSetting.high) {
+ reporter.Error(MessageSource.Translator, tok, "Fuel can only increase within a given scope.");
+ }
+ }
+ // add oldContext to newContext if it doesn't exist already
foreach (var pair in oldFuelContext) {
if (!newContext.ContainsKey(pair.Key)) { // Local setting takes precedence over old context
- newContext.Add(pair.Key, pair.Value);
+ newContext.Add(pair.Key, pair.Value);
}
- }
+ }
} else {
newContext = oldFuelContext;
}
SavedContexts.Push(oldFuelContext);
+
return newContext;
}
diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy index abbc831e..6347e134 100644 --- a/Test/dafny0/Fuel.dfy +++ b/Test/dafny0/Fuel.dfy @@ -126,7 +126,7 @@ module TestModule4 { requires y > 5;
requires z < 0;
{
- assert {:fuel pos,0,0} pos(z) == 0; // error: Should fail due to "opaque" fuel setting
+ assert {:fuel pos,0,0} pos(z) == 0; // error: fuel can't be decreased
assert pos(-1) == 0;
if (*) {
assert pos(y) == 3 + pos(y - 3); // error: Should fail without extra fuel setting
@@ -404,7 +404,7 @@ module TestModule9 { requires y > 5;
requires z < 0;
{
- assert {:fuel abs,0,0} abs(z) == -1*z; // error: Cannot see the body of abs
+ assert {:fuel abs,0,0} abs(z) == -1*z; // error: fuel can't be decreased
assert abs(y) == y; // Normal success
assert abs(-1) == 1; // lit bypasses fuel, so this should succeed
}
diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect index 0c128941..275be237 100644 --- a/Test/dafny0/Fuel.dfy.expect +++ b/Test/dafny0/Fuel.dfy.expect @@ -1,3 +1,5 @@ +Fuel.dfy(129,8): Error: Fuel can only increase within a given scope.
+Fuel.dfy(407,8): Error: Fuel can only increase within a given scope.
Fuel.dfy(17,22): Error: assertion violation
Execution trace:
(0,0): anon0
@@ -25,14 +27,17 @@ Execution trace: Fuel.dfy(129,38): Error: assertion violation
Execution trace:
(0,0): anon0
+ (0,0): anon7_Then
Fuel.dfy(132,26): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon3_Then
+ Fuel.dfy(129,9): anon7_Else
+ (0,0): anon8_Then
Fuel.dfy(133,26): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon3_Then
+ Fuel.dfy(129,9): anon7_Else
+ (0,0): anon8_Then
Fuel.dfy(157,22): Error: assertion violation
Execution trace:
(0,0): anon0
@@ -91,6 +96,7 @@ Execution trace: Fuel.dfy(407,38): Error: assertion violation
Execution trace:
(0,0): anon0
+ (0,0): anon3_Then
Fuel.dfy(435,22): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny4/Bug93.dfy b/Test/dafny4/Bug93.dfy new file mode 100644 index 00000000..5a1dd27f --- /dev/null +++ b/Test/dafny4/Bug93.dfy @@ -0,0 +1,37 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module Fuel {
+ function FunctionA(x:int) : int
+ {
+ x + 2
+ }
+
+ function FunctionB(y:int) : int
+ {
+ FunctionA(y - 2)
+ }
+
+ method {:fuel FunctionA,0,0} MethodX(z:int)
+ {
+ assert FunctionB(z) == z; // error: Cannot see the body of FunctionA
+ }
+}
+
+module Opaque {
+ function {:opaque} FunctionA(x:int) : int
+ {
+ x + 2
+ }
+
+ function FunctionB(y:int) : int
+ {
+ FunctionA(y - 2)
+ }
+
+ method MethodX(z:int)
+ {
+ assert FunctionB(z) == z;
+ }
+}
+
diff --git a/Test/dafny4/Bug93.dfy.expect b/Test/dafny4/Bug93.dfy.expect new file mode 100644 index 00000000..d0baf877 --- /dev/null +++ b/Test/dafny4/Bug93.dfy.expect @@ -0,0 +1,8 @@ +Bug93.dfy(17,28): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Bug93.dfy(34,28): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 7 verified, 2 errors
|