Patchwork [Ada] Generation of routine _Postconditions

login
register
mail settings
Submitter Arnaud Charlet
Date April 24, 2013, 2:22 p.m.
Message ID <20130424142258.GA17249@adacore.com>
Download mbox | patch
Permalink /patch/239213/
State New
Headers show

Comments

Arnaud Charlet - April 24, 2013, 2:22 p.m.
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  <kirtchev@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.

Patch

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;