diff options
| author | Yannick Moy <moy@adacore.com> | 2022-02-10 12:36:52 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-12 12:38:39 +0000 |
| commit | cc508db0d323279dc26e8471fd9f727492367e5c (patch) | |
| tree | 153b5c9b6cd4972dead1d523df05cbc6f38b9097 /gcc/function-tests.cc | |
| parent | ce19ac123abde3d9c52d52e13a00bbbe60e08722 (diff) | |
| download | gcc-cc508db0d323279dc26e8471fd9f727492367e5c.zip gcc-cc508db0d323279dc26e8471fd9f727492367e5c.tar.gz gcc-cc508db0d323279dc26e8471fd9f727492367e5c.tar.bz2 | |
[Ada] Do not issue a warning on a postcondition of True or False
Do not issue a warning about the postcondition of a function not
mentioning its result when this postcondition is statically True or
False, as this is a specification of non-termination (for value False)
or a hint to SPARK prover for not inlining an expression function (for
value True). In any case, the warning brings no value here.
gcc/ada/
* sem_util.adb (Check_Result_And_Post_State): Exempt trivial
post.
Diffstat (limited to 'gcc/function-tests.cc')
0 files changed, 0 insertions, 0 deletions