[Ada] Aspects on stubs

Programming / Compilers / GCC - pmderodat [138bc75d-0d04-0410-961f-82ee72b054a4] - 21 May 2018 14:52 EDT

This patch ensures that aspect specifications which appear on package, protected, and task body stubs are properly analyzed.


-- Source --


-- pack.ads

package Pack with SPARK_Mode, Abstract_State => State is

-- Refined_Depends, Refined_Global --


procedure Proc_1; procedure Proc_2 with Global => (In_Out => State), Depends => (State => State);

task Task_Obj_1; task Task_Obj_2 with Global => (In_Out => State), Depends => (State => State);


-- Refined_Post --


function Func_1 (Formal : Integer) return Integer; function Func_2 (Formal : Integer) return Integer with Post => Func_2'Result > Formal;


-- Refined_State --


package Pack_1 is end Pack_1; package Pack_2 with Abstract_State => State_2 is end Pack_2;


-- SPARK_Mode --


package Pack_3 with SPARK_Mode => Off is end Pack_3; package Pack_4 with SPARK_Mode => Off is end Pack_4; package Pack_5 is end Pack_5;

protected type Prot_Typ_1 with SPARK_Mode => Off is end Prot_Typ_1; protected type Prot_Typ_2 with SPARK_Mode => Off is end Prot_Typ_2; protected type Prot_Typ_3 is end Prot_Typ_3;

procedure Proc_3 with SPARK_Mode => Off; procedure Proc_4 with SPARK_Mode => Off; procedure Proc_5;

task type Task_Typ_1 with SPARK_Mode => Off; task type Task_Typ_2 with SPARK_Mode => Off; task type Task_Typ_3; end Pack;

-- pack.adb

package body Pack with SPARK_Mode, Refined_State => (State => Constit) is Constit : Integer := 0;


-- Refined_Depends, Refined_Global --


procedure Proc_1 is separate with Refined_Global => (In_Out => Constit), -- Error Refined_Depends => (Constit => Constit); -- Error

procedure Proc_2 is separate with Refined_Global => (In_Out => Constit), -- OK Refined_Depends => (Constit => Constit); -- OK

task body Task_Obj_1 is separate with Refined_Global => (In_Out => Constit), -- Error Refined_Depends => (Constit => Constit); -- Error

task body Task_Obj_2 is separate with Refined_Global => (In_Out => Constit), -- OK Refined_Depends => (Constit => Constit); -- OK


-- Refined_Post --


function Func_1 (Formal : Integer) return Integer is separate with Refined_Post => Func_1'Result > Formal; -- OK

function Func_2 (Formal : Integer) return Integer is separate with Refined_Post => Func_2'Result > Formal; -- OK


-- Refined_State --


package body Pack_1 is separate with Refined_State => (State_1 => Constit_1); -- Error

package body Pack_2 is separate with Refined_State => (State_2 => Constit_2); -- Error


-- SPARK_Mode --


package body Pack_3 is separate with SPARK_Mode => On; -- Error package body Pack_4 is separate; package body Pack_5 is separate with SPARK_Mode => Off; -- Error

protected body Prot_Typ_1 is separate with SPARK_Mode => On; -- Error protected body Prot_Typ_2 is separate; protected body Prot_Typ_3 is separate with SPARK_Mode => Off; -- Error

procedure Proc_3 is separate with SPARK_Mode => On; -- Error procedure Proc_4 is separate; procedure Proc_5 is separate with SPARK_Mode => Off; -- Error

task body Task_Typ_1 is separate with SPARK_Mode => On; -- Error task body Task_Typ_2 is separate; task body Task_Typ_3 is separate with SPARK_Mode => Off; -- Error end Pack;

-- pack-func_1.adb

separate (Pack)

function Func_1 (Formal : Integer) return Integer with Refined_Post => Func_1'Result > Formal -- Error is begin return Formal * 10; end Func_1;

-- pack-func_2.adb

separate (Pack)

function Func_2 (Formal : Integer) return Integer with Refined_Post => Func_2'Result > Formal -- Error is begin return Formal * 10; end Func_2;

-- pack-pack_1.adb

separate (Pack)

package body Pack_1 with SPARK_Mode, Refined_State => (State_1 => Constit_1) -- Error is Constit_1 : Integer := 1; end Pack_1;

-- pack-pack_2.adb

separate (Pack)

package body Pack_2 with SPARK_Mode, Refined_State => (State_2 => Constit_2) -- OK is Constit_2 : Integer := 2; end Pack_2;

-- pack-pack_3.adb

separate (Pack)

package body Pack_3 is end Pack_3;

-- pack-pack_4.adb

separate (Pack)

package body Pack_4 with SPARK_Mode => On is end Pack_4; -- OK

-- pack-pack_5.adb

separate (Pack)

package body Pack_5 with SPARK_Mode => On is end Pack_5; -- OK

-- pack-proc_1.adb

separate (Pack)

procedure Proc_1 with Refined_Global => (In_Out => Constit), -- Error Refined_Depends => (Constit => Constit) -- Error is begin null; end Proc_1;

-- pack-proc_2.adb

separate (Pack)

procedure Proc_2 with Refined_Global => (In_Out => Constit), -- Error Refined_Depends => (Constit => Constit) -- Error is begin null; end Proc_2;

-- pack-proc_3.adb

separate (Pack)

procedure Proc_3 is begin null; end Proc_3;

-- pack-proc_4.adb

separate (Pack)

procedure Proc_4 with SPARK_Mode => On is begin null; end Proc_4; -- OK

-- pack-proc_5.adb

separate (Pack)

procedure Proc_5 with SPARK_Mode => On is begin null; end Proc_5; -- OK

-- pack-prot_typ_1.adb

separate (Pack)

protected body Prot_Typ_1 is end Prot_Typ_1;

-- pack-prot_typ_2.adb

separate (Pack)

protected body Prot_Typ_2 with SPARK_Mode => On is end Prot_Typ_2; -- OK

-- pack-prot_typ_3.adb

separate (Pack)

protected body Prot_Typ_3 with SPARK_Mode => On is end Prot_Typ_3; -- OK

-- pack-task_obj_1.adb

separate (Pack)

task body Task_Obj_1 with Refined_Global => (In_Out => Constit), -- Error Refined_Depends => (Constit => Constit) -- Error is begin null; end Task_Obj_1;

-- pack-task_obj_2.adb

separate (Pack)

task body Task_Obj_2 with Refined_Global => (In_Out => Constit), -- Error Refined_Depends => (Constit => Constit) -- Error is begin null; end Task_Obj_2;

-- pack-task_typ_1.adb

separate (Pack)

task body Task_Typ_1 is begin null; end Task_Typ_1;

-- pack-task_typ_2.adb

separate (Pack)

task body Task_Typ_2 with SPARK_Mode => On is -- OK begin null; end Task_Typ_2;

-- pack-task_typ_3.adb

separate (Pack)

task body Task_Typ_3 with SPARK_Mode => On is -- OK begin null; end Task_Typ_3;


-- Compilation and output --


$ gcc -c pack.adb pack.adb:12:11: useless refinement, declaration of subprogram "Proc_1" lacks aspect or pragma Global pack.adb:13:11: useless refinement, declaration of subprogram "Proc_1" lacks aspect or pragma Depends pack.adb:20:11: useless refinement, declaration of task type "Task_Obj_1" lacks aspect or pragma Global pack.adb:21:11: useless refinement, declaration of task type "Task_Obj_1" lacks aspect or pragma Depends pack.adb:42:11: aspect "Refined_State" must apply to a package body pack.adb:45:11: aspect "Refined_State" must apply to a package body pack.adb:51:41: incorrect placement of aspect "Spark_Mode" pack.adb:53:41: incorrect placement of aspect "Spark_Mode" pack.adb:55:47: incorrect placement of aspect "Spark_Mode" pack.adb:57:47: incorrect placement of aspect "Spark_Mode" pack.adb:59:38: incorrect placement of aspect "Spark_Mode" pack.adb:61:38: incorrect placement of aspect "Spark_Mode" pack.adb:63:42: incorrect placement of aspect "Spark_Mode" pack.adb:65:42: incorrect placement of aspect "Spark_Mode" pack-proc_1.adb:4:08: aspect "Refined_Global" cannot apply to a subunit pack-proc_1.adb:5:08: aspect "Refined_Depends" cannot apply to a subunit pack-proc_2.adb:4:08: aspect "Refined_Global" cannot apply to a subunit pack-proc_2.adb:5:08: aspect "Refined_Depends" cannot apply to a subunit pack-task_obj_1.adb:4:08: aspect "Refined_Global" cannot apply to a subunit pack-task_obj_1.adb:5:08: aspect "Refined_Depends" cannot apply to a subunit pack-task_obj_2.adb:4:08: aspect "Refined_Global" cannot apply to a subunit pack-task_obj_2.adb:5:08: aspect "Refined_Depends" cannot apply to a subunit pack-func_1.adb:4:08: aspect "Refined_Post" cannot apply to a subunit pack-func_2.adb:4:08: aspect "Refined_Post" cannot apply to a subunit pack-pack_1.adb:3:14: body of package "Pack_1" has unused hidden states pack-pack_1.adb:3:14: variable "Constit_1" defined at line 7 pack-pack_1.adb:5:08: useless refinement, package "Pack_1" does not define abstract states pack-pack_1.adb:5:26: "State_1" is undefined pack-pack_3.adb:3:01: incorrect use of SPARK_Mode at pack.adb:2 pack-pack_3.adb:3:01: value Off was set for SPARK_Mode on "Pack_3" at pack.ads:38 pack-pack_4.adb:3:01: incorrect use of SPARK_Mode at pack.adb:2 pack-pack_4.adb:3:01: value Off was set for SPARK_Mode on "Pack_4" at pack.ads:39 pack-pack_4.adb:3:26: incorrect use of SPARK_Mode pack-pack_4.adb:3:26: value Off was set for SPARK_Mode on "Pack_4" at pack.ads:39 pack-prot_typ_2.adb:3:32: incorrect use of SPARK_Mode pack-prot_typ_2.adb:3:32: value Off was set for SPARK_Mode on "Prot_Typ_2" at pack.ads:43 pack-proc_3.adb:3:01: incorrect use of SPARK_Mode at pack.adb:2 pack-proc_3.adb:3:01: value Off was set for SPARK_Mode on "Proc_3" at pack.ads:46 pack-proc_4.adb:3:01: incorrect use of SPARK_Mode at pack.adb:2 pack-proc_4.adb:3:01: value Off was set for SPARK_Mode on "Proc_4" at pack.ads:47 pack-proc_4.adb:3:23: incorrect use of SPARK_Mode pack-proc_4.adb:3:23: value Off was set for SPARK_Mode on "Proc_4" at pack.ads:47 pack-task_typ_2.adb:3:27: incorrect use of SPARK_Mode pack-task_typ_2.adb:3:27: value Off was set for SPARK_Mode on "Task_Typ_2" at pack.ads:51

2018-05-21 Hristian Kirtchev

gcc/ada/

- sem_ch6.adb (Analyze_Generic_Subprogram_Body): Rename the call to Analyze_Aspect_Specifications_On_Body_Or_Stub. (Analyze_Subprogram_Body_Helper): Rename the calls to Analyze_Aspect_Specifications_On_Body_Or_Stub.
- sem_ch9.adb (Analyze_Entry_Body): Rename the call to Analyze_Aspect_Specifications_On_Body_Or_Stub.
- sem_ch10.adb: Add with and use clause for Sem_Ch13. (Analyze_Package_Body_Stub): Add constant Id. Decorate the package stub prior to analyzing its aspects. (Analyze_Protected_Body_Stub): Add constant Id. Decorate the package stub prior to analyzing its aspects. Save and restore the configuration switches. (Analyze_Task_Body_Stub): Add constant Id. Decorate the package stub prior to analyzing its aspects.
- sem_ch13.adb (Analyze_Aspect_Specifications_On_Body_Or_Stub): Renamed to Analyze_Aspects_On_Subprogram_Body_Or_Stub.
- sem_ch13.ads (Analyze_Aspect_Specifications_On_Body_Or_Stub): Renamed to Analyze_Aspects_On_Subprogram_Body_Or_Stub.
- sem_prag.adb: Code reformatting. (Analyze_Refined_Depends_Global_Post): Consider task body stubs.

f38beee57d4 [Ada] Aspects on stubs
gcc/ada/ChangeLog | 23 +++++++++++++
gcc/ada/sem_ch10.adb | 51 ++++++++++++++++++++++------
gcc/ada/sem_ch13.adb | 12 +++----
gcc/ada/sem_ch13.ads | 2 +-
gcc/ada/sem_ch6.adb | 6 ++--
gcc/ada/sem_ch9.adb | 2 +-
gcc/ada/sem_prag.adb | 94 ++++++++++------------------------------------------
7 files changed, 92 insertions(+), 98 deletions(-)

Upstream: gcc.gnu.org


  • Share