diff mbox

[Ada] Fixes in handling of spark code

Message ID 20130910144431.GA13403@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Sept. 10, 2013, 2:44 p.m. UTC 
This patch corrects the analysis of pragma SPARK_Mode to handle the case where
the pragma appears without an argument.

It also corrects the analysis of aspect/pragma Global to propery process
an item that appears as a selected component and is later converted into an
expanded name.

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

2013-09-10  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Get_SPARK_Mode_Id): Handle the
	case where the pragma may appear without an argument.
	(Analyze_Global_List): Add expanded_name to the list of constructs
	that denote a single item.
	(Collect_Global_List): Add expanded_name to the list of constructs
	that denote a single item.
diff mbox

Patch

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 202450)
+++ sem_prag.adb
@@ -1576,7 +1576,10 @@ 
       begin
          --  Single global item declaration
 
-         if Nkind_In (List, N_Identifier, N_Selected_Component) then
+         if Nkind_In (List, N_Expanded_Name,
+                            N_Identifier,
+                            N_Selected_Component)
+         then
             Analyze_Global_Item (List, Global_Mode);
 
          --  Simple global list or moded global list declaration
@@ -16338,7 +16341,7 @@ 
          -- SPARK_Mode --
          ----------------
 
-         --  pragma SPARK_Mode (On | Off | Auto);
+         --  pragma SPARK_Mode [(On | Off | Auto)];
 
          when Pragma_SPARK_Mode => SPARK_Mod : declare
             procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id);
@@ -18369,7 +18372,10 @@ 
       begin
          --  Single global item declaration
 
-         if Nkind_In (List, N_Identifier, N_Selected_Component) then
+         if Nkind_In (List, N_Expanded_Name,
+                            N_Identifier,
+                            N_Selected_Component)
+         then
             Collect_Global_Item (List, Mode);
 
          --  Simple global list or moded global list declaration
@@ -18596,16 +18602,24 @@ 
    -----------------------
 
    function Get_SPARK_Mode_Id (N : Node_Id) return SPARK_Mode_Id is
+      Args : List_Id;
       Mode : Node_Id;
 
    begin
-      pragma Assert
-        (Nkind (N) = N_Pragma
-          and then Present (Pragma_Argument_Associations (N)));
+      pragma Assert (Nkind (N) = N_Pragma);
+      Args := Pragma_Argument_Associations (N);
 
-      Mode := First (Pragma_Argument_Associations (N));
+      --  Extract the mode from the argument list
 
-      return Get_SPARK_Mode_Id (Chars (Get_Pragma_Arg (Mode)));
+      if Present (Args) then
+         Mode := First (Pragma_Argument_Associations (N));
+         return Get_SPARK_Mode_Id (Chars (Get_Pragma_Arg (Mode)));
+
+      --  When SPARK_Mode appears without an argument, the default is ON
+
+      else
+         return SPARK_On;
+      end if;
    end Get_SPARK_Mode_Id;
 
    ----------------