From 7ee036cae0cc6a2d48786f18908f26de37136236 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 1 Apr 2013 14:28:37 -0700 Subject: Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, where more type information is known Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement. Fixed numerous places where some recursive checks did not reach. --- Test/dafny0/Answer | 10 ++++++---- Test/dafny0/Basics.dfy | 1 - Test/dafny0/Maps.dfy | 4 ++-- Test/dafny0/ResolutionErrors.dfy | 16 ++++++++++++++++ 4 files changed, 24 insertions(+), 7 deletions(-) (limited to 'Test/dafny0') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0ca8c4f8..d2ddc057 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -357,6 +357,8 @@ ResolutionErrors.dfy(606,10): Error: ghost variables are allowed only in specifi ResolutionErrors.dfy(615,17): Error: 'new' is not allowed in ghost contexts ResolutionErrors.dfy(617,20): Error: only ghost methods can be called from this context ResolutionErrors.dfy(619,8): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(637,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type. +ResolutionErrors.dfy(637,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type. ResolutionErrors.dfy(427,2): Error: More than one default constructor ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts @@ -429,7 +431,7 @@ ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only i ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts ResolutionErrors.dfy(544,18): Error: unresolved identifier: w -89 resolution/type errors detected in ResolutionErrors.dfy +91 resolution/type errors detected in ResolutionErrors.dfy -------------------- ParseErrors.dfy -------------------- ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator @@ -703,7 +705,7 @@ Basics.dfy(110,16): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon10_Then -Basics.dfy(129,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have the same value +Basics.dfy(129,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value Execution trace: (0,0): anon0 (0,0): anon10_Then @@ -712,7 +714,7 @@ Execution trace: (0,0): anon6 (0,0): anon12_Then (0,0): anon9 -Basics.dfy(143,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value +Basics.dfy(143,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value Execution trace: (0,0): anon0 Basics.dfy(155,19): Error: assertion violation @@ -743,7 +745,7 @@ Execution trace: (0,0): anon13_Then (0,0): anon8 (0,0): anon14_Then -Basics.dfy(236,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value +Basics.dfy(235,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value Execution trace: (0,0): anon0 diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index ccd55fa3..b451cdf1 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -207,7 +207,6 @@ method m() { var i: int, j: int; i, j := 3, 6; - i, i := 3, 3; } method swap(a: array, i: nat, j: nat) diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy index 1c245952..b23a3750 100644 --- a/Test/dafny0/Maps.dfy +++ b/Test/dafny0/Maps.dfy @@ -103,13 +103,13 @@ method m7() } method m8() { - var a := map[]; + var a: map := map[]; assert forall i :: i !in a; // check emptiness var i,n := 0, 100; while(i < n) invariant 0 <= i <= n; invariant forall i | i in a :: a[i] == i * i; - invariant forall k :: 0 <= k < i <==> k in a; + invariant forall k :: 0 <= k < i <==> k in a; { a := a[i := i * i]; i := i + 1; diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 696a583f..60314836 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -626,3 +626,19 @@ module GhostAllocationTests { { } } + +// ------------------------- underspecified types ------------------------------ + +module UnderspecifiedTypes { + method M(S: set) { + var n, p, T0 :| 12 <= n && n in T0 && 10 <= p && p in T0 && T0 <= S && p % 2 != n % 2; + var T1 :| 12 in T1 && T1 <= S; + var T2 :| T2 <= S && 12 in T2; + var T3 :| 120 in T3; // error: underspecified type + var T3'0: set :| 120 in T3'0; + var T3'1: multiset :| 120 in T3'1; + var T3'2: map :| 120 in T3'2; + var T3'3: seq :| 120 in T3'3; + var T4 :| T4 <= S; + } +} -- cgit v1.2.3