Inconsistent content between "Verification Method" and "Notes"

[brobecke]

This was reported by Yannick in an earlier version of this document, but I suspect is still applicable.

Yannick's report:

It seems that the fields "Verification Method" and "Notes" are used inconsistently to list the verification methods for a given rule. Take for example rule EXU02 (No Unhandled Application-Defined Exceptions). Its field "Verification Method" points at GNATcheck as verification method:

 GNATcheck rule: Unhandled_Exceptions

and its field "Notes" points at SPARK as verification method:

SPARK can prove that no exception will be raised (or fail to prove it and indicate the failure).

This is the case for many rules. It would be better to always have a short description of the verification methods in the field "Verification Method" and a longer explanation in "Notes".

Also note that there is no restriction or GNATcheck rule called "Unhandled_Exceptions". But the restriction "No_Exception_Propagation" could be used here.

Vasiliy sent a small reply:

No_Exception_Propagation is uncheckable with gnatcheck though.

[gusthoff]

[...] in an earlier version of this document,

"document" => Guidelines for Safe and Secure Ada/SPARK