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] Pragma SPARK_Mode and expression functions


This patch ensures that an internally generated subprogram body that completes
an expression function inherits the SPARK_Mode from the expression function
spec.

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

--  expr_funcs.ads

package Expr_Funcs with SPARK_Mode is
   function F1 return Boolean is (True);  --  F1 spec has mode ON
   function F2 return Boolean;            --  F2 spec has mode ON
   function F3 return Boolean;            --  F3 spec has mode ON

private
   pragma SPARK_Mode (Off);

-- function F1 return Boolean is          --  F1 body has mode ON
-- begin
--    return True;
-- end F1;

   function F2 return Boolean is (True);  --  F2 body has mode OFF
   function F3 return Boolean is (True)   --  F3 body attempts mdoe ON
     with SPARK_Mode;                     --                         Error
end Expr_Funcs;

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

$ gcc -c expr_funcs.ads
expr_funcs.ads:16:11: cannot change SPARK_Mode from Off to On
expr_funcs.ads:16:11: SPARK_Mode was set to Off at line 7

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

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

	* inline.adb (Is_Expression_Function): Removed.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): An internally
	generated subprogram body that completes an expression function
	inherits the SPARK_Mode from the spec.
	* sem_res.adb (Resolve_Call): Update all calls to
	Is_Expression_Function.
	* sem_util.ads, sem_util.adb (Is_Expression_Function): Reimplemented.
	(Is_Expression_Function_Or_Completion): New 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]