This patch suppresses the creation of routine _Postconditions when the related
context lacks invariants or predicates and all postcindition aspect / pragmas
are disabled.
------------
-- Source --
------------
-- main.adb
procedure Main is
X : Integer := 0;
procedure P with
Post => X > 0;
procedure P is begin null; end P;
begin
P;
end Main;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnat12 -gnatdg -gnatd.V main.adb
Source recreated from tree for Main (body)
------------------------------------------
procedure main is
x : integer := 0;
procedure main__p
with post => x > 0;
pragma postcondition (check => x > 0, message =>
"failed postcondition from main.adb:5");
procedure main__p is
begin
null;
return;
end main__p;
begin
main__p;
return;
end main;
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-04-24 Hristian Kirtchev <kirtc...@adacore.com>
* sem_ch6.adb (Contains_Enabled_Pragmas): New routine.
(Process_PPCs): Generate procedure _Postconditions
only when the context has invariants or predicates or enabled
aspects/pragmas.
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 198234)
+++ sem_ch6.adb (working copy)
@@ -11196,6 +11196,10 @@
-- under the same visibility conditions as for other invariant checks,
-- the type invariant must be applied to the returned value.
+ function Contains_Enabled_Pragmas (L : List_Id) return Boolean;
+ -- Determine whether list L has at least one enabled pragma. The routine
+ -- ignores nother non-pragma elements.
+
procedure Expand_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id);
-- Given pragma Contract_Cases CCs, create the circuitry needed to
-- evaluate case guards and trigger consequence expressions. Subp_Id
@@ -11263,6 +11267,26 @@
end if;
end Check_Access_Invariants;
+ ------------------------------
+ -- Contains_Enabled_Pragmas --
+ ------------------------------
+
+ function Contains_Enabled_Pragmas (L : List_Id) return Boolean is
+ Prag : Node_Id;
+
+ begin
+ Prag := First (L);
+ while Present (Prag) loop
+ if Nkind (Prag) = N_Pragma and then Is_Ignored (Prag) then
+ return False;
+ end if;
+
+ Next (Prag);
+ end loop;
+
+ return True;
+ end Contains_Enabled_Pragmas;
+
---------------------------
-- Expand_Contract_Cases --
---------------------------
@@ -12252,8 +12276,11 @@
-- If we had any postconditions and expansion is enabled, or if the
-- subprogram has invariants, then build the _Postconditions procedure.
- if (Present (Plist) or else Invariants_Or_Predicates_Present)
- and then Expander_Active
+ if Expander_Active
+ and then
+ (Invariants_Or_Predicates_Present
+ or else
+ (Present (Plist) and then Contains_Enabled_Pragmas (Plist)))
then
if No (Plist) then
Plist := Empty_List;
