Merge my autoTriggers work into the master branch

This contains trigger related things under the autoTriggers flag (disabled by default), and some bug-fixes and cleanups that are already enabled.
author: Clément Pit--Claudel <clement.pitclaudel@live.com> 2015-07-17 17:25:10 -0700
committer: Clément Pit--Claudel <clement.pitclaudel@live.com> 2015-07-17 17:25:10 -0700
commit: 7c766a43a77845ed1af5a0e5367e7a21edf13a8f (patch)
tree: 21911b3d9a25d4cc74dca3f831a635929428b993 /Test/dafny0
parent: fc6ebea9b9ec614e4e014c64d9cad7940deb86fb (diff)
parent: 61a5be0930c43694d270809ed5550c74b6e59e5d (diff)
16 files changed, 817 insertions, 35 deletions
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index c8fa76c8..89b0f02a 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -100,7 +100,7 @@ method ExpliesAssociativityM(A: bool, B: bool, C: bool) {
   }
 }
 
-method ExpliesShortCircuiting(a: array<T>)
+method ExpliesShortCircuiting(a: array)
 {
   assert a == null || 0 <= a.Length;  // (W)
   assert a != null ==> 0 <= a.Length;  // (X) -- same as (W)
diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy
index b2812759..c510cfb1 100644
--- a/Test/dafny0/EqualityTypes.dfy
+++ b/Test/dafny0/EqualityTypes.dfy
@@ -241,3 +241,115 @@ module Deep {
     var m1 := map[ko := 5];  // error: bad type
   }
 }
+
+//--------------------------
+
+module UnderspecifiedTypeParameters {
+  method UP<T>()
+  function method UG<T>(): int
+  method Callee<T(==)>()
+  class TakesParam<U> { }
+  
+  method MPG()
+  {
+    var g := UG();  // error: type parameter underspecified
+    UP();  // error: type parameter underspecified
+  }
+  method M() {
+    var zs: set;  // error: type is underspecified
+    Callee<(int)>();
+    Callee<set>();  // error: type is underspecified
+    Callee<()>();
+    // The following 
+    Callee<TakesParam>();  // error: type is underspecified
+  }
+}
+
+module EqualitySupportingTypes {
+  method P<T>()
+  function method G<T>(): int
+  class AClass<V(==),Y> {
+    static function method H<W,X(==)>(): bool
+    static method Q<A,B(==)>()
+  }
+
+  method Callee<T(==)>()
+  function method FCallee<T>(): T
+
+  datatype Dt = Dt(f: int -> int)
+  codatatype Stream<T> = Cons(T, Stream)
+
+  method M<ArbitraryTypeArg>()
+  {
+    Callee<Dt>();  // error:  Dt is not an equality-supporting type
+    Callee<Stream<int>>();  // error: specified type does not support equality
+
+    // set<X> is allowed in a non-ghost context only if X is equality supporting.
+    // Ditto for multiset<X> and map<X,Y>.
+    var s3x: set<Dt>;  // error: this type not allowed in a non-ghost context
+    var is3x: iset<Dt>;  // error: this type not allowed in a non-ghost context
+    var mast: multiset<ArbitraryTypeArg>;  // error: this type not allowed in a non-ghost context
+    var qt: seq<Stream<int>>;  // allowed
+    var mp0: map<Dt,int>;  // error: this type not allowed in a non-ghost context
+    var mp1: map<int,Dt>;  // allowed
+    var imp0: imap<Dt,int>;  // error: this type not allowed in a non-ghost context
+    var imp1: imap<int,Dt>;  // allowed
+
+    var S := FCallee<set>();  // this gives s:set<?>
+    if 4 in S {              // this constrains the type further to be s:set<int>
+    }
+
+    var xy: set<set<int>>;
+    var xz: set<set<Stream<int>>>;  // error: set type argument must support equality
+    
+    Callee<set<Stream<int>>>();  // bogus: a set shouldn't ever be allowed to take a Stream as an argument (this check seems to be missing for explicit type arguments)  -- Note: language definition should be changed, because it doesn't make sense for it to talk about a type appearing in a ghost or non-ghost context. Instead, set/iset/multiset/map/imap should always be allowed to take any type argument, but these types may or may not support equality.
+    var xg := G<set<Stream<int>>>();
+    
+    var ac0: AClass<int,int>;
+    var ac1: AClass<Stream<int>,int>;  // error: type parameter 0 is required to support equality
+    var ac2: AClass<int,Stream<int>>;
+    var xd0 := ac0.H<real,real>();
+    var xd1 := ac1.H<Stream<real>,real>();  // error (remnant of the fact that the type of ac1 is not allowed)
+    var xd2 := ac2.H<real,Stream<real>>();  // error: type parameter 1 is required to support equality
+    var xe0 := ac0.H<real,real>;
+    var xe1 := ac1.H<Stream<real>,real>;  // error (remnant of the fact that the type of ac1 is not allowed)
+    var xe2 := ac2.H<real,Stream<real>>;  // error: type parameter 1 is required to support equality
+    var xh0 := AClass<int,int>.H<real,real>();
+    var xh1 := AClass<int,int>.H<Stream<real>,real>();
+    var xh2 := AClass<int,int>.H<real,Stream<real>>();  // error: type parameter 1 is required to support equality
+    var xk0 := AClass<real,real>.H<int,int>;
+    var xk1 := AClass<Stream<real>,real>.H<int,int>;  // error: class type param 0 wants an equality-supporting type
+    var xk2 := AClass<real,Stream<real>>.H<int,int>;
+    AClass<Stream<int>,int>.Q<real,real>();  // error: class type param 0 wants an equality-supporting type
+    AClass<int,Stream<int>>.Q<real,real>();
+    AClass<int,Stream<int>>.Q<Stream<real>,real>();
+    AClass<int,Stream<int>>.Q<real,Stream<real>>();  // error: method type param 1 wants an equality-supporting type
+  
+/*************************** TESTS YET TO COME
+    var ac8: AClass<real,real>;
+    var xd8 := (if 5/0 == 3 then ac0 else ac8).H<real,real>();  // error: this should be checked by the verifier
+
+    AClass<int,set<Stream<int>>>.Q<real,real>();  // error: cannot utter "set<Stream<int>>"   Or is that okay???
+    AClass<int,int>.Q<set<Stream<real>>,real>();  // error: cannot utter "set<Stream<real>>"   Or is that okay???
+    var xi0 := AClass<int,set<Stream<int>>>.H<real,real>();  // error: cannot utter "set<Stream<int>>"   Or is that okay???
+    var xi1 := AClass<int,int>.H<real,set<Stream<real>>>();  // error: cannot utter "set<Stream<real>>"   Or is that okay???
+
+    var x, t, s: seq<int -> int>, fii: int -> int;
+    if s == t {
+      x := 5;  // error: assigning to non-ghost variable in ghost context
+    }
+    if fii in s {
+      x := 4;  // error: assigning to non-ghost variable in ghost context
+    }
+    if !(fii in s) {
+      x := 3;  // error: assigning to non-ghost variable in ghost context
+    }
+
+    ghost var ghostset: set<Stream<int>> := {};  // fine, since this is ghost
+    forall u | 0 <= u < 100
+      ensures var lets: set<Stream<int>> := {}; lets == lets  // this is ghost, so the equality requirement doesn't apply
+    {
+    }
+*********************************************/
+  }
+}
diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect
index 9f277582..1c02f3a0 100644
--- a/Test/dafny0/EqualityTypes.dfy.expect
+++ b/Test/dafny0/EqualityTypes.dfy.expect
@@ -35,4 +35,26 @@ EqualityTypes.dfy(238,24): Error: set argument type must support equality (got C
 EqualityTypes.dfy(239,21): Error: multiset argument type must support equality (got Co)
 EqualityTypes.dfy(241,8): Error: map domain type must support equality (got Co)
 EqualityTypes.dfy(241,14): Error: map domain type must support equality (got Co)
-37 resolution/type errors detected in EqualityTypes.dfy
+EqualityTypes.dfy(255,13): Error: type variable 'T' in the function call to 'UG' could not be determined
+EqualityTypes.dfy(256,4): Error: type '?' to the method 'UP' is not determined
+EqualityTypes.dfy(259,8): Error: the type of this local variable is underspecified
+EqualityTypes.dfy(261,4): Error: type 'set<?>' to the method 'Callee' is not determined
+EqualityTypes.dfy(264,4): Error: type 'TakesParam<?>' to the method 'Callee' is not determined
+EqualityTypes.dfy(284,14): Error: type parameter 0 (T) passed to method Callee must support equality (got Dt)
+EqualityTypes.dfy(285,23): Error: type parameter 0 (T) passed to method Callee must support equality (got Stream<int>)
+EqualityTypes.dfy(289,8): Error: set argument type must support equality (got Dt)
+EqualityTypes.dfy(290,8): Error: iset argument type must support equality (got Dt)
+EqualityTypes.dfy(291,8): Error: multiset argument type must support equality (got ArbitraryTypeArg) (perhaps try declaring type parameter 'ArbitraryTypeArg' on line 282 as 'ArbitraryTypeArg(==)', which says it can only be instantiated with a type that supports equality)
+EqualityTypes.dfy(293,8): Error: map domain type must support equality (got Dt)
+EqualityTypes.dfy(295,8): Error: imap domain type must support equality (got Dt)
+EqualityTypes.dfy(303,8): Error: set argument type must support equality (got Stream<int>)
+EqualityTypes.dfy(309,8): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)
+EqualityTypes.dfy(312,19): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)
+EqualityTypes.dfy(313,19): Error: type parameter 1 (X) passed to function H must support equality (got Stream<real>)
+EqualityTypes.dfy(315,19): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)
+EqualityTypes.dfy(316,19): Error: type parameter 1 (X) passed to function 'H' must support equality (got Stream<real>)
+EqualityTypes.dfy(319,31): Error: type parameter 1 (X) passed to function H must support equality (got Stream<real>)
+EqualityTypes.dfy(321,41): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<real>)
+EqualityTypes.dfy(323,28): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)
+EqualityTypes.dfy(326,48): Error: type parameter 1 (B) passed to method Q must support equality (got Stream<real>)
+59 resolution/type errors detected in EqualityTypes.dfy
diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy
new file mode 100644
index 00000000..c8a1fc2f
--- /dev/null
+++ b/Test/dafny0/Fuel.dfy
@@ -0,0 +1,423 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module TestModule1 {
+    function pos(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos(x - 1)
+    }
+
+    method test(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert pos(z) == 0;
+        assert pos(-1) == 0;
+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel
+        assert pos(y) == 4 + pos(y - 4);    // Succeeds, thanks to the assume from the preceding assert
+    }
+}
+
+// Test with function-level fuel boost
+module TestModule2 {
+    function {:fuel 3} pos1(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos1(x - 1)
+    }
+
+    function {:fuel 3,5} pos2(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos2(x - 1)
+    }
+
+    function {:fuel 3,5} pos3(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos3(x - 1)
+    }
+
+    function {:opaque} {:fuel 3,5} pos4(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos3(x - 1)
+    }
+
+    method test(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert pos1(z) == 0;
+        assert pos1(-1) == 0;
+        assert pos1(y) == 3 + pos1(y - 3);
+        assert pos1(y) == 4 + pos1(y - 4);
+
+        assert pos2(z) == 0;
+        assert pos2(-1) == 0;
+        assert pos2(y) == 3 + pos2(y - 3);
+        assert pos2(y) == 4 + pos2(y - 4);
+
+        if (*) {
+            assert pos3(y) == 5 + pos3(y - 5);  // Just enough fuel to get here
+        } else {
+            assert pos3(y) == 6 + pos3(y - 6);  // error: Should fail even with a boost, since boost is too small
+        }
+
+        if (*) {
+            assert pos4(z) == 0;    // error: Fuel shouldn't overcome opaque
+        } else {
+            reveal_pos4();
+            assert pos4(y) == 5 + pos4(y - 5);  // With reveal, everything should work as above
+        }
+
+
+    }
+}
+
+
+module TestModule3 {
+    // This fuel setting is equivalent to opaque, except for literals
+    function {:fuel 0,0} pos(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos(x - 1)
+    }
+
+    method test(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert pos(z) == 0;             // error: Opaque setting hides body
+        assert pos(-1) == 0;            // Passes, since Dafny's computation mode for lits ignore fuel
+        assert pos(y) == 3 + pos(y - 3);// error: Opaque setting hides body
+    }
+}
+
+// Test fuel settings via different contexts
+module TestModule4 {
+    function pos(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos(x - 1)
+    }
+
+    // Should pass
+    method {:fuel pos,3,5} test1(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert pos(z) == 0;
+        assert pos(-1) == 0;
+        assert pos(y) == 3 + pos(y - 3);
+    }
+
+    method {:fuel pos,0,0} test2(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert pos(z) == 0;               // error: Should fail due to "opaque" fuel setting
+        assert pos(-1) == 0;
+        assert pos(y) == 3 + pos(y - 3);  // error: Should fail due to "opaque" fuel setting
+    }
+
+    method test3(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert {:fuel pos,0,0} pos(z) == 0;               // error: Should fail due to "opaque" fuel setting
+        assert pos(-1) == 0;
+        if (*) {
+            assert pos(y) == 3 + pos(y - 3);  // error: Should fail without extra fuel setting
+            assert pos(y) == 6 + pos(y - 6);  // error: Should fail even with previous assert turned into assume
+        } else {
+            assert {:fuel pos,3,5} pos(y) == 3 + pos(y - 3);  // Should succeed with extra fuel setting
+            assert pos(y) == 6 + pos(y - 6);  // Should succeed thanks to previous assert turned into assume
+        } 
+    }
+
+    method test4(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        forall t:int {:fuel pos,3} | t > 0 
+            ensures true;
+        {
+            assert pos(y) == 3 + pos(y - 3);    // Expected to pass, due to local fuel boost
+        }
+
+        if (*) {
+            calc {:fuel pos,3} {
+                pos(y);
+                3 + pos(y - 3);
+            }
+        }
+
+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel outside the forall
+    }
+}
+
+// Test fuel settings via different module contexts
+module TestModule5 {
+    // Test module level fuel settings, with nested modules
+
+    module TestModule5a {
+        module {:fuel TestModule5aiA.pos,3} TestModule5ai {
+            module TestModule5aiA {
+                function pos(x:int) : int 
+                {
+                    if x < 0 then 0
+                    else 1 + pos(x - 1)
+                }
+
+                method test(y:int, z:int) 
+                    requires y > 5;
+                    requires z < 0;
+                {
+                    assert pos(z) == 0;
+                    assert pos(-1) == 0;
+                    assert pos(y) == 3 + pos(y - 3);    // Should pass due to intermediate module's fuel setting
+                }
+            }
+
+            method test(y:int, z:int) 
+                requires y > 5;
+                requires z < 0;
+            {
+                assert TestModule5aiA.pos(z) == 0;
+                assert TestModule5aiA.pos(-1) == 0;
+                assert TestModule5aiA.pos(y) == 3 + TestModule5aiA.pos(y - 3);    // Should pass due to module level fuel
+            }
+        }
+  
+        method test(y:int, z:int) 
+            requires y > 5;
+            requires z < 0;
+        {
+            assert TestModule5ai.TestModule5aiA.pos(z) == 0;
+            assert TestModule5ai.TestModule5aiA.pos(-1) == 0;
+            assert TestModule5ai.TestModule5aiA.pos(y) == 3 + TestModule5ai.TestModule5aiA.pos(y - 3);    // error: Should fail, due to lack of fuel
+        }
+    }
+
+    module {:fuel TestModule5bi.TestModule5biA.pos,3} TestModule5b {
+        module  TestModule5bi {
+            module TestModule5biA {
+                function pos(x:int) : int 
+                {
+                    if x < 0 then 0
+                    else 1 + pos(x - 1)
+                }
+
+                method test(y:int, z:int) 
+                    requires y > 5;
+                    requires z < 0;
+                {
+                    assert pos(z) == 0;
+                    assert pos(-1) == 0;
+                    assert pos(y) == 3 + pos(y - 3);    // Should succceed due to outer module fuel setting
+                }
+            }
+        }
+    }
+}
+
+// Test fuel setting for multiple functions
+module TestModule6 {
+    function pos(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos(x - 1)
+    }
+
+    function neg(x:int) : int
+        decreases 1 - x;
+    {
+        if x > 0 then 0
+        else 1 + neg(x + 1)
+    }
+
+    method test1(y:int, z:int) 
+        requires y > 5;
+        requires z < 5;
+    {
+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel
+
+        assert neg(z) == 3 + neg(z + 3);    // error: Should fail, due to lack of fuel
+    }
+
+    method {:fuel pos,3} {:fuel neg,4} test2(y:int, z:int) 
+        requires y > 5;
+        requires z < -5;
+    {
+        assert pos(y) == 3 + pos(y - 3);    
+
+        assert neg(z) == 3 + neg(z + 3);    
+    }
+}
+
+// Test fuel settings with multiple overlapping contexts
+module TestModule7 {
+    function {:fuel 3} pos(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos(x - 1)
+    }
+
+    function {:fuel 0,0} neg(x:int) : int
+        decreases 1 - x;
+    {
+        if x > 0 then 0
+        else 1 + neg(x + 1)
+    }
+
+    method {:fuel neg,4} {:fuel pos,0,0} test1(y:int, z:int) 
+        requires y > 5;
+        requires z < -5;
+    {
+        if (*) {
+            assert pos(y) == 3 + pos(y - 3);    // error: Method fuel should override function fuel, so this should fail
+            assert neg(z) == 3 + neg(z + 3);    // Method fuel should override function fuel, so this succeeds
+        }
+
+        forall t:int {:fuel pos,3} | t > 0 
+            ensures true;
+        {
+            assert pos(y) == 3 + pos(y - 3);    // Statement fuel should override method fuel, so this should succeed
+        }
+    }
+}
+
+// Test fuel in a slightly more complicated setting
+module TestModule8 {
+
+    newtype byte = i:int | 0 <= i < 0x100
+    newtype uint64 = i:int | 0 <= i < 0x10000000000000000
+
+    datatype G = GUint64
+               | GArray(elt:G)
+               | GTuple(t:seq<G>)
+               | GByteArray
+               | GTaggedUnion(cases:seq<G>)
+
+        datatype V = VUint64(u:uint64)
+                   | VTuple(t:seq<V>)
+                   | VCase(c:uint64, val:V)
+
+        predicate {:fuel 2} ValInGrammar(val:V, grammar:G)
+        {
+            match val
+                case VUint64(_) => grammar.GUint64?
+                case VTuple(t)  => grammar.GTuple? && |t| == |grammar.t|
+                                      && forall i :: 0 <= i < |t| ==> ValInGrammar(t[i], grammar.t[i])
+                case VCase(c, val) => grammar.GTaggedUnion? && int(c) < |grammar.cases| && ValInGrammar(val, grammar.cases[c])
+        }
+
+        datatype CRequest = CRequest(client:EndPoint, seqno:uint64, request:CAppMessage) | CRequestNoOp()
+
+        type EndPoint
+        function method EndPoint_grammar() : G { GUint64 }
+        function method CRequest_grammar() : G { GTaggedUnion([ GTuple([EndPoint_grammar(), GUint64, CAppMessage_grammar()]), GUint64]) }
+
+        function method parse_EndPoint(val:V) : EndPoint
+            requires ValInGrammar(val, EndPoint_grammar());
+
+        type CAppMessage
+        function method CAppMessage_grammar() : G { GTaggedUnion([GUint64, GUint64, GUint64]) }
+        function method parse_AppMessage(val:V) : CAppMessage
+            requires ValInGrammar(val, CAppMessage_grammar());
+
+        function method {:fuel ValInGrammar,1,2} parse_Request1(val:V) : CRequest
+            requires ValInGrammar(val, CRequest_grammar());
+        {
+            if val.c == 0 then
+                var ep := parse_EndPoint(val.val.t[0]); // With default fuel, error: function precondition, destructor, index
+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]))    // error: index out of range, destructor
+            else 
+                CRequestNoOp()
+        }
+
+        function method parse_Request2(val:V) : CRequest
+            requires ValInGrammar(val, CRequest_grammar());
+        {
+            if val.c == 0 then
+                var ep := parse_EndPoint(val.val.t[0]);                      // With fuel boosted to 2 this succeeds
+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2])) // error: destructor
+            else 
+                CRequestNoOp()
+        }
+
+        function method {:fuel ValInGrammar,3} parse_Request3(val:V) : CRequest
+            requires ValInGrammar(val, CRequest_grammar());
+        {
+            if val.c == 0 then
+                var ep := parse_EndPoint(val.val.t[0]); 
+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]))    // With one more boost, everything succeeds
+            else 
+                CRequestNoOp()
+        }
+
+        // With the method, everything succeeds with one less fuel boost (i.e., 2, rather than 3, as in parse_Request3)
+        method parse_Request4(val:V) returns (req:CRequest)     
+            requires ValInGrammar(val, CRequest_grammar());
+        {
+            if val.c == 0 {
+                var ep := parse_EndPoint(val.val.t[0]);
+                req := CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]));
+            } else {
+                req := CRequestNoOp();
+            }
+        }
+}
+
+
+// Test fuel when it's applied to a non-recursive function
+module TestModule9 {
+    function abs(x:int) : int
+    {
+        if x < 0 then -1 * x else x
+    }
+
+    // All should pass.
+    method test1(y:int, z:int)
+        requires y > 5;
+        requires z < 0;
+    {
+        assert abs(z) == -1*z;
+        assert abs(y) == y;
+        assert abs(-1) == 1;
+    }
+
+    // Method-level fuel override
+    method {:fuel abs,0,0} test2(y:int, z:int)
+        requires y > 5;
+        requires z < 0;
+    {
+        assert abs(z) == -1*z;  // error: Cannot see the body of abs
+        assert abs(y) == y;     // error: Cannot see the body of abs
+        assert abs(-1) == 1;    // lit bypasses fuel, so this should succeed
+    }
+
+    // Statement-level fuel override
+    method test3(y:int, z:int)
+        requires y > 5;
+        requires z < 0;
+    {
+        assert {:fuel abs,0,0} abs(z) == -1*z;  // error: Cannot see the body of abs
+        assert abs(y) == y;     // Normal success
+        assert abs(-1) == 1;    // lit bypasses fuel, so this should succeed
+    }
+
+    // Giving more fuel to a non-recursive function won't help,
+    // but it shouldn't hurt either.
+    method {:fuel abs,5,7} test4(y:int, z:int)
+        requires y > 5;
+        requires z < 0;
+    {
+        assert abs(z) == -1*z;
+        assert abs(y) == y;
+        assert abs(-1) == 1;
+    }
+}
+
diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect
new file mode 100644
index 00000000..4c180a9c
--- /dev/null
+++ b/Test/dafny0/Fuel.dfy.expect
@@ -0,0 +1,95 @@
+Fuel.dfy(17,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(65,28): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon6_Else
+Fuel.dfy(69,28): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon6_Then
+    (0,0): anon7_Then
+Fuel.dfy(92,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(94,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(120,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(122,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(129,39): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(132,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+Fuel.dfy(133,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+Fuel.dfy(157,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon10_Else
+    (0,0): anon9
+Fuel.dfy(200,56): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(245,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(247,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(280,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Then
+Fuel.dfy(335,27): Error: possible violation of function precondition
+Fuel.dfy(324,22): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(335,50): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(335,51): Error: index out of range
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(336,39): Error: index out of range
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(336,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(346,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(397,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(398,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(407,39): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 51 verified, 24 errors
diff --git a/Test/dafny0/JustWarnings.dfy b/Test/dafny0/JustWarnings.dfy
new file mode 100644
index 00000000..86523f5b
--- /dev/null
+++ b/Test/dafny0/JustWarnings.dfy
@@ -0,0 +1,19 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /warnShadowing "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file tests the behavior where the Resolver reports some warnings
+// but no errors.  In the case of errors, resolution does not continue
+// to clone modules and resolve them, but the cloning does proceed if there
+// are only warnings.  Dafny should report only one copy of these warnings,
+// and warnings are therefore turned off when processing the clones.  This
+// test file makes sure the warnings don't appear twice.
+
+method M(x: int)
+{
+  var x := 10;  // warning: this shadows the parameter 'x'
+}
+
+class C<T> {
+  var u: T
+  method P<T>(t: T)  // warning: this shadows the type parameter 'T'
+}
diff --git a/Test/dafny0/JustWarnings.dfy.expect b/Test/dafny0/JustWarnings.dfy.expect
new file mode 100644
index 00000000..5f0e66d8
--- /dev/null
+++ b/Test/dafny0/JustWarnings.dfy.expect
@@ -0,0 +1,4 @@
+JustWarnings.dfy(18,11): Warning: Shadowed type-parameter name: T
+JustWarnings.dfy(13,6): Warning: Shadowed local-variable name: x
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index 34aba3de..dbbffd87 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -71,16 +71,17 @@ module X1 {
 }
 
 module X2 {
+  import opened X1
   class MyClass2 {
-    method Down(x1: MyClass1, x0: MyClass0) {
+    method Down(x1: MyClass1, x0: X0'.MyClass0) {
       x1.Down(x0);
     }
-    method WayDown(x0: MyClass0) {
+    method WayDown(x0: X0'.MyClass0) {
       x0.Down();
     }
     method Up() {
     }
-    method Somewhere(y: MyClassY) {
+    method Somewhere(y: MyClassY) {  // error: no such type in scope
       y.M();
     }
   }
@@ -97,8 +98,7 @@ module YY {
 class ClassG {
   method T() { }
   function method TFunc(): int { 10 }
-  method V(y: MyClassY) {  // Note, MyClassY is in scope, since we are in the _default
-                           // module, which imports everything
+  method V(y: MyClassY) {
     y.M();
   }
 }
@@ -141,10 +141,10 @@ class AClassWithSomeField {
     SomeField := SomeField + 4;
     var a := old(SomeField);  // error: old can only be used in ghost contexts
     var b := fresh(this);  // error: fresh can only be used in ghost contexts
-    var c := allocated(this);  // error: allocated can only be used in ghost contexts
+//    var c := allocated(this);  // error: allocated can only be used in ghost contexts
     if (fresh(this)) {  // this guard makes the if statement a ghost statement
       ghost var x := old(SomeField);  // this is a ghost context, so it's okay
-      ghost var y := allocated(this);  // this is a ghost context, so it's okay
+//      ghost var y := allocated(this);  // this is a ghost context, so it's okay
     }
   }
 }
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect
index 5d11f9c9..d2f0bcc8 100644
--- a/Test/dafny0/Modules0.dfy.expect
+++ b/Test/dafny0/Modules0.dfy.expect
@@ -9,13 +9,8 @@ Modules0.dfy(15,11): Error: Duplicate name of top-level declaration: WazzupB
 Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)
 Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
 Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
-Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down
-Modules0.dfy(76,13): Error: expected method call, found expression
-Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down
-Modules0.dfy(79,13): Error: expected method call, found expression
-Modules0.dfy(84,8): Error: type MyClassY does not have a member M
-Modules0.dfy(84,9): Error: expected method call, found expression
-Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
+Modules0.dfy(84,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)
+Modules0.dfy(93,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
 Modules0.dfy(226,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
 Modules0.dfy(226,8): Error: new can be applied only to reference types (got X)
 Modules0.dfy(235,13): Error: module 'B' does not declare a type 'X'
@@ -35,11 +30,5 @@ Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup
 Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon'
 Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
 Modules0.dfy(324,30): Error: member Create does not exist in class Klassy
-Modules0.dfy(102,6): Error: type MyClassY does not have a member M
-Modules0.dfy(102,7): Error: expected method call, found expression
-Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts
-Modules0.dfy(142,13): Error: old expressions are allowed only in specification and ghost contexts
-Modules0.dfy(143,13): Error: fresh expressions are allowed only in specification and ghost contexts
-Modules0.dfy(144,13): Error: unresolved identifier: allocated
-Modules0.dfy(147,21): Error: unresolved identifier: allocated
-42 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)
+31 resolution/type errors detected in Modules0.dfy
diff --git a/Test/dafny0/NestedMatch.dfy b/Test/dafny0/NestedMatch.dfy
index e6e7c489..81319b4a 100644
--- a/Test/dafny0/NestedMatch.dfy
+++ b/Test/dafny0/NestedMatch.dfy
@@ -28,7 +28,7 @@ function last<T>(xs: List<T>): T
   case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
 }
 
-method checkLast(y: T) {
+method checkLast<T>(y: T) {
   assert last(Cons(y, Nil)) == y;
   assert last(Cons(y, Cons(y, Nil))) == last(Cons(y, Nil));
 }
diff --git a/Test/dafny0/NestedPatterns.dfy b/Test/dafny0/NestedPatterns.dfy
index ef597936..d1d88b2a 100644
--- a/Test/dafny0/NestedPatterns.dfy
+++ b/Test/dafny0/NestedPatterns.dfy
@@ -69,7 +69,7 @@ method MethodG<T>(xs: List<T>) returns (xxs: List<List<T>>)
   case Cons(h, Cons(ht, tt)) => 
 }
 
-method AssertionFailure(xs: List<T>)
+method AssertionFailure(xs: List)
 {
   match xs
   case (Nil) =>  // BUG: this line causes an assertion in the Dafny implementation (what should happen is that "(Nil)" should not be allowed here)
@@ -100,7 +100,7 @@ method DuplicateIdentifierInPattern2<T>(xs: List<T>)
   case Cons(h, Cons(e, e)) =>  // BUG:  here, the duplicate identifier is detected, but the error message is shown 3 times, which is less than ideal
 }
 
-method Tuples0(xs: List<T>, ys: List<T>)
+method Tuples0(xs: List, ys: List)
 {
   match (xs, ys)
   case (Nil, Nil) =>
@@ -110,14 +110,14 @@ method Tuples0(xs: List<T>, ys: List<T>)
                                     // only the identifiers in the last constructors are
 }
 
-method Tuples1(xs: List<T>, ys: List<T>)
+method Tuples1(xs: List, ys: List)
 {
   match (xs, ys, 4)
   case (Nil, Nil) =>  // BUG: the mismatch of 3 versus 2 arguments in the previous line and this line causes Dafny to crash with an
                       // assertion failure "mc.CasePatterns.Count == e.Arguments.Count"
 }
 
-method Tuples2(xs: List<T>, ys: List<T>)
+method Tuples2(xs: List, ys: List)
 {
   match (xs, ys, ())
   case (Nil, Nil, ()) =>  // BUG: Dafny crashes with an assertion failure "e.Arguments.Count >= 1"
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 761cffa0..8c910959 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1253,14 +1253,14 @@ module SignatureCompletion {
   datatype Dt = Ctor(X -> Dt)  // error: X is not a declared type
   datatype Et<Y> = Ctor(X -> Et, Y)  // error: X is not a declared type
 
-  // For methods and functions, signatures can auto-declare type parameters
-  method My0(s: set, x: A -> B)
-  method My1(x: A -> B, s: set)
+
+  method My0<A,B>(s: set, x: A -> B)
+  method My1<A,B>(x: A -> B, s: set)
   method My2<A,B>(s: set, x: A -> B)
   method My3<A,B>(x: A -> B, s: set)
 
-  function F0(s: set, x: A -> B): int
-  function F1(x: A -> B, s: set): int
+  function F0<A,B>(s: set, x: A -> B): int
+  function F1<A,B>(x: A -> B, s: set): int
   function F2<A,B>(s: set, x: A -> B): int
   function F3<A,B>(x: A -> B, s: set): int
 }
diff --git a/Test/dafny0/Shadows.dfy b/Test/dafny0/Shadows.dfy
new file mode 100644
index 00000000..da1e74d6
--- /dev/null
+++ b/Test/dafny0/Shadows.dfy
@@ -0,0 +1,42 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /warnShadowing "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module Module0 {
+  class C<alpha> {
+    method M<beta, beta>(x: beta)  // error: duplicate type parameter
+    method P<alpha>(x: alpha)  // shadowed type parameter
+    function F<beta, beta>(x: beta): int  // error: duplicate type parameter
+    function G<alpha>(x: alpha): int  // shadowed type parameter
+
+    method Q0(x: int) returns (x: int)  // error: duplicate variable name
+  }
+}
+module Module1 {
+  class D {
+    method Q1(x: int) returns (y: int)
+    {
+      var x;  // shadowed
+      var y;  // error: duplicate
+    }
+
+    var f: int
+    method R()
+    {
+      var f;  // okay
+      var f;  // error: duplicate
+    }
+    method S()
+    {
+      var x;
+      {
+        var x;  // shadow
+      }
+    }
+    method T()
+    {
+      var x;
+      ghost var b := forall x :: x < 10;  // shadow
+      ghost var c := forall y :: forall y :: y != y + 1;  // shadow
+    }
+  }
+}
diff --git a/Test/dafny0/Shadows.dfy.expect b/Test/dafny0/Shadows.dfy.expect
new file mode 100644
index 00000000..5083ac64
--- /dev/null
+++ b/Test/dafny0/Shadows.dfy.expect
@@ -0,0 +1,12 @@
+Shadows.dfy(6,19): Error: Duplicate type-parameter name: beta
+Shadows.dfy(7,13): Warning: Shadowed type-parameter name: alpha
+Shadows.dfy(8,21): Error: Duplicate type-parameter name: beta
+Shadows.dfy(9,15): Warning: Shadowed type-parameter name: alpha
+Shadows.dfy(11,31): Error: Duplicate parameter name: x
+Shadows.dfy(18,10): Warning: Shadowed local-variable name: x
+Shadows.dfy(19,10): Error: Duplicate local-variable name: y
+Shadows.dfy(26,10): Error: Duplicate local-variable name: f
+Shadows.dfy(32,12): Warning: Shadowed local-variable name: x
+Shadows.dfy(38,28): Warning: Shadowed bound-variable name: x
+Shadows.dfy(39,40): Warning: Shadowed bound-variable name: y
+5 resolution/type errors detected in Shadows.dfy
diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy b/Test/dafny0/Trait/TraitsDecreases.dfy
index 53ce28be..8ab3672a 100644
--- a/Test/dafny0/Trait/TraitsDecreases.dfy
+++ b/Test/dafny0/Trait/TraitsDecreases.dfy
@@ -106,3 +106,49 @@ class CC extends TT {
     decreases *
   { }
 }
+
+
+// The following module contains various regression tests
+module More {
+  trait A0 {
+    predicate P() decreases 5
+  }
+  class B0 extends A0 {
+    predicate P()  // error: rank is not lower
+  }
+
+  trait A1 {
+    predicate P() decreases 5
+  }
+  class B1 extends A1 {
+    predicate P() reads this  // error: rank is not lower
+  }
+
+  trait A2 {
+    predicate P(x: int)
+  }
+  class B2 extends A2 {
+    predicate P(x: int) reads this  // error: rank is not lower
+  }
+
+  trait A3 {
+    predicate P() reads this
+  }
+  class B3 extends A3 {
+    predicate P()  // error: rank is not lower
+  }
+
+  trait A4 {
+    predicate P(x: int) decreases 5
+  }
+  class B4 extends A4 {
+    predicate P(x: int)  // error: rank is not lower
+  }
+
+  trait A5 {
+    method M(x: int) decreases 5
+  }
+  class B5 extends A5 {
+    method M(x: int)  // error: rank is not lower
+  }
+}
diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy.expect b/Test/dafny0/Trait/TraitsDecreases.dfy.expect
index 6c76f9a8..2607a0c6 100644
--- a/Test/dafny0/Trait/TraitsDecreases.dfy.expect
+++ b/Test/dafny0/Trait/TraitsDecreases.dfy.expect
@@ -1,3 +1,21 @@
+TraitsDecreases.dfy(117,15): Error: predicate's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(124,15): Error: predicate's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(131,15): Error: predicate's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(138,15): Error: predicate's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(145,15): Error: predicate's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(152,12): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
 TraitsDecreases.dfy(57,10): Error: method's decreases clause must be below or equal to that in the trait
 Execution trace:
     (0,0): anon0
@@ -14,4 +32,4 @@ TraitsDecreases.dfy(88,10): Error: method's decreases clause must be below or eq
 Execution trace:
     (0,0): anon0
 
-Dafny program verifier finished with 63 verified, 5 errors
+Dafny program verifier finished with 75 verified, 11 errors
author	Clément Pit--Claudel <clement.pitclaudel@live.com>	2015-07-17 17:25:10 -0700
committer	Clément Pit--Claudel <clement.pitclaudel@live.com>	2015-07-17 17:25:10 -0700
commit	7c766a43a77845ed1af5a0e5367e7a21edf13a8f (patch)
tree	21911b3d9a25d4cc74dca3f831a635929428b993 /Test/dafny0
parent	fc6ebea9b9ec614e4e014c64d9cad7940deb86fb (diff)
parent	61a5be0930c43694d270809ed5550c74b6e59e5d (diff)