From 733c87fcb27a43b9fd842a363d74e579ce35c25a Mon Sep 17 00:00:00 2001 From: leino Date: Fri, 23 Jan 2015 18:11:49 -0800 Subject: Make sure to check that subrange types are not used as type parameters --- Test/dafny0/TypeTests.dfy | 49 ++++++++++++++++++++++++++++++++++++++++ Test/dafny0/TypeTests.dfy.expect | 40 ++++++++++++++++++++++++++------ 2 files changed, 82 insertions(+), 7 deletions(-) (limited to 'Test') diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 141e48cb..01c2a0a5 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -114,6 +114,55 @@ method K() { var d: MutuallyRecursiveDataType; // error: not allowed to instantiate with 'nat' var a := new nat[100]; // error: not allowed the type array var b := new nat[100,200]; // error: not allowed the type array2 + + // constructors + var ci0 := new Expl_Class.Init(0, 0); // error: subrange not allowed here + var ci1 := new Expl_Class; // error + var ci2 := new Expl_Class.Init(0, 0); // error + + // collection types (sets are above) and array types + var m0: multiset; // error + var m1: seq; // error + var m2: map; // error + var m3: map; // error + var n: seq>; // error + var o: array; // error + var o': array2; // error + + // tuple types + var tu0: (nat); // no problem, this just means 'nat' + var tu1: (nat,int); // error + var tu2: (int,nat); // error + + // function types + var fn: nat -> int; // error + var gn: int -> nat; // error + var hn: (int,nat) -> int; // error + + // the following tests test NameSegment and ExprDotName in types: + var k: Expl_Class; // error + var k': Expl_Module.E; // error + + // the following tests test NameSegment and ExprDotName in expressions: + var e0 := Expl_M(0); // error + var e1 := Expl_F(0); // error + var ec := new Expl_Class; + ec.Init(0, 0); // error + Expl_Class.DoIt(0, 0); // error + Expl_Class.DoIt(0, 0); // error + Expl_Module.E.N(0, 0); // error + Expl_Module.E.N(0, 0); // error +} +method Expl_M(x: T) returns (y: T) +function method Expl_F(x: T): T +class Expl_Class { + method Init(t: T, u: U) + static method DoIt(t: T, u: U) +} +module Expl_Module { + class E { + static method N(t: T, u: U) + } } // --------------------- more ghost tests, for assign-such-that statements diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index e40f2c35..500b1af9 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -1,6 +1,6 @@ -TypeTests.dfy(156,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt) -TypeTests.dfy(162,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt) -TypeTests.dfy(169,6): Error: RHS (of type set) not assignable to LHS (of type ?) +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(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) @@ -30,8 +30,34 @@ TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a su TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter with a subrange type TypeTests.dfy(115,8): Error: sorry, cannot instantiate type parameter with a subrange type TypeTests.dfy(116,8): Error: sorry, cannot instantiate type parameter with a subrange type -TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification contexts -TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context -TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context +TypeTests.dfy(119,28): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(119,28): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(120,17): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(120,10): Error: new can be applied only to reference types (got Expl_Class) +TypeTests.dfy(121,17): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(124,6): Error: sorry, cannot instantiate collection type with a subrange type +TypeTests.dfy(125,6): Error: sorry, cannot instantiate collection type with a subrange type +TypeTests.dfy(126,6): Error: sorry, cannot instantiate collection type with a subrange type +TypeTests.dfy(127,6): Error: sorry, cannot instantiate collection type with a subrange type +TypeTests.dfy(128,13): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(129,9): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(130,10): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(134,11): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(135,11): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(138,14): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(139,14): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(140,20): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(143,9): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(144,22): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(147,12): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(148,12): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(150,5): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(151,13): Error: sorry, cannot instantiate type parameter with a subrange type +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,15): Error: ghost variables are allowed only in specification contexts +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 -36 resolution/type errors detected in TypeTests.dfy +62 resolution/type errors detected in TypeTests.dfy -- cgit v1.2.3