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