This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Assertion policy and postconditions


This patch fixes the handling of attribute reference 'Old in the presence
of Assertion_Policy (Checked) pragma, when a unit is compiled without the
-gnata flag.

Compiling and executing the following:

      gnatmake -q assertion_policy_test.adb
      assertion_policy_test

Must yield:
   +++++ Assertion_Policy_Test starts +++++
   Houston we have a problem: Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
   Message: failed precondition from advanced_stacks.ads:31

while if the configuration pragma in advanced_stacks.ads is set to Ignore,
the output must be:

   +++++ Assertion_Policy_Test starts +++++
   Houston we have a problem: Exception name: CONSTRAINT_ERROR
   Message: advanced_stacks.adb:13 index check failed

---
-- assertion_policy_test.adb
with Ada.Text_Io;
with Ada.Exceptions; use Ada;

with Advanced_Stacks;

procedure Assertion_Policy_Test is
   use Ada;
   use Text_Io;

   Stack_Size : constant := 10;
   Test_Stack : Advanced_Stacks.Stack (Stack_Size);
   Result : Advanced_Stacks.Element := Advanced_Stacks.Element'First;

begin

   Put_Line ("+++++ Assertion_Policy_Test starts +++++");
   Result := Advanced_Stacks.Pop (Test_Stack);
   Put_Line ("+++++ Assertion_Policy_Test ends +++++");

exception
   when Err : others =>
      Put_Line ("Houston we have a problem: " &
                                     
Exceptions.Exception_Information(Err));

end Assertion_Policy_Test;
---
-- advanced_stacks.ads
pragma Assertion_Policy (Check);

package Advanced_Stacks is

   subtype Element is Integer;

   type Vector is array (Positive range <>) of Element;

   type Stack (Max_Length : Natural) is
   record
      Length : Natural := Natural'First;
      Data : Vector (1 .. Max_Length);
   end record;

   function Not_Empty (S : Stack) return Boolean is
      (S.Length > 0 and S.Length <= S.Max_Length);

   function Not_Full (S : Stack) return Boolean is
      (S.Length < S.Max_Length);

   procedure Push (E : Element; S: in out Stack)
     with Pre => Not_Full(S),   -- Precodition
          Post =>               -- Postcondition
             (S.Length = S'Old.Length + 1) and then
             (S.Data (S.Length) = E) and then
             (for all J in 1 .. S'Old.Length =>
                 S.Data(J) = S'Old.Data(J));

   function Pop (S : in out Stack) return Element
      with Pre => Not_Empty(S), --Assertion_Error if Assertion_Policy is on
           Post => (S.Length + 1 = S'Old.Length) and then
                  (S.Data (1..S.Length) = S'Old.Data (1 .. S'Old.Length - 1));

   procedure Pop (S : in out Stack; E : out Element)
      with Pre => Not_Empty(S),
           Post => (S.Length = S'Old.Length - 1) and then
                   (S'Old.Data (S'Old.Length) = E) and then
                  (S.Data (1..S.Length) = S'Old.Data (1 .. S'Old.Length - 1));

end Advanced_Stacks;
---
-- advanced_stacks.adb
package body Advanced_Stacks is

   procedure Push (E : Element; S: in out Stack) is
   begin
      S.Length := S.Length + 1;
      S.Data(S.Length) := E;
   end Push;

   function Pop (S : in out Stack) return Element is
      Result : Element := Element'First;
   begin
      Result := S.Data(S.Length);
                --index check failed if Assertion_Policy not in effect
      S.Length := S.Length - 1;
      return Result;
   end Pop;

   procedure Pop (S : in out Stack; E : out Element) is
   begin
      E := S.Data (S.Length);
      S.Length := S.Length - 1;
   end Pop;

end Advanced_Stacks;

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-06-13  Ed Schonberg  <schonberg@adacore.com>

	* exp_attr.adb (Expand_N_Attribute_Reference, case 'Old):
	To determine whether the attribute should be expanded, examine
	whether the enclosing postcondition pragma is to be checked,
	rather than using the internal flag Assertions_Enabled.

Attachment: difs
Description: Text document


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]