This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Use of renamings of function results in SPARK annotations


This patch changes the expansion of object renamings in SPARK to reuse the
entity associated with the renaming when the name denotes a function call.
The patch also modifies a routine used to extract the entity of references
to abstract states and whole objects to handle renamings of function results.
Together, both these changes allow for function result renamings in SPARK
annotations.

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

--  pack.ads

package Pack with SPARK_Mode is
   type Lim_Rec is limited record
      Data : Integer;
   end record;

   function Get_Integer return Integer;
   function Get_Lim_Rec return Lim_Rec;
   function Get_String  return String;
end Pack;

--  pack.adb

package body Pack with SPARK_Mode is
   function Get_Integer return Integer is
   begin
      return 123;
   end Get_Integer;

   function Get_Lim_Rec return Lim_Rec is
   begin
      return Result : Lim_Rec;
   end Get_Lim_Rec;

   function Get_String return String is
   begin
      return "456";
   end Get_String;

   package Nested
     with Initializes => (Int_Ren, Lim_Ren, Str_Ren)
   is
      Int_Ren : Integer renames Get_Integer;
      Lim_Ren : Lim_Rec renames Get_Lim_Rec;
      Str_Ren : String  renames Get_String;

      procedure Proc
        with Global  => (Int_Ren, Lim_Ren, Str_Ren),
             Depends => (null => (Int_Ren, Lim_Ren, Str_Ren));

   end Nested;

   package body Nested is
      procedure Proc is begin null; end Proc;
   end Nested;
end Pack;

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

$ gcc -c pack.adb
$ gcc -c pack.adb -gnatd.F
pack.adb:9:14: warning: variable "Result" is read but never assigned
pack.adb:9:14: warning: variable "Result" is read but never assigned

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

2017-09-08  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_spark.adb (Expand_SPARK_N_Object_Renaming_Declaration):
	Reimplemented.
	(Expand_SPARK_Potential_Renaming): Code clean up.
	* sem_prag.adb (Analyze_Initialization_Item): Add a guard in case
	the item does not have a proper entity.
	(Analyze_Input_Item): Add a guard in case the item does not have a
	proper entity.
	(Collect_States_And_Objects): Include object renamings in the
	items being collected.
	(Resolve_State): Update the documentation of this routine.
	* sem_util.adb (Entity_Of): Add circuitry to handle
	renamings of function results.
	(Remove_Entity): New routine.
	(Remove_Overloaded_Entity): Take advantage of factorization.
	* sem_util.ads (Entity_Of): Update the documentation
	of this routine.
	(Remove_Entity): New routine.
	(Remove_Overloaded_Entity): Update the documentation of this
	routine.

Attachment: difs
Description: Text document


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]