A _Postconditions procedure is created during expansion to check postconditions
and invariants of parameters. A special case was made for Postcondition pragmas
from the subprogram body: it was checked whether they were enabled before
adding them to the list of pragmas to consider in _Postconditions. The only
benefit was potentially the absence of generation of an empty _Postconditions
procedure if all such postconditions were not enabled. We remove this special
case, as it has no valid motivation, and it complexifies the code.
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-04-23 Yannick Moy <[email protected]>
* sem_ch6.adb (Process_PPCs): Do not filter postconditions based on
applicable policy.
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 198175)
+++ sem_ch6.adb (working copy)
@@ -12174,13 +12174,10 @@
Prag := First (Declarations (N));
while Present (Prag) loop
if Nkind (Prag) = N_Pragma then
- Check_Applicable_Policy (Prag);
- -- If pragma, capture if postconditions enabled, else ignore
+ -- Capture postcondition pragmas
- if Pragma_Name (Prag) = Name_Postcondition
- and then not Is_Ignored (Prag)
- then
+ if Pragma_Name (Prag) = Name_Postcondition then
if Plist = No_List then
Plist := Empty_List;
end if;
