[Ada] Allow constants in SPARK contracts

[Arnaud Charlet <charlet at adacore dot com>]

This patch permits constants to appear in the following SPARK annotations:

   Depends
   Global
   Initializes
   Part_Of
   Refined_Depends
   Refined_Global
   Refined_State

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

--  legal_usage.ads

package Legal_Usage
  with SPARK_Mode,
       Abstract_State    => State,
       Initializes       => (C1, C2),
       Initial_Condition => (C1 = 1 and then C2 = 2)
is
   C1 : constant Integer := 1;
   C2 : constant Integer := 2;

   function Func (Formal : Integer) return Integer
     with Global  => (Input => (C1, C2, State)),
          Depends => (Func'Result => (Formal, C1, C2, State));

private
   C3 : constant Integer := 3 with Part_Of => State;
end Legal_Usage;

--  legal_usage.adb

package body Legal_Usage
  with SPARK_Mode,
       Refined_State => (State => (C3, C4))
is
   C4 : constant Integer := 4;

   function Func (Formal : Integer) return Integer
     with Refined_Global  => (Input => (C1, C2, C3, C4)),
          Refined_Depends => (Func'Result => (Formal, C1, C2, C3, C4))
   is
   begin
      return Formal + C1 + C2 + C3 + C4;
   end Func;
end Legal_Usage;

--  illegal_usage.ads

package Illegal_Usage is
   C1 : constant Integer := 1;

   procedure Error_1
     with Global => (In_Out => C1);

   procedure Error_2
     with Global => (Output => C1);

   procedure Error_3 (Formal : Integer)
     with Depends => (C1 => Formal);

   procedure Error_4 (Formal : Integer)
     with Global  => (Input => C1),
          Depends => (C1 => Formal);
end Illegal_Usage;

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

$ gcc -c legal_usage.adb
$ gcc -c illegal_usage.adb
illegal_usage.ads:5:32: constant "C1" cannot act as output
illegal_usage.ads:8:32: constant "C1" cannot act as output
illegal_usage.ads:11:23: read-only constant "C1" cannot appear as output in
  dependence relation
illegal_usage.ads:14:32: constant "C1" must appear in at least one input
  dependence list
illegal_usage.ads:15:23: read-only constant "C1" cannot appear as output in
  dependence relation

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

2015-05-21  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb (Contract): This attribute now applies to constants.
	(Set_Contract): This attribute now applies to constants.
	(Write_Field34_Name): Add output for constants.
	* einfo.ads Attribute Contract now applies to constants.
	* sem_ch3.adb (Analyze_Object_Contract): Constants now have
	their Part_Of indicator verified.
	* sem_prag.adb (Analyze_Constituent): A constant is now a valid
	constituent.
	(Analyze_Global_Item): A constant cannot act as an output.
	(Analyze_Initialization_Item): Constants are now a valid
	initialization item.
	(Analyze_Initializes_In_Decl_Part): Rename
	global variable States_And_Vars to States_And_Objs and update
	all its occurrences.
	(Analyze_Input_Item): Constants are now a
	valid initialization item. Remove SPARM RM references from error
	messages.
	(Analyze_Pragma): Indicator Part_Of can now apply to a constant.
	(Collect_Body_States): Collect both source constants
	and variables.
	(Collect_States_And_Objects): Collect both source constants and
	variables.
	(Collect_States_And_Variables): Rename
	to Collect_States_And_Objects and update all its occurrences.
	(Collect_Visible_States): Do not collect constants and variables
	used to map generic formals to actuals.
	(Find_Role): The role of a constant is that of an input. Separate the
	role of a variable from that of a constant.
	(Report_Unused_Constituents): Add specialized wording for constants.
	(Report_Unused_States): Add specialized wording for constants.
	* sem_util.adb (Add_Contract_Item): Add processing for constants.
	* sem_util.ads (Add_Contract_Item): Update the comment on usage.
	(Find_Placement_In_State_Space): Update the comment on usage.

Attachment: difs
Description: Text document