mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
431ed6caf3
The warning can be disabled by a debug flag. The bench was changed so as to accept examples that **should** output warning but not fail (this category did not exist, it does now) and label_scope has been switched to it.
12 lines
151 B
Plaintext
12 lines
151 B
Plaintext
|
|
module T
|
|
|
|
use ref.Ref
|
|
|
|
let f () =
|
|
label Foo in
|
|
let x = ref 0 in
|
|
assert { 42 = !x at Foo } (* variable x does not exist at Foo *)
|
|
|
|
end
|