diff mbox

[Ada] Detect all derived types as violation of the SPARK restriction

Message ID 20110831091434.GA11437@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 31, 2011, 9:14 a.m. UTC 
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  <sango@adacore.com>

	* 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.
diff mbox

Patch

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))