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 <schonb...@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.
Index: exp_attr.adb
===================================================================
--- exp_attr.adb (revision 211615)
+++ exp_attr.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -3962,13 +3962,6 @@
Temp : Entity_Id;
begin
- -- If assertions are disabled, no need to create the declaration
- -- that preserves the value.
-
- if not Assertions_Enabled then
- return;
- end if;
-
Temp := Make_Temporary (Loc, 'T', Pref);
-- Climb the parent chain looking for subprogram _Postconditions
@@ -3978,6 +3971,17 @@
exit when Nkind (Subp) = N_Subprogram_Body
and then Chars (Defining_Entity (Subp)) = Name_uPostconditions;
+ -- If assertions are disabled, no need to create the declaration
+ -- that preserves the value. The postcondition pragma in which
+ -- 'Old appears will be checked or disabled according to the
+ -- current policy in effect.
+
+ if Nkind (Subp) = N_Pragma
+ and then not Is_Checked (Subp)
+ then
+ return;
+ end if;
+
Subp := Parent (Subp);
end loop;
