diff mbox

[Ada] Cleanup code for the generation of the _Postconditions procedure

Message ID 20130423094046.GA28721@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet April 23, 2013, 9:40 a.m. UTC 
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  <moy@adacore.com>

	* sem_ch6.adb (Process_PPCs): Do not filter postconditions based on
	applicable policy.
diff mbox

Patch

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;