[Ada] Syntax checks when SPARK_Mode is Off

[Arnaud Charlet <charlet at adacore dot com>]

This patch adds syntax checks for SPARK aspects/pragmas Abstract_State,
Depends, Global, Initializes, Part_Of, Refined_Global, Refined_Depends and
Refined_State that trigger when SPARK features are disabled through SPARK_Mode
=> Off. The patch also suppresses refinement-related checks when the associated
context is a package or subprogram body.

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

--  issue_when_off.ads

package Issue_When_Off
  with SPARK_Mode     => Off,
       Abstract_State => "junk state",  --  error
       Initializes    => 1+2,           --  error
       Initial_Condition => 3.4         --  error
is
   procedure Error
     with Global  => (OK_Mode  => "global item"),  --  error
          Depends => ("output" => 56);             --  error
end Issue_When_Off;

--  issue_when_off.adb

package body Issue_When_Off
  with SPARK_Mode    => Off,
       Refined_State => ("state" => (123, "constituent"))  --  error
is
   procedure Error
     with Refined_Global  => (OK_Mode  => "global item"),  --  error
          Refined_Depends => ("output" => (4.5, "input"))  --  error
   is begin null; end Error;
end Issue_When_Off;

--  suppress_when_off.ads

package Suppress_When_Off
  with SPARK_Mode        => Off,
       Abstract_State    => State
is
   Var : Integer := 0;

   function OK_1 (Formal : Integer) return Integer
     with Global  => (Input => (State, Var)),
          Depends => (OK_1'Result => (State, Var));

   procedure OK_2;
end Suppress_When_Off;

--  suppress_when_off.adb

package body Suppress_When_Off                         --  suppressed error
  with SPARK_Mode => Off
is
   function OK_1 (Formal : Integer) return Integer is  --  suppress error
   begin
      return -1;
   end OK_1;

   procedure OK_2
     with Refined_Global  => null,                    --  suppressed error
          Refined_Depends => null                     --  suppressed error
   is begin null; end OK_2;
end Suppress_When_Off;

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

$ gcc -c issue_when_off.adb
$ gcc -c suppress_when_off.adb
issue_when_off.adb:3:26: malformed item
issue_when_off.adb:3:38: malformed item
issue_when_off.adb:3:43: malformed item
issue_when_off.adb:6:43: malformed global list
issue_when_off.adb:7:31: malformed item
issue_when_off.adb:7:44: malformed item
issue_when_off.adb:7:49: malformed item
issue_when_off.ads:3:26: malformed abstract state declaration
issue_when_off.ads:4:27: malformed item
issue_when_off.ads:5:29: expected type "Standard.Boolean"
issue_when_off.ads:5:29: found type universal real
issue_when_off.ads:8:35: malformed global list
issue_when_off.ads:9:23: malformed item
issue_when_off.ads:9:35: malformed input dependency list

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

2014-02-24  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Do not enforce
	global and dependence refinement when SPARK_Mode is off.
	* sem_ch7.adb (Analyze_Package_Body_Contract): Do not enforce
	state refinement when SPARK_Mode is off.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add local
	variable Decl. Insert the generated pragma for Refined_State
	after a potential pragma SPARK_Mode.
	* sem_prag.adb (Analyze_Depends_In_Decl_Part): Add local
	constant Deps. Remove local variable Expr. Check the syntax
	of pragma Depends when SPARK_Mode is off. Factor out the
	processing for extra parenthesis around individual clauses.
	(Analyze_Global_In_Decl_List): Items is now a constant. Check
	the syntax of pragma Global when SPARK_Mode is off.
	(Analyze_Initializes_In_Decl_Part): Check the syntax of pragma
	Initializes when SPARK_Mode is off.
	(Analyze_Part_Of): Check
	the syntax of the encapsulating state when SPARK_Mode is off.
	(Analyze_Pragma): Check the syntax of pragma Abstract_State when
	SPARK_Mode is off. Move the declaration order check with respect
	to pragma Initializes to the end of the processing. Do not verify
	the declaration order for pragma Initial_Condition when SPARK_Mode
	is off. Do not complain about a useless package refinement when
	SPARK_Mode is off.
	(Analyze_Refined_Depends_In_Decl_Part): Refs
	is now a constant. Check the syntax of pragma Refined_Depends
	when SPARK_Mode is off.
	(Analyze_Refined_Global_In_Decl_Part):
	Check the syntax of pragma Refined_Global when SPARK_Mode is off.
	(Analyze_Refined_State_In_Decl_Part): Check the syntax of pragma
	Refined_State when SPARK_Mode is off.
	(Check_Dependence_List_Syntax): New routine.
	(Check_Global_List_Syntax): New routine.
	(Check_Initialization_List_Syntax): New routine.
	(Check_Item_Syntax): New routine.
	(Check_State_Declaration_Syntax): New routine.
	(Check_Refinement_List_Syntax): New routine.
	(Has_Extra_Parentheses): Moved to the top level of Sem_Prag.

Attachment: difs
Description: Text document