blob: da1e74d671b118252d50bc97617ed6f5b739ab08 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
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
}
}
}
|