[Ada] Pragma Volatile_Function has no effect on subprogram body

This patch modifies the analysis of pragmas that appear on package specs and
and subprogram bodies. The new model of analysis allows for pragmas to appear
out of order, but they are still analyzed according to internal precedence. The
patch removes the restrictions concerning the declarations order of pragmas
Abstract_State, Initial_Condition and Initializes.

------------
-- Source --
------------

--  vol_funcs.ads

package Vol_Funcs with SPARK_Mode is
   type Int is new Natural range 0 .. 5 with Volatile;

   type Rec is record
      Comp : Natural := 0;
   end record with Volatile;

   Int_Obj : Int with Volatile;
   Rec_Obj : Rec with Volatile;

   --  Completion by subprogram body

   function Func_1_Int (Val : Int) return Boolean
     with Volatile_Function;

   function Func_1_Rec (Val : Rec) return Boolean
     with Volatile_Function;

   --  Completion by expression function

   function Func_2_Int (Val : Int) return Boolean
     with Volatile_Function;

   function Func_2_Rec (Val : Rec) return Boolean
     with Volatile_Function;

   --  Stand alone expression function (no completion required)

   function Func_3_Int (Val : Int) return Boolean is (True)
     with Volatile_Function;

   function Func_3_Rec (Val : Rec) return Boolean is (True)
     with Volatile_Function;
end Vol_Funcs;

--  vol_funcs.adb

package body Vol_Funcs with SPARK_Mode is

   --  Completion by subprogram body

   function Func_1_Int (Val : Int) return Boolean is
   begin return True; end Func_1_Int;

   function Func_1_Rec (Val : Rec) return Boolean is
   begin return True; end Func_1_Rec;

   --  Completion by expression function

   function Func_2_Int (Val : Int) return Boolean is
   begin return True; end Func_2_Int;

   function Func_2_Rec (Val : Rec) return Boolean is
   begin return True; end Func_2_Rec;

   --  Stand alone subprogram body (no initial declaration)

   function Func_4_Int (Val : Int) return Boolean
     with Volatile_Function
   is begin return True; end Func_4_Int;

   function Func_4_Rec (Val : Rec) return Boolean
     with Volatile_Function
   is begin return True; end Func_4_Rec;

   Status : Boolean;

begin
   Status := Func_1_Int (Int_Obj);                                   --  Error
   Status := Func_1_Rec (Rec_Obj);                                   --  OK
   Status := Func_2_Int (Int_Obj);                                   --  Error
   Status := Func_2_Rec (Rec_Obj);                                   --  OK
   Status := Func_3_Int (Int_Obj);                                   --  Error
   Status := Func_3_Rec (Rec_Obj);                                   --  OK
   Status := Func_4_Int (Int_Obj);                                   --  Error
   Status := Func_4_Rec (Rec_Obj);                                   --  OK
end Vol_Funcs;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c vol_funcs.adb
vol_funcs.adb:32:26: volatile object cannot act as actual in a call (SPARK RM
  7.1.3(12))
vol_funcs.adb:34:26: volatile object cannot act as actual in a call (SPARK RM
  7.1.3(12))
vol_funcs.adb:36:26: volatile object cannot act as actual in a call (SPARK RM
  7.1.3(12))
vol_funcs.adb:38:26: volatile object cannot act as actual in a call (SPARK RM
  7.1.3(12))

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

2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch13.adb (Analyze_Aspect_Specifications): The processing
	for aspects Abstract_State, Ghost, Initial_Condition, Initializes
	and Refined_State no longer have to take SPARK_Mode into account.
	(Insert_After_SPARK_Mode): Removed.
	(Insert_Pragma): Update profile and comment on usage. The routine can
	now insert a pragma after the "header" of an instance.
	* sem_prag.adb (Analyze_If_Available): New routine.
	(Analyze_Pragma): Do not reset the Analyzed flag of various
	SPARK pragmas as they use the Is_Analyzed_Pragma attribute to
	avoid reanalysis. Various pragmas now trigger the analysis
	of related pragmas that depend on or are dependent on the
	current pragma. Remove the declaration order checks related
	to pragmas Abstract_State, Initial_Condition and Initializes.
	(Analyze_Pre_Post_Condition): Analyze pragmas SPARK_Mode and
	Volatile_Function prior to analyzing the pre/postcondition.
	(Check_Declaration_Order): Removed.
	(Check_Distinct_Name): Ensure that a potentially duplicated pragma
	Test_Case is not the pragma being analyzed.
	(Is_Followed_By_Pragma): Removed.

[Ada] Pragma Volatile_Function has no effect on subprogram body

Commit Message

Patch