mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
f91bb58b89
Description: - Choice was made to not add unused variables when there is no contract and no body (no pre/(x)post, and no body). - For postcondition variable result, we only check variables that are not of unit type. And, we report a warning only if the variable is not present in all the ensures. - For result variable, with several imbricated raise, it seems possible to have false positive with no location. Removing the no location case which seems unhelpful anyway
11 lines
173 B
Plaintext
11 lines
173 B
Plaintext
|
|
exception Exception int
|
|
|
|
use ref.Ref
|
|
|
|
val t : ref int
|
|
|
|
val m (_a:int) (_b:int) : unit raises { Exception }
|
|
|
|
let test () raises { Exception } = (m ( assert { true } ; 0) 0)
|