[Ada] Legality rules for aspect Depends

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements the following legality rules concerning aspect Depends:

An input must have a mode of in or in out and an output must have an mode of
in out or out. [Note: As a consequence an entity which is both an input and an
output shall have a mode of in out.]

Every output of the subprogram shall appear in exactly one output_list.

Every input of the subprogram shall appear in at least one input_list.

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

--  semantics.ads

package Semantics
  with Abstract_State =>
    ((Input_State  with Volatile, Input),
     (Output_State with Volatile, Output))
is
   Input_Var  : Integer;  --  in
   Mixed_Var  : Integer;  --  in out
   Output_Var : Integer;  --     out

   --  Legality rule 2:
   --  An input must have a mode of in or in out and an output must have an
   --  mode of in out or out.

   --  Input
   --    formals of mode in or in out
   --    items in lists Input and In_Out of aspect Global (if available)

   procedure OK_1 (Formal_1 : Integer; Formal_2 : in out Integer) with
     Global =>
       (Input  =>
          (Input_State, Input_Var),
        Output =>
          (Output_State, Output_Var),
        In_Out =>
           Mixed_Var),

     Depends =>
       ((Formal_2,
         Mixed_Var,
         Output_State,
         Output_Var) => (Formal_1,
                         Formal_2,
                         Input_State,
                         Input_Var,
                         Mixed_Var));

   procedure Error_1 (Formal : Integer) with
     Global =>
       (Input  =>
          (Input_State, Input_Var),
        Output =>
          (Output_State, Output_Var),
        In_Out =>
           Mixed_Var),

     Depends =>
       ((Formal,       --  error
         Input_State,  --  error
         Input_Var,    --  error
         Mixed_Var,
         Output_State,
         Output_Var) => Mixed_Var);

   --  Output
   --    the result of a function (if applicable)
   --    formals of mode out or in out
   --    items in lists Output and In_Out of aspect Global (if available)

   procedure OK_2 (Formal_1 : in out Integer; Formal_2 : out Integer) with
     Global =>
       (Input  =>
          (Input_State, Input_Var),
        Output =>
          (Output_State, Output_Var),
        In_Out =>
           Mixed_Var),

     Depends =>
       ((Formal_1,
         Formal_2,
         Mixed_Var,
         Output_State,
         Output_Var) => (Input_State,
                         Input_Var,
                         Mixed_Var));

   function OK_3 return Integer with
     Depends => (OK_3'Result => null);

   procedure Error_2 (Formal_1 : in out Integer; Formal_2 : out Integer) with
     Global =>
       (Input  =>
          (Input_State, Input_Var),
        Output =>
          (Output_State, Output_Var),
        In_Out =>
           Mixed_Var),

     Depends =>
       ((Formal_1,
         Formal_2,
         Mixed_Var,
         Output_State,
         Output_Var) => (Formal_1,
                         Formal_2,      --  error
                         Input_State,
                         Input_Var,
                         Mixed_Var,
                         Output_State,  --  error
                         Output_Var));  --  error

   --  Legality rule 7
   --  Every output of the subprogram shall appear in exactly one output list

   function Error_3 return Integer with  --  error
     Depends => null;

   procedure Error_4 (Formal : out Integer) with  --  error
     Global =>
       (Output =>
          (Output_State, Output_Var),             --  error
        In_Out =>
           Mixed_Var),                            --  error

     Depends =>
       (null => Mixed_Var);

   --  Legality rule 8
   --  Every input of the subprogram shall appear in at least one input list

   procedure Error_5 (Formal_1 : Integer) with  --  error
     Global =>
       (Input  =>
          (Input_State, Input_Var),             --  error
        In_Out =>
           Mixed_Var),                          --  error

     Depends => null;
end Semantics;

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

$ gcc -c -gnat12 -gnatd.V semantics.ads
semantics.ads:47:10: item "Formal" must have mode out or in out
semantics.ads:48:10: item "Input_State" must have mode out or in out
semantics.ads:49:10: item "Input_Var" must have mode out or in out
semantics.ads:95:26: item "Formal_2" must have mode in or in out
semantics.ads:99:26: item "Output_State" must have mode in or in out
semantics.ads:100:26: item "Output_Var" must have mode in or in out
semantics.ads:106:06: result of "Error_3" must appear in exactly one output
  list
semantics.ads:108:23: item "Formal" must appear in exactly one output list of
  aspect Depends
semantics.ads:111:12: item "Output_State" must appear in exactly one output
  list of aspect Depends
semantics.ads:111:26: item "Output_Var" must appear in exactly one output list
  of aspect Depends
semantics.ads:113:12: item "Mixed_Var" must appear in exactly one output list
  of aspect Depends
semantics.ads:121:23: item "Formal_1" must appear in at least one input list of
  aspect Depends
semantics.ads:124:12: item "Input_State" must appear in at least one input list
  of aspect Depends
semantics.ads:124:25: item "Input_Var" must appear in at least one input list
  of aspect Depends
semantics.ads:126:12: item "Mixed_Var" must appear in at least one input list
  of aspect Depends

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

2013-04-12  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch13.adb (Analyze_Aspect_Specifications): Aspect
	Depends is now a delayed aspect. The delay is required
	due to the interplay between aspects Depends and Global.
	(Check_Aspect_At_Freeze_Point): Add an entry for aspect Depends.
	* sem_prag.adb: Reformat various error messages.
	(Add_Item): New subsidiary routine.
	(Analyze_Pragma): Add new variables
	Global_Seen, Result_Seen, Subp_Inputs and Subp_Outputs. The
	analysis of pragma Depends now has the capability to check
	the proper mode and usage of subprogram inputs and outputs.
	(Appears_In): New routine.
	(Check_Function_Return): New routine.
	(Check_Mode): New routine.
	(Check_Usage): New routine.
	(Collect_Subprogram_Inputs_Outputs): New routine.

Attachment: difs
Description: Text document