blob: 86523f5b74017c7df28efb97a4aa2caa5c4adc0d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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'
}
|