diff options
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 13 | ||||
| -rw-r--r-- | Source/Dafny/Cloner.cs | 14 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 11 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 172 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 562 | ||||
| -rw-r--r-- | Test/dafny0/AssumptionVariables0.dfy.expect | 4 | ||||
| -rw-r--r-- | Test/dafny0/CallStmtTests.dfy | 34 | ||||
| -rw-r--r-- | Test/dafny0/CallStmtTests.dfy.expect | 4 | ||||
| -rw-r--r-- | Test/dafny0/DiscoverBounds.dfy.expect | 6 | ||||
| -rw-r--r-- | Test/dafny0/NonGhostQuantifiers.dfy | 7 | ||||
| -rw-r--r-- | Test/dafny0/NonGhostQuantifiers.dfy.expect | 22 | ||||
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy | 13 | ||||
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy.expect | 36 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 278 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 87 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 50 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy.expect | 14 | ||||
| -rw-r--r-- | Test/dafny4/set-compr.dfy.expect | 4 |
18 files changed, 925 insertions, 406 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index d1a3c092..4dda19fe 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -1012,6 +1012,12 @@ namespace Dafny return pred(false) || pred(true);
}
}
+ public static bool QuantChar(bool frall, System.Predicate<char> pred) {
+ for (int i = 0; i < 0x10000; i++) {
+ if (pred((char)i) != frall) { return !frall; }
+ }
+ return frall;
+ }
public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
for (BigInteger i = lo; i < hi; i++) {
if (pred(i) != frall) { return !frall; }
@@ -1051,6 +1057,13 @@ namespace Dafny yield return true;
}
}
+ public static IEnumerable<char> AllChars {
+ get {
+ for (int i = 0; i < 0x10000; i++) {
+ yield return (char)i;
+ }
+ }
+ }
public static IEnumerable<BigInteger> AllIntegers {
get {
yield return new BigInteger(0);
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index dd2eed69..032e30a0 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -550,13 +550,21 @@ namespace Microsoft.Dafny r = new ForallStmt(Tok(s.Tok), Tok(s.EndTok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
} else if (stmt is CalcStmt) {
- var s = (CalcStmt)stmt;
- r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));
+ var s = (CalcStmt)stmt;
+ // calc statements have the unusual property that the last line is duplicated. If that is the case (which
+ // we expect it to be here), we share the clone of that line as well.
+ var lineCount = s.Lines.Count;
+ var lines = new List<Expression>(lineCount);
+ for (int i = 0; i < lineCount; i++) {
+ lines.Add(i == lineCount - 1 && 2 <= lineCount && s.Lines[i] == s.Lines[i - 1] ? lines[i - 1] : CloneExpr(s.Lines[i]));
+ }
+ Contract.Assert(lines.Count == lineCount);
+ r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), lines, s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
r = new MatchStmt(Tok(s.Tok), Tok(s.EndTok), CloneExpr(s.Source),
- s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);
+ s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 477acabf..cdd968cf 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1566,6 +1566,9 @@ namespace Microsoft.Dafny { if (bound is ComprehensionExpr.BoolBoundedPool) {
Indent(ind);
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ Indent(ind);
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
Indent(ind);
@@ -1777,6 +1780,8 @@ namespace Microsoft.Dafny { Indent(ind);
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllBooleans) {{ @{1} = {0};", tmpVar, bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllChars) {{ @{1} = {0};", tmpVar, bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
if (AsNativeType(bv.Type) != null) {
@@ -2831,6 +2836,8 @@ namespace Microsoft.Dafny { // emit: Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("Dafny.Helpers.QuantBool(");
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("Dafny.Helpers.QuantChar(");
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantInt(");
@@ -2898,6 +2905,8 @@ namespace Microsoft.Dafny { var bv = e.BoundVars[i];
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
if (AsNativeType(bv.Type) != null) {
@@ -2971,6 +2980,8 @@ namespace Microsoft.Dafny { var bv = e.BoundVars[0];
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
if (AsNativeType(bv.Type) != null) {
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 2a98d5c2..b460d9b4 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -509,6 +509,27 @@ namespace Microsoft.Dafny { }
}
+ public bool HasFinitePossibleValues {
+ get {
+ if (IsBoolType || IsCharType || IsRefType) {
+ return true;
+ }
+ var st = AsSetType;
+ if (st != null && st.Arg.HasFinitePossibleValues) {
+ return true;
+ }
+ var mt = AsMapType;
+ if (mt != null && mt.Domain.HasFinitePossibleValues) {
+ return true;
+ }
+ var dt = AsDatatype;
+ if (dt != null && dt.HasFinitePossibleValues) {
+ return true;
+ }
+ return false;
+ }
+ }
+
public CollectionType AsCollectionType { get { return NormalizeExpand() as CollectionType; } }
public SetType AsSetType { get { return NormalizeExpand() as SetType; } }
public MultiSetType AsMultiSetType { get { return NormalizeExpand() as MultiSetType; } }
@@ -2377,6 +2398,48 @@ namespace Microsoft.Dafny { }
/// <summary>
+ /// Returns the non-null expressions of this declaration proper (that is, do not include the expressions of substatements).
+ /// Does not include the generated class members.
+ /// </summary>
+ public virtual IEnumerable<Expression> SubExpressions {
+ get {
+ foreach (var e in Attributes.SubExpressions(Attributes)) {
+ yield return e;
+ }
+ foreach (var e in Attributes.SubExpressions(Reads.Attributes)) {
+ yield return e;
+ }
+ foreach (var e in Reads.Expressions) {
+ yield return e.E;
+ }
+ foreach (var e in Attributes.SubExpressions(Modifies.Attributes)) {
+ yield return e;
+ }
+ foreach (var e in Modifies.Expressions) {
+ yield return e.E;
+ }
+ foreach (var e in Attributes.SubExpressions(Decreases.Attributes)) {
+ yield return e;
+ }
+ foreach (var e in Decreases.Expressions) {
+ yield return e;
+ }
+ foreach (var e in Requires) {
+ yield return e.E;
+ }
+ foreach (var e in Ensures) {
+ yield return e.E;
+ }
+ foreach (var e in YieldRequires) {
+ yield return e.E;
+ }
+ foreach (var e in YieldEnsures) {
+ yield return e.E;
+ }
+ }
+ }
+
+ /// <summary>
/// This Dafny type exists only for the purpose of giving the yield-count variable a type, so
/// that the type can be recognized during translation of Dafny into Boogie. It represents
/// an integer component in a "decreases" clause whose order is (\lambda x,y :: x GREATER y),
@@ -2475,6 +2538,11 @@ namespace Microsoft.Dafny { return EnclosingClass.FullCompileName + ".@" + CompileName;
}
}
+ public virtual IEnumerable<Expression> SubExpressions {
+ get {
+ yield break;
+ }
+ }
}
public class Field : MemberDecl {
@@ -2999,6 +3067,26 @@ namespace Microsoft.Dafny { public bool IsBuiltin;
public Function OverriddenFunction;
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ foreach (var e in Req) {
+ yield return e;
+ }
+ foreach (var e in Reads) {
+ yield return e.E;
+ }
+ foreach (var e in Ens) {
+ yield return e;
+ }
+ foreach (var e in Decreases.Expressions) {
+ yield return e;
+ }
+ if (Body != null) {
+ yield return Body;
+ }
+ }
+ }
+
public Type Type {
get {
// Note, the following returned type can contain type parameters from the function and its enclosing class
@@ -3213,6 +3301,24 @@ namespace Microsoft.Dafny { public readonly ISet<IVariable> AssignedAssumptionVariables = new HashSet<IVariable>();
public Method OverriddenMethod;
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ foreach (var e in Req) {
+ yield return e.E;
+ }
+ foreach (var e in Mod.Expressions) {
+ yield return e.E;
+ }
+ foreach (var e in Ens) {
+ yield return e.E;
+ }
+ foreach (var e in Decreases.Expressions) {
+ yield return e;
+ }
+ }
+ }
+
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(TypeArgs));
@@ -4821,18 +4927,32 @@ namespace Microsoft.Dafny { }
public override IEnumerable<Expression> SubExpressions
{
- get { // FIXME: This can return duplicates; this could confuse BottomUpVisitors that modify the AST in place
+ get {
foreach (var e in base.SubExpressions) { yield return e; }
foreach (var e in Attributes.SubExpressions(Attributes)) { yield return e; }
-
- foreach (var l in Lines) {
- yield return l;
+
+ for (int i = 0; i < Lines.Count - 1; i++) { // note, we skip the duplicated line at the end
+ yield return Lines[i];
}
- foreach (var e in Steps) {
- yield return e;
+ foreach (var calcop in AllCalcOps) {
+ var o3 = calcop as TernaryCalcOp;
+ if (o3 != null) {
+ yield return o3.Index;
+ }
+ }
+ }
+ }
+
+ IEnumerable<CalcOp> AllCalcOps {
+ get {
+ if (Op != null) {
+ yield return Op;
}
- if (Result != null) {
- yield return Result;
+ foreach (var stepop in StepOps) {
+ yield return stepop;
+ }
+ if (ResultOp != null) {
+ yield return ResultOp;
}
}
}
@@ -6637,7 +6757,7 @@ namespace Microsoft.Dafny { public readonly Expression Body;
public readonly bool Exact; // Exact==true means a regular let expression; Exact==false means an assign-such-that expression
public readonly Attributes Attributes;
- public List<ComprehensionExpr.BoundedPool> Constraint_Bounds; // initialized and filled in by resolver; null for Exact=true and for a ghost statement
+ public List<ComprehensionExpr.BoundedPool> Constraint_Bounds; // initialized and filled in by resolver; null for Exact=true and for when expression is in a ghost context
// invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count;
public List<IVariable> Constraint_MissingBounds; // filled in during resolution; remains "null" if Exact==true or if bounds can be found
// invariant Constraint_Bounds == null || Constraint_MissingBounds == null;
@@ -6790,6 +6910,22 @@ namespace Microsoft.Dafny { return 5;
}
}
+ public class CharBoundedPool : BoundedPool
+ {
+ public override int Preference() {
+ return 4;
+ }
+ }
+ public class RefBoundedPool : BoundedPool
+ {
+ public Type Type;
+ public RefBoundedPool(Type t) {
+ Type = t;
+ }
+ public override int Preference() {
+ return 2;
+ }
+ }
public class IntBoundedPool : BoundedPool
{
public readonly Expression LowerBound;
@@ -6864,6 +7000,24 @@ namespace Microsoft.Dafny { public List<BoundVar> MissingBounds; // filled in during resolution; remains "null" if bounds can be found
// invariant Bounds == null || MissingBounds == null;
+ public List<BoundVar> UncompilableBoundVars() {
+ var bvs = new List<BoundVar>();
+ if (MissingBounds != null) {
+ bvs.AddRange(MissingBounds);
+ }
+ if (Bounds != null) {
+ Contract.Assert(Bounds.Count == BoundVars.Count);
+ for (int i = 0; i < Bounds.Count; i++) {
+ var bound = Bounds[i];
+ if (bound is RefBoundedPool) {
+ // yes, this is in principle a bound, but it's not one we'd like to compile
+ bvs.Add(BoundVars[i]);
+ }
+ }
+ }
+ return bvs;
+ }
+
public ComprehensionExpr(IToken tok, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
: base(tok) {
Contract.Requires(tok != null);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d82d7d1f..ec3a69c9 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1313,16 +1313,6 @@ namespace Microsoft.Dafny }
}
- private readonly List<SetComprehension> needFiniteBoundsChecks_SetComprehension = new List<SetComprehension>();
- private readonly List<AssignSuchThatStmt> needBoundsDiscovery_AssignSuchThatStmt = new List<AssignSuchThatStmt>();
- private readonly List<LetExpr> needFiniteBoundsChecks_LetSuchThatExpr = new List<LetExpr>();
- public int NFBC_Count {
- // provided just for the purpose of conveniently writing contracts for ResolveTopLevelDecl_Meat
- get {
- return needFiniteBoundsChecks_SetComprehension.Count + needFiniteBoundsChecks_LetSuchThatExpr.Count;
- }
- }
-
static readonly List<NativeType> NativeTypes = new List<NativeType>() {
new NativeType("byte", 0, 0x100, "", true),
new NativeType("sbyte", -0x80, 0x80, "", true),
@@ -1338,13 +1328,23 @@ namespace Microsoft.Dafny Contract.Requires(declarations != null);
Contract.Requires(cce.NonNullElements(datatypeDependencies));
Contract.Requires(cce.NonNullElements(codatatypeDependencies));
- Contract.Requires(NFBC_Count == 0);
Contract.Requires(AllTypeConstraints.Count == 0);
- Contract.Ensures(NFBC_Count == 0);
Contract.Ensures(AllTypeConstraints.Count == 0);
int prevErrorCount = reporter.Count(ErrorLevel.Error);
+ // ---------------------------------- Pass 0 ----------------------------------
+ // This pass resolves names, introduces (and may solve) type constraints, and
+ // builds the module's call graph.
+ // Some bounds are discovered during this pass [is this necessary? can they be
+ // moved to pass 1 like the other bounds discovery? --KRML], namely:
+ // - forall statements
+ // - quantifier expressions
+ // - map comprehensions
+ // For 'newtype' declarations, it also checks that all types were fully
+ // determined.
+ // ----------------------------------------------------------------------------
+
// Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations
// First, resolve the newtype declarations and the constraint clauses, including filling in .ResolvedOp fields. This is needed for the
// resolution of the other declarations, because those other declarations may invoke DiscoverBounds, which looks at the .Constraint field
@@ -1403,172 +1403,80 @@ namespace Microsoft.Dafny allTypeParameters.PopMarker();
}
+ // ---------------------------------- Pass 1 ----------------------------------
+ // This pass:
+ // * checks that type inference was able to determine all types
+ // * fills in the .ResolvedOp field of binary expressions
+ // * discovers bounds for:
+ // - set comprehensions
+ // - assign-such-that statements
+ // - compilable let-such-that expressions
+ // - newtype constraints
+ // For each statement body that it successfully typed, this pass also:
+ // * computes ghost interests
+ // * determines/checks tail-recursion.
+ // ----------------------------------------------------------------------------
+
Dictionary<string, NativeType> nativeTypeMap = new Dictionary<string, NativeType>();
foreach (var nativeType in NativeTypes) {
nativeTypeMap.Add(nativeType.Name, nativeType);
}
-
if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
// Check that type inference went well everywhere; this will also fill in the .ResolvedOp field in binary expressions
foreach (TopLevelDecl d in declarations) {
if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
+ var prevErrCnt = reporter.Count(ErrorLevel.Error);
iter.Members.Iter(CheckTypeInference_Member);
+ if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+ iter.SubExpressions.Iter(e => CheckExpression(e, this, iter));
+ }
if (iter.Body != null) {
CheckTypeInference(iter.Body);
+ if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+ ComputeGhostInterest(iter.Body, false, iter);
+ CheckExpression(iter.Body, this, iter);
+ }
}
} else if (d is ClassDecl) {
var cl = (ClassDecl)d;
- cl.Members.Iter(CheckTypeInference_Member);
foreach (var member in cl.Members) {
- var m = member as Method;
- if (m != null && m.Body != null) {
- DetermineTailRecursion(m);
+ var prevErrCnt = reporter.Count(ErrorLevel.Error);
+ CheckTypeInference_Member(member);
+ if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+ if (member is Method) {
+ var m = (Method)member;
+ if (m.Body != null) {
+ ComputeGhostInterest(m.Body, m.IsGhost, m);
+ CheckExpression(m.Body, this, m);
+ DetermineTailRecursion(m);
+ }
+ } else if (member is Function) {
+ var f = (Function)member;
+ if (!f.IsGhost && f.Body != null) {
+ CheckIsNonGhost(f.Body);
+ }
+ DetermineTailRecursion(f);
+ }
+ if (prevErrCnt == reporter.Count(ErrorLevel.Error) && member is ICodeContext) {
+ member.SubExpressions.Iter(e => CheckExpression(e, this, (ICodeContext)member));
+ }
}
}
} else if (d is NewtypeDecl) {
var dd = (NewtypeDecl)d;
- bool? boolNativeType = null;
- NativeType stringNativeType = null;
- object nativeTypeAttr = true;
- bool hasNativeTypeAttr = Attributes.ContainsMatchingValue(dd.Attributes, "nativeType", ref nativeTypeAttr,
- new Attributes.MatchingValueOption[] {
- Attributes.MatchingValueOption.Empty,
- Attributes.MatchingValueOption.Bool,
- Attributes.MatchingValueOption.String },
- err => reporter.Error(MessageSource.Resolver, dd, err));
- if (hasNativeTypeAttr) {
- if (nativeTypeAttr is bool) {
- boolNativeType = (bool)nativeTypeAttr;
- } else {
- string keyString = (string)nativeTypeAttr;
- if (nativeTypeMap.ContainsKey(keyString)) {
- stringNativeType = nativeTypeMap[keyString];
- } else {
- reporter.Error(MessageSource.Resolver, dd, "Unsupported nativeType {0}", keyString);
- }
- }
- }
- if (stringNativeType != null || boolNativeType == true) {
- if (!dd.BaseType.IsNumericBased(Type.NumericPersuation.Int)) {
- reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used on integral types");
- }
- if (dd.Var == null) {
- reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used if newtype specifies a constraint");
- }
- }
if (dd.Var != null) {
Contract.Assert(dd.Constraint != null);
- CheckTypeInference(dd.Constraint);
-
- Func<Expression, BigInteger?> GetConst = null;
- GetConst = (Expression e) => {
- int m = 1;
- BinaryExpr bin = e as BinaryExpr;
- if (bin != null && bin.Op == BinaryExpr.Opcode.Sub && GetConst(bin.E0) == BigInteger.Zero) {
- m = -1;
- e = bin.E1;
- }
- LiteralExpr l = e as LiteralExpr;
- if (l != null && l.Value is BigInteger) {
- return m * (BigInteger)l.Value;
- }
- return null;
- };
- var bounds = DiscoverAllBounds_SingleVar(dd.Var, dd.Constraint);
- List<NativeType> potentialNativeTypes =
- (stringNativeType != null) ? new List<NativeType> { stringNativeType } :
- (boolNativeType == false) ? new List<NativeType>() :
- NativeTypes;
- foreach (var nt in potentialNativeTypes) {
- bool lowerOk = false;
- bool upperOk = false;
- foreach (var bound in bounds) {
- if (bound is ComprehensionExpr.IntBoundedPool) {
- var bnd = (ComprehensionExpr.IntBoundedPool)bound;
- if (bnd.LowerBound != null) {
- BigInteger? lower = GetConst(bnd.LowerBound);
- if (lower != null && nt.LowerBound <= lower) {
- lowerOk = true;
- }
- }
- if (bnd.UpperBound != null) {
- BigInteger? upper = GetConst(bnd.UpperBound);
- if (upper != null && upper <= nt.UpperBound) {
- upperOk = true;
- }
- }
- }
- }
- if (lowerOk && upperOk) {
- dd.NativeType = nt;
- break;
- }
- }
- if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) {
- reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics cannot find a compatible native type. " +
- "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'");
- }
- if (dd.NativeType != null && stringNativeType == null) {
- reporter.Info(MessageSource.Resolver, dd.tok, "{:nativeType \"" + dd.NativeType.Name + "\"}");
- }
+ CheckExpression(dd.Constraint, this, dd);
}
+ FigureOutNativeType(dd, nativeTypeMap);
}
}
}
- if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
- // At this point, it is necessary to know for each statement and expression if it is ghost or not
- foreach (var e in needFiniteBoundsChecks_SetComprehension) {
- CheckTypeInference(e.Range); // we need to resolve operators before the call to DiscoverBounds
- List<BoundVar> missingBounds;
- e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.Range, true, true, out missingBounds);
- if (missingBounds.Count != 0) {
- e.MissingBounds = missingBounds;
- if (e.Finite) {
- foreach (var bv in e.MissingBounds) {
- reporter.Error(MessageSource.Resolver, e, "a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
- }
- }
- }
- }
- foreach (AssignSuchThatStmt s in needBoundsDiscovery_AssignSuchThatStmt) {
- Contract.Assert(!s.IsGhost);
- var varLhss = new List<IVariable>();
- foreach (var lhs in s.Lhss) {
- var ide = (IdentifierExpr)lhs.Resolved; // successful resolution above implies all LHS's are IdentifierExpr's
- varLhss.Add(ide.Var);
- }
-
- List<IVariable> missingBounds;
- var bestBounds = DiscoverBestBounds_MultipleVars(varLhss, s.Expr, true, false, out missingBounds);
- if (missingBounds.Count != 0) {
- s.MissingBounds = missingBounds; // so that an error message can be produced during compilation
- } else {
- Contract.Assert(bestBounds != null);
- s.Bounds = bestBounds;
- }
- }
- foreach (var e in needFiniteBoundsChecks_LetSuchThatExpr) {
- Contract.Assert(!e.Exact); // only let-such-that expressions are ever added to the list
- Contract.Assert(e.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully
- var constraint = e.RHSs[0];
- CheckTypeInference(constraint); // we need to resolve operators before the call to DiscoverBounds
- List<IVariable> missingBounds;
- var vars = new List<IVariable>(e.BoundVars);
- var bestBounds = DiscoverBestBounds_MultipleVars(vars, constraint, true, false, out missingBounds);
- if (missingBounds.Count != 0) {
- e.Constraint_MissingBounds = missingBounds;
- foreach (var bv in e.Constraint_MissingBounds) {
- reporter.Error(MessageSource.Resolver, e, "a non-ghost let-such-that constraint must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
- }
- } else {
- e.Constraint_Bounds = bestBounds;
- }
- }
- }
- needFiniteBoundsChecks_SetComprehension.Clear();
- needFiniteBoundsChecks_LetSuchThatExpr.Clear();
+ // ---------------------------------- Pass 2 ----------------------------------
+ // This pass fills in various additional information.
+ // ----------------------------------------------------------------------------
if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
// fill in the postconditions and bodies of prefix lemmas
@@ -1894,6 +1802,93 @@ namespace Microsoft.Dafny }
}
+ private void FigureOutNativeType(NewtypeDecl dd, Dictionary<string, NativeType> nativeTypeMap) {
+ Contract.Requires(dd != null);
+ Contract.Requires(nativeTypeMap != null);
+ bool? boolNativeType = null;
+ NativeType stringNativeType = null;
+ object nativeTypeAttr = true;
+ bool hasNativeTypeAttr = Attributes.ContainsMatchingValue(dd.Attributes, "nativeType", ref nativeTypeAttr,
+ new Attributes.MatchingValueOption[] {
+ Attributes.MatchingValueOption.Empty,
+ Attributes.MatchingValueOption.Bool,
+ Attributes.MatchingValueOption.String },
+ err => reporter.Error(MessageSource.Resolver, dd, err));
+ if (hasNativeTypeAttr) {
+ if (nativeTypeAttr is bool) {
+ boolNativeType = (bool)nativeTypeAttr;
+ } else {
+ string keyString = (string)nativeTypeAttr;
+ if (nativeTypeMap.ContainsKey(keyString)) {
+ stringNativeType = nativeTypeMap[keyString];
+ } else {
+ reporter.Error(MessageSource.Resolver, dd, "Unsupported nativeType {0}", keyString);
+ }
+ }
+ }
+ if (stringNativeType != null || boolNativeType == true) {
+ if (!dd.BaseType.IsNumericBased(Type.NumericPersuation.Int)) {
+ reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used on integral types");
+ }
+ if (dd.Var == null) {
+ reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used if newtype specifies a constraint");
+ }
+ }
+ if (dd.Var != null) {
+ Func<Expression, BigInteger?> GetConst = null;
+ GetConst = (Expression e) => {
+ int m = 1;
+ BinaryExpr bin = e as BinaryExpr;
+ if (bin != null && bin.Op == BinaryExpr.Opcode.Sub && GetConst(bin.E0) == BigInteger.Zero) {
+ m = -1;
+ e = bin.E1;
+ }
+ LiteralExpr l = e as LiteralExpr;
+ if (l != null && l.Value is BigInteger) {
+ return m * (BigInteger)l.Value;
+ }
+ return null;
+ };
+ var bounds = DiscoverAllBounds_SingleVar(dd.Var, dd.Constraint);
+ List<NativeType> potentialNativeTypes =
+ (stringNativeType != null) ? new List<NativeType> { stringNativeType } :
+ (boolNativeType == false) ? new List<NativeType>() :
+ NativeTypes;
+ foreach (var nt in potentialNativeTypes) {
+ bool lowerOk = false;
+ bool upperOk = false;
+ foreach (var bound in bounds) {
+ if (bound is ComprehensionExpr.IntBoundedPool) {
+ var bnd = (ComprehensionExpr.IntBoundedPool)bound;
+ if (bnd.LowerBound != null) {
+ BigInteger? lower = GetConst(bnd.LowerBound);
+ if (lower != null && nt.LowerBound <= lower) {
+ lowerOk = true;
+ }
+ }
+ if (bnd.UpperBound != null) {
+ BigInteger? upper = GetConst(bnd.UpperBound);
+ if (upper != null && upper <= nt.UpperBound) {
+ upperOk = true;
+ }
+ }
+ }
+ }
+ if (lowerOk && upperOk) {
+ dd.NativeType = nt;
+ break;
+ }
+ }
+ if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) {
+ reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics cannot find a compatible native type. " +
+ "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'");
+ }
+ if (dd.NativeType != null && stringNativeType == null) {
+ reporter.Info(MessageSource.Resolver, dd.tok, "{:nativeType \"" + dd.NativeType.Name + "\"}");
+ }
+ }
+ }
+
/// <summary>
/// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
/// untenable. If this is immediately known not to be untenable, false is returned.
@@ -2123,16 +2118,60 @@ namespace Microsoft.Dafny } else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable"));
+ } else if (stmt is AssignSuchThatStmt) {
+ var s = (AssignSuchThatStmt)stmt;
+ if (s.AssumeToken == null) {
+ var varLhss = new List<IVariable>();
+ foreach (var lhs in s.Lhss) {
+ var ide = (IdentifierExpr)lhs.Resolved; // successful resolution implies all LHS's are IdentifierExpr's
+ varLhss.Add(ide.Var);
+ }
+ List<IVariable> missingBounds;
+ var bestBounds = DiscoverBestBounds_MultipleVars(varLhss, s.Expr, true, false, out missingBounds);
+ if (missingBounds.Count != 0) {
+ s.MissingBounds = missingBounds; // so that an error message can be produced during compilation
+ } else {
+ Contract.Assert(bestBounds != null);
+ s.Bounds = bestBounds;
+ }
+ }
+ } else if (stmt is CalcStmt) {
+ var s = (CalcStmt)stmt;
+ // The resolution of the calc statement builds up .Steps and .Result, which are of the form E0 OP E1, where
+ // E0 and E1 are expressions from .Lines. These additional expressions still need to have their .ResolvedOp
+ // fields filled in, so we visit them (but not their subexpressions) here.
+ foreach (var e in s.Steps) {
+ VisitOneExpr(e);
+ }
+ VisitOneExpr(s.Result);
}
}
protected override void VisitOneExpr(Expression expr) {
if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
- if (e != null) {
- foreach (var bv in e.BoundVars) {
- if (!IsDetermined(bv.Type.Normalize())) {
- resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly",
- bv.Name);
+ foreach (var bv in e.BoundVars) {
+ if (!IsDetermined(bv.Type.Normalize())) {
+ resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly", bv.Name);
+ }
+ }
+ if (e is SetComprehension) {
+ var sc = (SetComprehension)e;
+ if (sc.Finite) {
+ // A set must be finite. Discover bounds for the Range expression, but report an error only if the Term is not
+ // of a finite-individuals type.
+ List<BoundVar> missingBounds;
+ sc.Bounds = DiscoverBestBounds_MultipleVars(sc.BoundVars, sc.Range, true, true, out missingBounds);
+ if (missingBounds.Count != 0) {
+ sc.MissingBounds = missingBounds;
+ if (sc.Type.HasFinitePossibleValues) {
+ // This means the set is finite, regardless of if the Range is bounded. So, we don't give any error here.
+ // However, if this expression is used in a non-ghost context (which is not yet known at this stage of
+ // resolution), the resolver will generate an error about that later.
+ } else {
+ foreach (var bv in sc.MissingBounds) {
+ resolver.reporter.Error(MessageSource.Resolver, sc, "a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+ }
+ }
}
}
}
@@ -2172,6 +2211,7 @@ namespace Microsoft.Dafny var bin = expr as BinaryExpr;
if (bin != null) {
bin.ResolvedOp = ResolveOp(bin.Op, bin.E1.Type);
+
}
}
}
@@ -2250,6 +2290,58 @@ namespace Microsoft.Dafny #endregion CheckTypeInference
// ------------------------------------------------------------------------------------------------------
+ // ----- CheckExpression --------------------------------------------------------------------------------
+ // ------------------------------------------------------------------------------------------------------
+ #region CheckExpression
+ /// <summary>
+ /// This method computes ghost interests in the statement portion of StmtExpr's and
+ /// checks for hint restrictions in any CalcStmt.
+ /// </summary>
+ void CheckExpression(Expression expr, Resolver resolver, ICodeContext codeContext) {
+ Contract.Requires(expr != null);
+ Contract.Requires(resolver != null);
+ Contract.Requires(codeContext != null);
+ var v = new CheckExpression_Visitor(resolver, codeContext);
+ v.Visit(expr);
+ }
+ /// <summary>
+ /// This method computes ghost interests in the statement portion of StmtExpr's and
+ /// checks for hint restrictions in any CalcStmt.
+ /// </summary>
+ void CheckExpression(Statement stmt, Resolver resolver, ICodeContext codeContext) {
+ Contract.Requires(stmt != null);
+ Contract.Requires(resolver != null);
+ Contract.Requires(codeContext != null);
+ var v = new CheckExpression_Visitor(resolver, codeContext);
+ v.Visit(stmt);
+ }
+ class CheckExpression_Visitor : ResolverBottomUpVisitor
+ {
+ readonly ICodeContext CodeContext;
+ public CheckExpression_Visitor(Resolver resolver, ICodeContext codeContext)
+ : base(resolver) {
+ Contract.Requires(resolver != null);
+ Contract.Requires(codeContext != null);
+ CodeContext = codeContext;
+ }
+ protected override void VisitOneExpr(Expression expr) {
+ if (expr is StmtExpr) {
+ var e = (StmtExpr)expr;
+ resolver.ComputeGhostInterest(e.S, true, CodeContext);
+ }
+ }
+ protected override void VisitOneStmt(Statement stmt) {
+ if (stmt is CalcStmt) {
+ var s = (CalcStmt)stmt;
+ foreach (var h in s.Hints) {
+ resolver.CheckHintRestrictions(h, new HashSet<LocalVariable>());
+ }
+ }
+ }
+ }
+ #endregion
+
+ // ------------------------------------------------------------------------------------------------------
// ----- CheckTailRecursive -----------------------------------------------------------------------------
// ------------------------------------------------------------------------------------------------------
#region CheckTailRecursive
@@ -3009,11 +3101,11 @@ namespace Microsoft.Dafny // ----- ComputeGhostInterest ---------------------------------------------------------------------------
// ------------------------------------------------------------------------------------------------------
#region ComputeGhostInterest
- public void ComputeGhostInterest(Statement stmt, ICodeContext codeContext) {
+ public void ComputeGhostInterest(Statement stmt, bool mustBeErasable, ICodeContext codeContext) {
Contract.Requires(stmt != null);
Contract.Requires(codeContext != null);
var visitor = new GhostInterest_Visitor(codeContext, this);
- visitor.Visit(stmt, codeContext.IsGhost);
+ visitor.Visit(stmt, mustBeErasable);
}
class GhostInterest_Visitor
{
@@ -3037,12 +3129,6 @@ namespace Microsoft.Dafny Contract.Requires(msgArgs != null);
resolver.reporter.Error(MessageSource.Resolver, expr, msg, msgArgs);
}
- protected void Error(IToken tok, string msg, params object[] msgArgs) {
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
- Contract.Requires(msgArgs != null);
- resolver.reporter.Error(MessageSource.Resolver, tok, msg, msgArgs);
- }
/// <summary>
/// This method does three things:
/// 0. Reports an error if "mustBeErasable" and the statement assigns to a non-ghost field
@@ -3057,6 +3143,7 @@ namespace Microsoft.Dafny /// because break statements look at the ghost status of its enclosing statements.
/// </summary>
public void Visit(Statement stmt, bool mustBeErasable) {
+ Contract.Requires(stmt != null);
Contract.Assume(!codeContext.IsGhost || mustBeErasable); // (this is really a precondition) codeContext.IsGhost ==> mustBeErasable
if (stmt is PredicateStmt) {
@@ -3107,9 +3194,6 @@ namespace Microsoft.Dafny }
}
}
- if (!s.IsGhost) {
- resolver.needBoundsDiscovery_AssignSuchThatStmt.Add(s);
- }
} else if (stmt is UpdateStmt) {
var s = (UpdateStmt)stmt;
@@ -3124,13 +3208,6 @@ namespace Microsoft.Dafny local.IsGhost = true;
}
}
- foreach (var local in s.Locals) {
- if (Attributes.Contains(local.Attributes, "assumption")) {
- if (!local.IsGhost) {
- Error(local.Tok, "assumption variable must be ghost");
- }
- }
- }
s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Locals.All(v => v.IsGhost);
if (s.Update != null) {
Visit(s.Update, mustBeErasable);
@@ -4040,14 +4117,10 @@ namespace Microsoft.Dafny var prevErrorCount = reporter.Count(ErrorLevel.Error);
ResolveExpression(f.Body, new ResolveOpts(f, false));
SolveAllTypeConstraints();
- if (!f.IsGhost && prevErrorCount == reporter.Count(ErrorLevel.Error)) {
- CheckIsNonGhost(f.Body);
- }
Contract.Assert(f.Body.Type != null); // follows from postcondition of ResolveExpression
ConstrainTypes(f.Body.Type, f.ResultType, f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);
}
scope.PopMarker();
- DetermineTailRecursion(f);
}
/// <summary>
@@ -4187,7 +4260,7 @@ namespace Microsoft.Dafny ResolveBlockStatement(m.Body, m.IsGhost, m);
SolveAllTypeConstraints();
if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
- ComputeGhostInterest(m.Body, m);
+//KRML ComputeGhostInterest(m.Body, m);
}
}
@@ -4308,7 +4381,7 @@ namespace Microsoft.Dafny if (iter.Body != null) {
ResolveBlockStatement(iter.Body, false, iter);
if (reporter.Count(ErrorLevel.Error) == postSpecErrorCount) {
- ComputeGhostInterest(iter.Body, iter);
+ //KRML ComputeGhostInterest(iter.Body, iter);
}
}
@@ -5290,7 +5363,10 @@ namespace Microsoft.Dafny }
if (!(local.Type.IsBoolType))
{
- reporter.Error(MessageSource.Resolver, s, "assumption variable must be of type 'bool'");
+ reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable must be of type 'bool'");
+ }
+ if (!local.IsGhost) {
+ reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable must be ghost");
}
}
}
@@ -5599,7 +5675,6 @@ namespace Microsoft.Dafny loopStack = new List<Statement>();
foreach (var h in s.Hints) {
ResolveStatement(h, true, codeContext);
- CheckHintRestrictions(h);
}
labeledStatements = prevLblStmts;
loopStack = prevLoopStack;
@@ -6347,9 +6422,6 @@ namespace Microsoft.Dafny if (!isInitCall && callee is Constructor) {
reporter.Error(MessageSource.Resolver, s, "a constructor is allowed to be called only when an object is being allocated");
}
- if (specContextOnly && !callee.IsGhost) {
- reporter.Error(MessageSource.Resolver, s, "only ghost methods can be called from this context");
- }
// resolve left-hand sides
foreach (var lhs in s.Lhs) {
@@ -6633,8 +6705,9 @@ namespace Microsoft.Dafny /// Check that a statment is a valid hint for a calculation.
/// ToDo: generalize the part for compound statements to take a delegate?
/// </summary>
- public void CheckHintRestrictions(Statement stmt) {
+ public void CheckHintRestrictions(Statement stmt, ISet<LocalVariable> localsAllowedInUpdates) {
Contract.Requires(stmt != null);
+ Contract.Requires(localsAllowedInUpdates != null);
if (stmt is PredicateStmt) {
// cool
} else if (stmt is PrintStmt) {
@@ -6648,11 +6721,11 @@ namespace Microsoft.Dafny } else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
foreach (var lhs in s.Lhss) {
- CheckHintLhs(s.Tok, lhs.Resolved);
+ CheckHintLhs(s.Tok, lhs.Resolved, localsAllowedInUpdates);
}
} else if (stmt is AssignStmt) {
var s = (AssignStmt)stmt;
- CheckHintLhs(s.Tok, s.Lhs.Resolved);
+ CheckHintLhs(s.Tok, s.Lhs.Resolved, localsAllowedInUpdates);
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
if (s.Method.Mod.Expressions.Count != 0) {
@@ -6661,33 +6734,33 @@ namespace Microsoft.Dafny } else if (stmt is UpdateStmt) {
var s = (UpdateStmt)stmt;
foreach (var ss in s.ResolvedStatements) {
- CheckHintRestrictions(ss);
+ CheckHintRestrictions(ss, localsAllowedInUpdates);
}
} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
+ s.Locals.Iter(local => localsAllowedInUpdates.Add(local));
if (s.Update != null) {
- CheckHintRestrictions(s.Update);
+ CheckHintRestrictions(s.Update, localsAllowedInUpdates);
}
} else if (stmt is BlockStmt) {
var s = (BlockStmt)stmt;
- scope.PushMarker();
+ var newScopeForLocals = new HashSet<LocalVariable>(localsAllowedInUpdates);
foreach (var ss in s.Body) {
- CheckHintRestrictions(ss);
+ CheckHintRestrictions(ss, newScopeForLocals);
}
- scope.PopMarker();
} else if (stmt is IfStmt) {
var s = (IfStmt)stmt;
- CheckHintRestrictions(s.Thn);
+ CheckHintRestrictions(s.Thn, localsAllowedInUpdates);
if (s.Els != null) {
- CheckHintRestrictions(s.Els);
+ CheckHintRestrictions(s.Els, localsAllowedInUpdates);
}
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
foreach (var alt in s.Alternatives) {
foreach (var ss in alt.Body) {
- CheckHintRestrictions(ss);
+ CheckHintRestrictions(ss, localsAllowedInUpdates);
}
}
@@ -6697,14 +6770,14 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, s.Mod.Expressions[0].tok, "a while statement used inside a hint is not allowed to have a modifies clause");
}
if (s.Body != null) {
- CheckHintRestrictions(s.Body);
+ CheckHintRestrictions(s.Body, localsAllowedInUpdates);
}
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
foreach (var alt in s.Alternatives) {
foreach (var ss in alt.Body) {
- CheckHintRestrictions(ss);
+ CheckHintRestrictions(ss, localsAllowedInUpdates);
}
}
@@ -6726,14 +6799,14 @@ namespace Microsoft.Dafny } else if (stmt is CalcStmt) {
var s = (CalcStmt)stmt;
foreach (var h in s.Hints) {
- CheckHintRestrictions(h);
+ CheckHintRestrictions(h, new HashSet<LocalVariable>());
}
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
foreach (var kase in s.Cases) {
foreach (var ss in kase.Body) {
- CheckHintRestrictions(ss);
+ CheckHintRestrictions(ss, localsAllowedInUpdates);
}
}
@@ -6742,11 +6815,14 @@ namespace Microsoft.Dafny }
}
- void CheckHintLhs(IToken tok, Expression lhs) {
+ void CheckHintLhs(IToken tok, Expression lhs, ISet<LocalVariable> localsAllowedInUpdates) {
+ Contract.Requires(tok != null);
+ Contract.Requires(lhs != null);
+ Contract.Requires(localsAllowedInUpdates != null);
var idExpr = lhs as IdentifierExpr;
if (idExpr == null) {
reporter.Error(MessageSource.Resolver, tok, "a hint is not allowed to update heap locations");
- } else if (scope.ContainsDecl(idExpr.Var)) {
+ } else if (!localsAllowedInUpdates.Contains(idExpr.Var)) {
reporter.Error(MessageSource.Resolver, tok, "a hint is not allowed to update a variable declared outside the hint");
}
}
@@ -7768,9 +7844,6 @@ namespace Microsoft.Dafny ResolveExpression(rhs, opts);
ConstrainTypes(rhs.Type, Type.Bool, rhs.tok, "type of RHS of let-such-that expression must be boolean (got {0})", rhs.Type);
}
- if (!opts.DontCareAboutCompilation && !e.BoundVars.All(bv => bv.IsGhost)) {
- needFiniteBoundsChecks_LetSuchThatExpr.Add(e);
- }
}
ResolveExpression(e.Body, opts);
ResolveAttributes(e.Attributes, new ResolveOpts(opts, true));
@@ -7819,21 +7892,17 @@ namespace Microsoft.Dafny List<BoundVar> missingBounds;
e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.LogicalBody(), e is ExistsExpr, true, out missingBounds);
if (missingBounds.Count != 0) {
- // Report errors here about quantifications that depend on the allocation state.
- var mb = missingBounds;
- if (opts.codeContext is Function) {
- mb = new List<BoundVar>(); // (who cares if we allocate another array; this happens only in the case of a resolution error anyhow)
- foreach (var bv in missingBounds) {
- if (bv.Type.IsRefType) {
- reporter.Error(MessageSource.Resolver, expr, "a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{0}'", bv.Name);
- } else {
- mb.Add(bv);
- }
+ e.MissingBounds = missingBounds;
+ }
+ if (opts.codeContext is Function && e.Bounds != null) {
+ Contract.Assert(e.Bounds.Count == e.BoundVars.Count);
+ for (int i = 0; i < e.Bounds.Count; i++) {
+ var bound = e.Bounds[i] as ComprehensionExpr.RefBoundedPool;
+ if (bound != null) {
+ var bv = e.BoundVars[i];
+ reporter.Error(MessageSource.Resolver, expr, "a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{0}'", bv.Name);
}
}
- if (mb.Count != 0) {
- e.MissingBounds = mb;
- }
}
}
@@ -7855,12 +7924,6 @@ namespace Microsoft.Dafny scope.PopMarker();
expr.Type = new SetType(e.Finite, e.Term.Type);
- if (opts.DontCareAboutCompilation && (e.Term.Type.IsRefType || e.Term.Type.IsBoolType) || e.Term.Type.IsCharType) {
- // ok, term type is finite and we're in a ghost context
- } else {
- needFiniteBoundsChecks_SetComprehension.Add(e);
- }
-
} else if (expr is MapComprehension) {
var e = (MapComprehension)expr;
int prevErrorCount = reporter.Count(ErrorLevel.Error);
@@ -9329,17 +9392,47 @@ namespace Microsoft.Dafny CheckIsNonGhost(e.RHSs[0]);
}
CheckIsNonGhost(e.Body);
+
+ // fill in bounds for this to-be-compiled let-such-that expression
+ Contract.Assert(e.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully
+ var constraint = e.RHSs[0];
+ List<IVariable> missingBounds;
+ var vars = new List<IVariable>(e.BoundVars);
+ var bestBounds = DiscoverBestBounds_MultipleVars(vars, constraint, true, false, out missingBounds);
+ if (missingBounds.Count != 0) {
+ e.Constraint_MissingBounds = missingBounds;
+ foreach (var bv in e.Constraint_MissingBounds) {
+ reporter.Error(MessageSource.Resolver, e, "a non-ghost let-such-that constraint must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+ }
+ } else {
+ e.Constraint_Bounds = bestBounds;
+ }
}
return;
- } else if (expr is QuantifierExpr) {
- var e = (QuantifierExpr)expr;
- Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution
- if (e.MissingBounds != null) {
- foreach (var bv in e.MissingBounds) {
- reporter.Error(MessageSource.Resolver, expr, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+ } else if (expr is LambdaExpr) {
+ var e = expr as LambdaExpr;
+ CheckIsNonGhost(e.Body);
+ return;
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ var uncompilableBoundVars = e.UncompilableBoundVars();
+ if (uncompilableBoundVars.Count != 0) {
+ string what;
+ if (e is SetComprehension) {
+ what = "set comprehensions";
+ } else if (e is MapComprehension) {
+ what = "map comprehensions";
+ } else {
+ Contract.Assume(e is QuantifierExpr); // otherwise, unexpected ComprehensionExpr (since LambdaExpr is handled separately above)
+ Contract.Assert(((QuantifierExpr)e).SplitQuantifier == null); // No split quantifiers during resolution
+ what = "quantifiers";
+ }
+ foreach (var bv in uncompilableBoundVars) {
+ reporter.Error(MessageSource.Resolver, expr, "{0} in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for '{1}'", what, bv.Name);
}
return;
}
+
} else if (expr is MapComprehension) {
var e = (MapComprehension)expr;
if (e.MissingBounds != null && !e.Finite) {
@@ -9358,10 +9451,6 @@ namespace Microsoft.Dafny var e = (ChainingExpression)expr;
e.Operands.ForEach(CheckIsNonGhost);
return;
- } else if (expr is LambdaExpr) {
- var e = expr as LambdaExpr;
- CheckIsNonGhost(e.Body);
- return;
}
foreach (var ee in expr.SubExpressions) {
@@ -9520,8 +9609,11 @@ namespace Microsoft.Dafny // Maybe the type itself gives a bound
if (bv.Type.IsBoolType) {
- // easy
bounds.Add(new ComprehensionExpr.BoolBoundedPool());
+ } else if (bv.Type.IsCharType) {
+ bounds.Add(new ComprehensionExpr.CharBoundedPool());
+ } else if (bv.Type.IsRefType) {
+ bounds.Add(new ComprehensionExpr.RefBoundedPool(bv.Type));
} else if (bv.Type.IsIndDatatype && bv.Type.AsIndDatatype.HasFinitePossibleValues) {
bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));
} else if (bv.Type.IsNumericBased(Type.NumericPersuation.Int)) {
diff --git a/Test/dafny0/AssumptionVariables0.dfy.expect b/Test/dafny0/AssumptionVariables0.dfy.expect index 16572961..83eb8a73 100644 --- a/Test/dafny0/AssumptionVariables0.dfy.expect +++ b/Test/dafny0/AssumptionVariables0.dfy.expect @@ -1,13 +1,13 @@ AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && <boolean expression>"
-AssumptionVariables0.dfy(9,2): Error: assumption variable must be of type 'bool'
+AssumptionVariables0.dfy(9,26): Error: assumption variable must be of type 'bool'
AssumptionVariables0.dfy(15,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"
AssumptionVariables0.dfy(17,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"
AssumptionVariables0.dfy(27,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(31,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(53,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
-AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool'
+AssumptionVariables0.dfy(61,34): Error: assumption variable must be of type 'bool'
AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(78,20): Error: assumption variable must be ghost
12 resolution/type errors detected in AssumptionVariables0.dfy
diff --git a/Test/dafny0/CallStmtTests.dfy b/Test/dafny0/CallStmtTests.dfy index 67e66b34..46c466ff 100644 --- a/Test/dafny0/CallStmtTests.dfy +++ b/Test/dafny0/CallStmtTests.dfy @@ -1,23 +1,27 @@ // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-method testing1(t: int)
-{
- t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
-}
+module M0 {
+ method testing1(t: int)
+ {
+ t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
+ }
-method m() returns (r: int)
-{
- return 3;
+ method m() returns (r: int)
+ {
+ return 3;
+ }
}
-method testing2()
-{
- var v;
- v := m2(); // error: v needs to be ghost because r is.
-}
+module M1 {
+ method testing2()
+ {
+ var v;
+ v := m2(); // error: v needs to be ghost because r is.
+ }
-method m2() returns (ghost r: int)
-{
- r := 23;
+ method m2() returns (ghost r: int)
+ {
+ r := 23;
+ }
}
diff --git a/Test/dafny0/CallStmtTests.dfy.expect b/Test/dafny0/CallStmtTests.dfy.expect index 8a334754..246b89f8 100644 --- a/Test/dafny0/CallStmtTests.dfy.expect +++ b/Test/dafny0/CallStmtTests.dfy.expect @@ -1,3 +1,3 @@ -CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable
-CallStmtTests.dfy(17,10): Error: actual out-parameter 0 is required to be a ghost variable
+CallStmtTests.dfy(7,4): Error: LHS of assignment must denote a mutable variable
+CallStmtTests.dfy(20,11): Error: actual out-parameter 0 is required to be a ghost variable
2 resolution/type errors detected in CallStmtTests.dfy
diff --git a/Test/dafny0/DiscoverBounds.dfy.expect b/Test/dafny0/DiscoverBounds.dfy.expect index ee816683..34003053 100644 --- a/Test/dafny0/DiscoverBounds.dfy.expect +++ b/Test/dafny0/DiscoverBounds.dfy.expect @@ -1,4 +1,4 @@ -DiscoverBounds.dfy(36,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o''
-DiscoverBounds.dfy(39,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r'
-DiscoverBounds.dfy(40,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r''
+DiscoverBounds.dfy(36,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o''
+DiscoverBounds.dfy(39,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'r'
+DiscoverBounds.dfy(40,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'r''
3 resolution/type errors detected in DiscoverBounds.dfy
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy index bff1d65b..e522d0fc 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy +++ b/Test/dafny0/NonGhostQuantifiers.dfy @@ -181,6 +181,12 @@ module DependencyOnAllAllocatedObjects { forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
}
+ class SomeClass {
+ var f: int;
+ }
+}
+
+module DependencyOnAllAllocatedObjects_More {
method M()
{
var b := forall c: SomeClass :: c != null ==> c.f == 0; // error: non-ghost code requires bounds
@@ -192,3 +198,4 @@ module DependencyOnAllAllocatedObjects { var f: int;
}
}
+
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy.expect b/Test/dafny0/NonGhostQuantifiers.dfy.expect index 1e2fce17..6b737add 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy.expect +++ b/Test/dafny0/NonGhostQuantifiers.dfy.expect @@ -6,16 +6,16 @@ NonGhostQuantifiers.dfy(167,4): Error: a quantifier involved in a function defin NonGhostQuantifiers.dfy(171,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
NonGhostQuantifiers.dfy(176,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
NonGhostQuantifiers.dfy(181,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
-NonGhostQuantifiers.dfy(186,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'
-NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'
-NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
-NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
-NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+NonGhostQuantifiers.dfy(192,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'c'
+NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'd'
+NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'x'
NonGhostQuantifiers.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
20 resolution/type errors detected in NonGhostQuantifiers.dfy
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index 61956651..8c48487d 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -7,7 +7,6 @@ class C { ghost method Init_ModifyNothing() { }
ghost method Init_ModifyThis() modifies this;
{
- data := 6; // error: assignment to a non-ghost field
gdata := 7;
}
ghost method Init_ModifyStuff(c: C) modifies this, c; { }
@@ -120,3 +119,15 @@ method M3(c: C) c.GhostMethodWithModifies(x); // error: not allowed to call method with nonempty modifies clause
}
}
+
+module AnotherModule {
+ class C {
+ var data: int;
+ ghost var gdata: int;
+ ghost method Init_ModifyThis() modifies this;
+ {
+ data := 6; // error: assignment to a non-ghost field
+ gdata := 7;
+ }
+ }
+}
diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect index 00030994..4d25ba11 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy.expect +++ b/Test/dafny0/ParallelResolveErrors.dfy.expect @@ -1,23 +1,23 @@ -ParallelResolveErrors.dfy(10,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ParallelResolveErrors.dfy(21,4): Error: LHS of assignment must denote a mutable variable
-ParallelResolveErrors.dfy(26,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
+ParallelResolveErrors.dfy(129,11): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(20,4): Error: LHS of assignment must denote a mutable variable
+ParallelResolveErrors.dfy(25,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
+ParallelResolveErrors.dfy(42,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
ParallelResolveErrors.dfy(43,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
-ParallelResolveErrors.dfy(44,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
-ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements
+ParallelResolveErrors.dfy(55,13): Error: new allocation not supported in forall statements
+ParallelResolveErrors.dfy(60,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context
-ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context
-ParallelResolveErrors.dfy(65,22): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-ParallelResolveErrors.dfy(66,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
-ParallelResolveErrors.dfy(73,19): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(77,18): Error: return statement is not allowed inside a forall statement
-ParallelResolveErrors.dfy(84,21): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(85,20): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(86,20): Error: break label is undefined or not in scope: OutsideLoop
-ParallelResolveErrors.dfy(95,24): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scope: OutsideLoop
-ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations
-ParallelResolveErrors.dfy(115,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-ParallelResolveErrors.dfy(120,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(64,22): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(65,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
+ParallelResolveErrors.dfy(72,19): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(76,18): Error: return statement is not allowed inside a forall statement
+ParallelResolveErrors.dfy(83,21): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(84,20): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(85,20): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(94,24): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(95,24): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing forall statement is not allowed to update heap locations
+ParallelResolveErrors.dfy(114,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(119,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
22 resolution/type errors detected in ParallelResolveErrors.dfy
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 2fab6bf3..d3514b2b 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -102,7 +102,7 @@ class EE { }
// --------------- ghost tests -------------------------------------
-
+module HereAreMoreGhostTests {
datatype GhostDt =
Nil(ghost extraInfo: int) |
Cons(data: int, tail: GhostDt, ghost moreInfo: int)
@@ -154,7 +154,7 @@ class GhostTests { ensures false;
{
while (true)
- decreases *; // error: not allowed in ghost context
+//KRML-confirmed decreases *; // error: not allowed in ghost context
{
}
}
@@ -228,7 +228,7 @@ class GhostTests { if (p == 67) {
break break; // fine, since this is not a ghost context
} else if (*) {
- break break break; // error: tries to break out of more loop levels than there are
+//KRML-confirmed break break break; // error: tries to break out of more loop levels than there are
}
q := q + 1;
}
@@ -238,7 +238,7 @@ class GhostTests { p := p + 1;
}
}
-method BreakMayNotBeFineHere_Ghost(ghost t: int)
+ method BreakMayNotBeFineHere_Ghost(ghost t: int)
{
var n := 0;
ghost var k := 0;
@@ -297,7 +297,7 @@ method BreakMayNotBeFineHere_Ghost(ghost t: int) }
}
}
-
+} //HereAreMoreGhostTests
method DuplicateLabels(n: int) {
var x;
if (n < 7) {
@@ -364,17 +364,17 @@ method DatatypeDestructors(d: DTD_List) { }
}
method DatatypeDestructors_Ghost(d: DTD_List) {
- var g1 := d.g; // error: cannot use ghost member in non-ghost code
+ var g1 := d.g; // error: cannot use ghost member in non-ghost code//KRML-confirmed
}
// ------------------- print statements ---------------------------------------
-
+module GhostPrintAttempts {
method PrintOnlyNonGhosts(a: int, ghost b: int)
{
print "a: ", a, "\n";
print "b: ", b, "\n"; // error: print statement cannot take ghosts
}
-
+}
// ------------------- auto-added type arguments ------------------------------
class GenericClass<T> { var data: T; }
@@ -439,11 +439,11 @@ method TestCalc_Ghost(m: int, n: int, a: bool, b: bool) {
calc {
n + m;
- { print n + m; } // error: non-ghost statements are not allowed in hints
+ { print n + m; } // error: non-ghost statements are not allowed in hints//KRML-confirmed
m + n;
}
}
-
+module MyOwnModule {
class SideEffectChecks {
ghost var ycalc: int;
@@ -461,11 +461,11 @@ class SideEffectChecks { var x: int;
calc {
0;
- { Mod(0); } // methods with side-effects are not allowed
+ { Mod(0); } // error: methods with side-effects are not allowed
ycalc;
- { ycalc := 1; } // heap updates are not allowed
+ { ycalc := 1; } // error: heap updates are not allowed
1;
- { x := 1; } // updates to locals defined outside of the hint are not allowed
+ { x := 1; } // error: updates to locals defined outside of the hint are not allowed
x;
{
var x: int;
@@ -475,7 +475,7 @@ class SideEffectChecks { }
}
}
-
+}
// ------------------- nameless constructors ------------------------------
class YHWH {
@@ -523,13 +523,13 @@ method AssignSuchThatFromGhost() var x: int;
ghost var g: int;
- x := g; // error: ghost cannot flow into non-ghost
+ x := g; // error: ghost cannot flow into non-ghost//KRML-confirmed
x := *;
assume x == g; // this mix of ghosts and non-ghosts is cool (but, of course,
// the compiler will complain)
- x :| x == g; // error: left-side has non-ghost, so RHS must be non-ghost as well
+ x :| x == g; // error: left-side has non-ghost, so RHS must be non-ghost as well//KRML-confirmed
x :| assume x == g; // this is cool, since it's an assume (but, of course, the
// compiler will complain)
@@ -605,7 +605,7 @@ method LetSuchThat(ghost z: int, n: nat) }
method LetSuchThat_Ghost(ghost z: int, n: nat)
{
- var x := var y :| y < z; y; // error: contraint depend on ghost (z)
+ var x := var y :| y < z; y; // error: contraint depend on ghost (z)//KRML-confirmed
}
// ------------ quantified variables whose types are not inferred ----------
@@ -677,9 +677,9 @@ module GhostAllocationTests { 5;
{ var y := new G; } // error: 'new' not allowed in ghost contexts
2 + 3;
- { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context
+ { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context//KRML-confirmed
1 + 4;
- { GhostNew5(g); } // error: cannot call method with nonempty modifies
+ { GhostNew5(g); } // error: cannot call method with nonempty modifies//KRML-confirmed
-5 + 10;
}
}
@@ -735,7 +735,7 @@ module StatementsInExpressions { {
calc {
5;
- { SideEffect(); } // error: cannot call method with side effects
+ { SideEffect(); } // error: cannot call method with side effects//KRML
5;
}
}
@@ -745,7 +745,7 @@ module StatementsInExpressions { calc {
6;
{ assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method
+ { NonGhostMethod(); } // error: cannot call non-ghost method//KRML-confirmed
{ var x := 8;
while x != 0
decreases *; // error: cannot use 'decreases *' in a ghost context
@@ -759,12 +759,12 @@ module StatementsInExpressions { x := x - 1;
}
}
- { MyField := 12; } // error: cannot assign to a field
- { MyGhostField := 12; } // error: cannot assign to any field
- { SideEffect(); } // error: cannot call (ghost) method with a modifies clause
+ { MyField := 12; } // error: cannot assign to a field//KRML-confirmed
+ { MyGhostField := 12; } // error: cannot assign to any field//KRML-confirmed
+ { SideEffect(); } // error: cannot call (ghost) method with a modifies clause//KRML-confirmed
{ var x := 8;
while x != 0
- modifies this; // error: cannot use a modifies clause on a loop
+ modifies this; // error: cannot use a modifies clause on a loop//KRML-confirmed
{
x := x - 1;
}
@@ -783,7 +783,7 @@ module StatementsInExpressions { calc {
6;
{ assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method
+ { NonGhostMethod(); } // error: cannot call non-ghost method//KRML-confirmed
{ var x := 8;
while x != 0
decreases *; // error: cannot use 'decreases *' in a ghost context
@@ -791,12 +791,12 @@ module StatementsInExpressions { x := x - 1;
}
}
- { MyField := 12; } // error: cannot assign to a field
- { MyGhostField := 12; } // error: cannot assign to any field
- { M(); } // error: cannot call (ghost) method with a modifies clause
+ { MyField := 12; } // error: cannot assign to a field//KRML-confirmed
+ { MyGhostField := 12; } // error: cannot assign to any field//KRML-confirmed
+ { M(); } // error: cannot call (ghost) method with a modifies clause//KRML-confirmed
{ var x := 8;
while x != 0
- modifies this; // error: cannot use a modifies clause on a loop
+ modifies this; // error: cannot use a modifies clause on a loop//KRML-confirmed
{
x := x - 1;
}
@@ -822,7 +822,7 @@ module StatementsInExpressions { {
MyLemma();
MyGhostMethod(); // error: modifi2es state
- OrdinaryMethod(); // error: not a ghost
+ OrdinaryMethod(); // error: not a ghost//KRML-confirmed
OutParamMethod(); // error: has out-parameters
10
}
@@ -1446,3 +1446,219 @@ module SuchThat { w
}
}
+
+// ---------------------- NEW STUFF ----------------------------------------
+
+module GhostTests {
+ class G { }
+
+ method GhostNew4(n: nat)
+ {
+ var g := new G;
+ calc {
+ 5;
+ 2 + 3;
+ { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context//ADD:680
+ 1 + 4;
+ { GhostNew5(g); } // error: cannot call method with nonempty modifies//ADD:682
+ -5 + 10;
+ }
+ }
+
+ ghost method GhostNew5(g: G)
+ modifies g;
+ {
+ }
+
+ class MyClass {
+ ghost method SideEffect()
+ modifies this;
+ {
+ }
+
+ method NonGhostMethod()
+ {
+ }
+
+ ghost method M()
+ modifies this;
+ {
+ calc {
+ 5;
+ { SideEffect(); } // error: cannot call method with side effects//ADD:738
+ 5;
+ }
+ }
+ function F(): int
+ {
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method//ADD:748
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field, and especially not a non-ghost field//ADD:762
+ { MyGhostField := 12; } // error: cannot assign to any field//ADD:763
+ { SideEffect(); } // error: cannot call (ghost) method with a modifies clause//ADD:764
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop//ADD:767
+ {
+ x := x - 1;
+ }
+ }
+ 6;
+ }
+ 5
+ }
+ var MyField: int;
+ ghost var MyGhostField: int;
+ method N()
+ {
+ var y :=
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method//ADD:786
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field, and especially not a non-ghost field//ADD:794
+ { MyGhostField := 12; } // error: cannot assign to any field//ADD:795
+ { M(); } // error: cannot call (ghost) method with a modifies clause//ADD:796
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop//ADD:799
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ 6;
+ }
+ 5;
+ }
+ ghost method MyLemma()
+ ghost method MyGhostMethod()
+ modifies this;
+ method OrdinaryMethod()
+ ghost method OutParamMethod() returns (y: int)
+
+ function UseLemma(): int
+ {
+ MyLemma();
+ OrdinaryMethod(); // error: not a ghost//ADD:825
+ 10
+ }
+ }
+}
+
+module EvenMoreGhostTests {
+ ghost method NiceTry()
+ ensures false;
+ {
+ while (true)
+ decreases *; // error: not allowed in ghost context//ADD:157
+ {
+ }
+ }
+ method BreakMayNotBeFineHere()
+ {
+ var n := 0;
+ var p := 0;
+ while (true)
+ {
+ var dontKnow;
+ if (n == 112) {
+ } else if (dontKnow == 708) {
+ while * {
+ label IfNest:
+ if (p == 67) {
+ break break; // fine, since this is not a ghost context
+ } else if (*) {
+ break break break; // error: tries to break out of more loop levels than there are//ADD:231
+ }
+ }
+ }
+ }
+ }
+ ghost method Bad()
+ {
+ var x: int;
+ calc {
+ 1;
+//****** { x := 1; } // error: updates to locals defined outside of the hint are not allowed
+ x;
+ {
+ var x: int;
+ x := 1; // this is OK
+ }
+ 1;
+ }
+ }
+}
+
+module BadGhostTransfer {
+ datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List, ghost g: int)
+
+ method DatatypeDestructors_Ghost(d: DTD_List) {
+ var g1 := d.g; // error: cannot use ghost member in non-ghost code//ADD:367
+ }
+ method AssignSuchThatFromGhost()
+ {
+ var x: int;
+ ghost var g: int;
+
+ x := g; // error: ghost cannot flow into non-ghost//ADD:526
+
+ x := *;
+ assume x == g; // this mix of ghosts and non-ghosts is cool (but, of course,
+ // the compiler will complain)
+
+ x :| x == g; // error: left-side has non-ghost, so RHS must be non-ghost as well//ADD:532
+
+ x :| assume x == g; // this is cool, since it's an assume (but, of course, the
+ // compiler will complain)
+
+ x :| x == 5;
+ g :| g <= g;
+ g :| assume g < g; // the compiler will complain here, despite the LHS being
+ // ghost -- and rightly so, since an assume is used
+ }
+}
+
+module MoreGhostPrintAttempts {
+ method TestCalc_Ghost(m: int, n: int, a: bool, b: bool)
+ {
+ calc {
+ n + m;
+ { print n + m; } // error: non-ghost statements are not allowed in hints//ADD:442
+ m + n;
+ }
+ }
+}
+
+module MoreLetSuchThatExpr {
+ method LetSuchThat_Ghost(ghost z: int, n: nat)
+ {
+ var x := var y :| y < z; y; // error: contraint depend on ghost (z)//ADD:608
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 0286778b..ee2dd5f7 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -1,3 +1,21 @@ +ResolutionErrors.dfy(113,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(114,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(118,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(119,10): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(126,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(130,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(251,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(274,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(288,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(293,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
+ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(464,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(466,14): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(468,10): Error: a hint is not allowed to update a variable declared outside the hint
ResolutionErrors.dfy(558,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(563,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(577,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
@@ -13,26 +31,11 @@ ResolutionErrors.dfy(652,11): Error: the body of the enclosing forall statement ResolutionErrors.dfy(652,14): Error: new allocation not allowed in ghost context
ResolutionErrors.dfy(662,23): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(669,15): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(669,15): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(678,17): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(680,29): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(682,17): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(700,21): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(738,20): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(748,24): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(751,22): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(762,18): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(763,23): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(764,20): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(767,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(786,24): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(789,22): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(794,18): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(795,23): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(796,11): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(799,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
ResolutionErrors.dfy(824,19): Error: calls to methods with side-effects are not allowed inside a statement expression
-ResolutionErrors.dfy(825,20): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(826,20): Error: wrong number of method result arguments (got 0, expected 1)
ResolutionErrors.dfy(838,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(848,4): Error: ghost variables are allowed only in specification contexts
@@ -74,8 +77,8 @@ ResolutionErrors.dfy(1146,6): Error: RHS (of type P<int>) not assignable to LHS ResolutionErrors.dfy(1151,13): Error: arguments must have the same type (got P<int> and P<X>)
ResolutionErrors.dfy(1152,13): Error: arguments must have the same type (got P<bool> and P<X>)
ResolutionErrors.dfy(1153,13): Error: arguments must have the same type (got P<int> and P<bool>)
-ResolutionErrors.dfy(1176,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-ResolutionErrors.dfy(1178,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+ResolutionErrors.dfy(1176,38): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
+ResolutionErrors.dfy(1178,24): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
ResolutionErrors.dfy(1283,26): Error: the type of this variable is underspecified
ResolutionErrors.dfy(1284,31): Error: the type of this variable is underspecified
ResolutionErrors.dfy(1285,29): Error: the type of this variable is underspecified
@@ -106,6 +109,29 @@ ResolutionErrors.dfy(1440,11): Error: type of RHS of assign-such-that statement ResolutionErrors.dfy(1441,9): Error: type of RHS of assign-such-that statement must be boolean (got int)
ResolutionErrors.dfy(1442,13): Error: type of RHS of assign-such-that statement must be boolean (got int)
ResolutionErrors.dfy(1445,15): Error: type of RHS of let-such-that expression must be boolean (got int)
+ResolutionErrors.dfy(1488,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1510,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1511,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1512,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1515,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1497,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1510,18): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(1539,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1540,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1541,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1544,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1532,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1539,18): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(1568,20): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1461,29): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1463,17): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1579,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(1597,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(1623,16): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(1630,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1636,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+ResolutionErrors.dfy(1653,8): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(1662,26): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(488,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
@@ -113,25 +139,6 @@ ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype construc ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
-ResolutionErrors.dfy(113,9): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(114,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(118,11): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(119,10): Error: actual out-parameter 0 is required to be a ghost variable
-ResolutionErrors.dfy(126,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(130,23): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(157,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(231,12): Error: trying to break out of more loop levels than there are enclosing loops
-ResolutionErrors.dfy(251,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
-ResolutionErrors.dfy(274,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(288,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(293,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
-ResolutionErrors.dfy(464,11): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(466,14): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(468,10): Error: a hint is not allowed to update a variable declared outside the hint
ResolutionErrors.dfy(494,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
ResolutionErrors.dfy(499,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
ResolutionErrors.dfy(500,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
@@ -168,8 +175,6 @@ ResolutionErrors.dfy(345,9): Error: a constructor is allowed to be called only w ResolutionErrors.dfy(359,16): Error: arguments must have the same type (got int and DTD_List)
ResolutionErrors.dfy(360,16): Error: arguments must have the same type (got DTD_List and int)
ResolutionErrors.dfy(361,25): Error: arguments must have the same type (got bool and int)
-ResolutionErrors.dfy(367,14): Error: ghost fields are allowed only in specification contexts
-ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(400,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(412,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
ResolutionErrors.dfy(420,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
@@ -180,11 +185,7 @@ ResolutionErrors.dfy(429,10): Error: first argument to ==> must be of type bool ResolutionErrors.dfy(429,10): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(434,10): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(434,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(442,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(526,7): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(532,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost
ResolutionErrors.dfy(603,18): Error: unresolved identifier: w
-ResolutionErrors.dfy(608,24): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(714,11): Error: lemmas are not allowed to have modifies clauses
ResolutionErrors.dfy(976,9): Error: unresolved identifier: s
ResolutionErrors.dfy(987,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
@@ -198,4 +199,4 @@ ResolutionErrors.dfy(1164,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1185,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1192,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1207,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-200 resolution/type errors detected in ResolutionErrors.dfy
+201 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index b44f4d68..a9d473f6 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -39,7 +39,7 @@ datatype ReverseOrder_TheCounterpart<T> = // ---------------------
-class ArrayTests {
+module ArrayTests {
ghost method G(a: array<int>)
requires a != null && 10 <= a.Length;
modifies a;
@@ -167,31 +167,33 @@ module Expl_Module { // --------------------- more ghost tests, for assign-such-that statements
-method M()
-{
- ghost var b: bool;
- ghost var k: int, l: int;
- var m: int;
-
- k :| k < 10;
- k, m :| 0 <= k < m; // error: LHS has non-ghost and RHS has ghost
- m :| m < 10;
-
- // Because of the ghost guard, these 'if' statements are ghost contexts, so only
- // assignments to ghosts are allowed.
- if (b) {
- k :| k < 10; // should be allowed
- k, l :| 0 <= k < l; // ditto
- }
- if (b) {
- m :| m < 10; // error: not allowed in ghost context
- k, m :| 0 <= k < m; // error: not allowed in ghost context
+module MoreGhostTests {
+ method M()
+ {
+ ghost var b: bool;
+ ghost var k: int, l: int;
+ var m: int;
+
+ k :| k < 10;
+ k, m :| 0 <= k < m; // error: LHS has non-ghost and RHS has ghost
+ m :| m < 10;
+
+ // Because of the ghost guard, these 'if' statements are ghost contexts, so only
+ // assignments to ghosts are allowed.
+ if (b) {
+ k :| k < 10; // should be allowed
+ k, l :| 0 <= k < l; // ditto
+ }
+ if (b) {
+ m :| m < 10; // error: not allowed in ghost context
+ k, m :| 0 <= k < m; // error: not allowed in ghost context
+ }
}
-}
-ghost method GhostM() returns (x: int)
-{
- x :| true; // no problem (but there once was a problem with this case, where an error was generated for no reason)
+ ghost method GhostM() returns (x: int)
+ {
+ x :| true; // no problem (but there once was a problem with this case, where an error was generated for no reason)
+ }
}
// ------------------ cycles that could arise from proxy assignments ---------
diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 8206fd43..de0bfbed 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -1,6 +1,10 @@ -TypeTests.dfy(205,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(211,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(218,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
+TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+TypeTests.dfy(178,7): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+TypeTests.dfy(188,6): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(189,9): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(207,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(213,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(220,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
TypeTests.dfy(7,17): Error: type mismatch for argument 0 (function expects C, got D)
TypeTests.dfy(7,20): Error: type mismatch for argument 1 (function expects D, got C)
TypeTests.dfy(8,15): Error: type mismatch for argument 0 (function expects C, got int)
@@ -8,7 +12,6 @@ TypeTests.dfy(8,18): Error: type mismatch for argument 1 (function expects D, go TypeTests.dfy(14,16): Error: incorrect type of method in-parameter 0 (expected int, got bool)
TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 0 (expected int, got C)
TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 1 (expected C, got int)
-TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
TypeTests.dfy(56,6): Error: Duplicate local-variable name: z
TypeTests.dfy(58,6): Error: Duplicate local-variable name: x
TypeTests.dfy(61,8): Error: Duplicate local-variable name: x
@@ -56,8 +59,5 @@ TypeTests.dfy(151,13): Error: sorry, cannot instantiate type parameter with a su TypeTests.dfy(152,2): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(153,16): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(154,14): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(177,5): Error: non-ghost variable cannot be assigned a value that depends on a ghost
-TypeTests.dfy(187,4): Error: cannot assign to non-ghost variable in a ghost context
-TypeTests.dfy(188,7): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
62 resolution/type errors detected in TypeTests.dfy
diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect index b31c6ac0..615ee2bc 100644 --- a/Test/dafny4/set-compr.dfy.expect +++ b/Test/dafny4/set-compr.dfy.expect @@ -1,3 +1,3 @@ -set-compr.dfy(25,7): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-set-compr.dfy(51,13): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+set-compr.dfy(25,7): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
+set-compr.dfy(51,13): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
2 resolution/type errors detected in set-compr.dfy
|