When the SPARK restriction was set, GNAT was not issuing violations on some
derived types. Now corrected.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-31 Marc Sango <[email protected]>
* restrict.adb (Check_SPARK_Restriction): Change Comes_From_Source (N)
by Comes_From_Source (Original_Node (N)) in order to treat also the
nodes which have been rewritten.
* sem_ch4.adb (Analyze_Explicit_Dereference, Analyze_Slice): Guard the
explicit dereference and slice violation in spark mode on the nodes
coming only from the source code.
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb (revision 178363)
+++ sem_ch4.adb (working copy)
@@ -1763,7 +1763,9 @@
-- Start of processing for Analyze_Explicit_Dereference
begin
- Check_SPARK_Restriction ("explicit dereference is not allowed", N);
+ if Comes_From_Source (N) then
+ Check_SPARK_Restriction ("explicit dereference is not allowed", N);
+ end if;
-- In formal verification mode, keep track of all reads and writes
-- through explicit dereferences.
@@ -4417,7 +4419,9 @@
-- Start of processing for Analyze_Slice
begin
- Check_SPARK_Restriction ("slice is not allowed", N);
+ if Comes_From_Source (N) then
+ Check_SPARK_Restriction ("slice is not allowed", N);
+ end if;
Analyze (P);
Analyze (D);
Index: restrict.adb
===================================================================
--- restrict.adb (revision 178358)
+++ restrict.adb (working copy)
@@ -117,7 +117,7 @@
Msg_Issued : Boolean;
Save_Error_Msg_Sloc : Source_Ptr;
begin
- if Force or else Comes_From_Source (N) then
+ if Force or else Comes_From_Source (Original_Node (N)) then
if Restriction_Check_Required (SPARK)
and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
@@ -145,7 +145,7 @@
begin
pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\');
- if Comes_From_Source (N) then
+ if Comes_From_Source (Original_Node (N)) then
if Restriction_Check_Required (SPARK)
and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
