* [Ada] Invariant checks on view conversion
@ 2015-01-07 11:15 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2015-01-07 11:15 UTC (permalink / raw)
To: gcc-patches; +Cc: Ed Schonberg
[-- Attachment #1: Type: text/plain, Size: 2150 bytes --]
This patch inplements RM 7.3.2 (12/3): an invariant check must be applied to
the result of a view conversion if the type of the expression has invariants.
THe following must execute quietly:
gnatmake -q -gnata t_package_test
t_package_test
---
with Ada.Assertions; use Ada.Assertions;
with T_Ancestor_Package;
with T_Package;
procedure T_Package_Test is
pragma Assertion_Policy (Check);
My_T_Ancestor : constant T_Ancestor_Package.T_Ancestor := (A => 3);
-- Initialise My_T with something valid otherwise may get an
-- Assertion_Error here
My_T : T_Package.T := T_Package.Init; -- Sets to (A => 1, B => 2)
begin
-- Should make invariant false
T_Ancestor_Package.T_Ancestor (My_T) := My_T_Ancestor;
raise Program_Error;
exception
when Assertion_Error => null;
end T_Package_Test;
---
package T_Ancestor_Package is
pragma Assertion_Policy (Check);
type T_Ancestor is tagged record
A : Integer;
end record;
function Init return T_Ancestor;
end T_Ancestor_Package;
---
package body T_Ancestor_Package is
pragma Assertion_Policy (Check);
function Init return T_Ancestor is
begin
return (A => 1);
end Init;
end T_Ancestor_Package;
---
with T_Ancestor_Package;
package T_Package is
pragma Assertion_Policy (Check);
type T is new T_Ancestor_Package.T_Ancestor with private
with
Type_Invariant => Increasing (T);
function Increasing (My_T : in T) return
Boolean;
function Init return T;
private
type T is new T_Ancestor_Package.T_Ancestor with record
B : Integer;
end record;
end T_Package;
---
package body T_Package is
pragma Assertion_Policy (Check);
function Increasing (My_T : in T) return Boolean is
begin
return My_T.B > My_T.A;
end Increasing;
function Init return T is
begin
return (T_Ancestor_Package.Init with B => 2);
end Init;
end T_Package;
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-01-07 Ed Schonberg <schonberg@adacore.com>
* sem_ch5.adb (Analyze_Assignment): If left-hand side is a view
conversion and type of expression has invariant, apply invariant
check on expression.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 1025 bytes --]
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb (revision 219280)
+++ sem_ch5.adb (working copy)
@@ -764,6 +764,18 @@
Set_Referenced_Modified (Lhs, Out_Param => False);
end if;
+ -- RM 7.3.2 (12/3) An assignment to a view conversion (from a type
+ -- to one of its ancestors) requires an invariant check. Apply check
+ -- only if expression comes from source, otherwise it will be applied
+ -- when value is assigned to source entity.
+
+ if Nkind (Lhs) = N_Type_Conversion
+ and then Has_Invariants (Etype (Expression (Lhs)))
+ and then Comes_From_Source (Expression (Lhs))
+ then
+ Insert_After (N, Make_Invariant_Call (Expression (Lhs)));
+ end if;
+
-- Final step. If left side is an entity, then we may be able to reset
-- the current tracked values to new safe values. We only have something
-- to do if the left side is an entity name, and expansion has not
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2015-01-07 11:15 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2015-01-07 11:15 [Ada] Invariant checks on view conversion Arnaud Charlet
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).