[Ada] Aspect / pragma SPARK_Mode

This patch provides the initial implementation of aspect/pragma SPARK_Mode. It
is intended for formal verification and has no effect on generated code.

The semantics of the aspect/pragma are as follows:

   pragma SPARK_Mode [ (On | Off | Auto) ] ;

When used as a configuration pragma on a single file or a set of files, this
sets the mode of the units involved, in particular:

   On : all entities in the units should follow the SPARK 2014 language, and an
error will be generated if not, unless locally overriden via a local SPARK_Mode
pragma or aspect. On is the default if pragma SPARK_Mode is used without any
parameter.

    Off : the units are considered to be in Ada by default and therefore not
part of SPARK 2014 unless overriden locally. These units may be called by SPARK
units.

    Auto : this one is more on the tools side, so potentially not part of the
SPARK 2014 Reference Manual (TBD). The tools will automatically detect for each
entity whether the entity is in SPARK or in Ada and may also provide ways to
know which entities are in or out SPARK.

When used as a local pragma, you can use it in a restricted set of places, with
only On or Off valid values (no Auto), with the following semantic:

    * After package X is, to mark a whole package (spec+body) either in or out
SPARK.

    * After package body X is, to mark a whole package body in/out SPARK.

    * After a subprogram spec, to mark the subprogram (spec+body) in/out SPARK.

    * After a procedure|function X[...] is, to mark a subprogram body in/out
SPARK.

    * After the private keyword of a package spec to mark the whole private
part of a package spec in/out SPARK.

    * After the begin keyword of a package body to mark the elaboration
procedure of a package in/out SPARK.

When used anywhere else, an error should be generated.

A new aspect: SPARK_Mode [=> On|Off]; which can be used similarly to the
SPARK_Mode pragma to mark package spec/body and procedure spec/body as in/out
SPARK.

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

--  semantics.ads

package Semantics is
   pragma SPARK_Mode (Auto); --  Error, cannot use "Auto" in non-configuration
                             --  variant

   procedure Error_1
   with SPARK_Mode => Junk_Argument; --  Error, unrecognized argument

   procedure Error_2;
   pragma SPARK_Mode (Junk_Formal => Junk_Argument); --  Error, cannot have
                                                     --  associations

   procedure Error_3;
   pragma SPARK_Mode (One, Two, Three); --  Error, can have at most one arg

   package Error_4 is
      procedure Dummy;
   end Error_4;

   procedure Error_5;
   procedure Error_6;

   procedure Error_7;
   pragma SPARK_Mode (On);
   pragma SPARK_Mode (On); --  Error, duplicate pragma

   procedure Error_8 with SPARK_Mode => On;
   pragma SPARK_Mode (On); --  Error, duplicate aspect/pragma combination

   procedure Error_9;

   Obj : Integer;
   pragma SPARK_Mode (On); --  Error, not immediately within package

   package OK_1 is
      pragma SPARK_Mode (On);
   end OK_1;

   package OK_2 with SPARK_Mode => On is
   end OK_2;

   package OK_3 is
   private
      pragma SPARK_Mode (On);
   end OK_3;

   package OK_4 is
      procedure Dummy;
   end OK_4;

   procedure OK_5;
   pragma SPARK_Mode (On);

   procedure OK_6 with SPARK_Mode => On;

   procedure OK_7;
end Semantics;

--  semantics.adb

package body Semantics is
   procedure Error_1 is begin null; end Error_1;
   procedure Error_2 is begin null; end Error_2;
   procedure Error_3 is begin null; end Error_3;

   package body Error_4 is
      procedure Dummy is begin null; end Dummy;
      pragma SPARK_Mode (On); --  Error, not immediately within package
   end Error_4;

   procedure Error_5 is
      Obj : Integer;
      pragma SPARK_Mode (On); --  Error, not immediately within subprogram
   begin
      null;
   end Error_5;

   procedure Error_6 is
      Obj : Integer;
   begin
      Obj := 1234;
      pragma SPARK_Mode (On); --  Error, not immediately within subprogram
   end Error_6;

   procedure Error_7 is begin null; end Error_7;
   procedure Error_8 is begin null; end Error_8;

   procedure Error_9 is
      pragma SPARK_Mode (On);
      pragma SPARK_Mode (On); --  Error, duplicate pragma
   begin
      null;
   end Error_9;

   package body OK_4 is
      pragma SPARK_Mode (On);
      procedure Dummy is begin null; end Dummy;
   end OK_4;

   procedure OK_5 is begin null; end OK_5;
   procedure OK_6 is begin null; end OK_6;

   procedure OK_7 is
      pragma SPARK_Mode (On);
   begin
      null;
   end OK_7;
end Semantics;

--  monotonic_pairs.adb

procedure Monotonic_Pairs is
   package OK_1 is
      pragma SPARK_Mode (On);
   private
      pragma SPARK_Mode (Off);
   end OK_1;

   package OK_2 is
      procedure Dummy;
   end OK_2;

   package body OK_2 is
      pragma SPARK_Mode (On);
      procedure Dummy is begin null; end Dummy;
   begin
      pragma SPARK_Mode (Off);
   end OK_2;

   package OK_3 is
      pragma SPARK_Mode (On);
      procedure Dummy;
   end OK_3;

   package body OK_3 is
      pragma SPARK_Mode (Off);
      procedure Dummy is begin null; end Dummy;
   end OK_3;

   package OK_4 is
      procedure Dummy;
   private
      pragma SPARK_Mode (Off);
   end OK_4;

   package body OK_4 is
      pragma SPARK_Mode (On);  --  OK, Off applies to the private part only
      procedure Dummy is begin null; end Dummy;
   end OK_4;

   package OK_5 is
      procedure Dummy;
   private
      pragma SPARK_Mode (Off);
   end OK_5;

   package body OK_5 is
      procedure Dummy is begin null; end Dummy;
   begin
      pragma SPARK_Mode (On);  --  OK, Off applies to the private part only
   end OK_5;

   package OK_Subprograms is
      procedure OK_6;
      pragma SPARK_Mode (On);
   end OK_Subprograms;

   package body OK_Subprograms is
      procedure OK_6 is
         pragma SPARK_Mode (Off);
      begin null; end OK_6;
   end OK_Subprograms;

   package Error_1 is
      pragma SPARK_Mode (Off);
   private
      pragma SPARK_Mode (On);  --  Error
   end Error_1;

   package Error_2 is
      procedure Dummy;
   end Error_2;

   package body Error_2 is
      pragma SPARK_Mode (Off);
      procedure Dummy is begin null; end Dummy;
   begin
      pragma SPARK_Mode (On);  --  Error
   end Error_2;

   package Error_3 is
      pragma SPARK_Mode (Off);
      procedure Dummy;
   end Error_3;

   package body Error_3 is
      pragma SPARK_Mode (On);  --  Error
      procedure Dummy is begin null; end Dummy;
   end Error_3;

   package Error_Subprograms is
      procedure Error_4;
      pragma SPARK_Mode (Off);
   end Error_Subprograms;

   package body Error_Subprograms is
      procedure Error_4 is
         pragma SPARK_Mode (On);  --  Error
      begin null; end Error_4;
   end Error_Subprograms;
begin
   null;
end Monotonic_Pairs;

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

$ gcc -c semantics.adb
$ gcc -c monotonic_pairs.adb
semantics.adb:8:07: incorrect placement of pragma "Spark_Mode"
semantics.adb:13:07: incorrect placement of pragma "Spark_Mode"
semantics.adb:22:07: incorrect placement of pragma "Spark_Mode"
semantics.adb:30:07: pragma "Spark_Mode" duplicates pragma declared at line 29
semantics.ads:2:23: mode "Auto" can only apply to the configuration variant of
  pragma "Spark_Mode"
semantics.ads:6:23: invalid argument for aspect "Spark_Mode"
semantics.ads:9:23: pragma "Spark_Mode" does not permit identifier
  "Junk_Formal" here
semantics.ads:13:28: too many arguments for pragma "Spark_Mode"
semantics.ads:24:04: pragma "Spark_Mode" duplicates pragma declared at line 23
semantics.ads:27:04: pragma "Spark_Mode" duplicates pragma declared at line 26
semantics.ads:32:04: incorrect placement of pragma "Spark_Mode"
monotonic_pairs.adb:66:07: cannot define SPARK mode "On"
monotonic_pairs.adb:66:07: mode is less restrictive than mode "Off" defined at
  line 64
monotonic_pairs.adb:77:07: cannot define SPARK mode "On"
monotonic_pairs.adb:77:07: mode is less restrictive than mode "Off" defined at
  line 74
monotonic_pairs.adb:86:07: cannot define SPARK mode "On"
monotonic_pairs.adb:86:07: mode is less restrictive than mode "Off" defined at
  line 81
monotonic_pairs.adb:97:10: cannot define SPARK mode "On"
monotonic_pairs.adb:97:10: mode is less restrictive than mode "Off" defined at
  line 92

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

2013-07-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add an entry for SPARK_Mode in table Canonical_Aspect.
	* aspects.ads: Add an entry for SPARK_Mode in tables Aspect_Id,
	Aspect_Argument, Aspect_Names.
	* atree.adb (Node32): New routine.
	(Set_Node32): New routine.
	* atree.ads (Node32): New routine.
	(Set_Node32): New routine.
	* einfo.adb: Node32 is now used as SPARK_Mode_Pragmas.
	(Set_SPARK_Mode_Pragmas): New routine.
	(SPARK_Mode_Pragmas): New routine.
	(Write_Field32_Name): Add and entry for SPARK_Modes.
	* einfo.ads: Add attribute SPARK_Mode_Pragmas along with usage
	in various entities.
	(Set_SPARK_Mode_Pragmas): New routine and
	pragma Inline.
	(SPARK_Mode_Pragmas): New routine and pragma Inline.
	* gnat_rm.texi: Add sections explaining the syntax and semantics
	of aspect/pragma SPARK_Mode.
	* gnat_ugn.texi: Add pragma SPARK_Mode to the list of
	configuration pragmas.
	* lib.adb (Set_SPARK_Mode_Pragma): New routine.
	(SPARK_Mode_Pragma): New routine.
	* lib.ads: Alphabetize the comments on fields of record
	Unit_Record. Add new field SPARK_Mode_Pragma along with
	comment on its usage. Update the layout of record Unit_Record.
	(Set_SPARK_Mode_Pragma): New routine and pragma Inline.
	(SPARK_Mode_Pragma): New routine and pragma Inline.
	* lib-load.adb (Create_Dummy_Package_Unit): Initialize
	field SPARK_Mode_Pragma.
	(Load_Main_Source): Initialize field SPARK_Mode_Pragma.
	(Load_Unit): Initialize field SPARK_Mode_Pragma.
	* lib-writ.adb (Add_Preprocessing_Dependency): Initialize field
	SPARK_Mode_Pragma.
	(Ensure_System_Dependency): Initialize field SPARK_Mode_Pragma.
	* opt.ads: Alphabetize verification flags. Store the
	compilation-wide SPARK mode in variable Global_SPARK_Mode.
	* par-prag.adb: Pragma SPARK_Mode does not need special processing
	by the parser.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Convert aspect
	SPARK_Mode into a pragma.
	(Check_Aspect_At_Freeze_Point): Aspect SPARK_Mode does not need
	delayed processing.
	* sem_prag.adb: Add an entry for SPARK_Mode in table Sig_Flags.
	(Analyze_Pragma): Add processing for pragma SPARK_Mode.
	(Get_SPARK_Mode_Id): New routine.
	(Is_Elaboration_SPARK_Mode): New routine.
	(Is_Private_SPARK_Mode): New routine.
	* sem_prag.ads (Get_SPARK_Mode_Id): New routine.
	(Is_Elaboration_SPARK_Mode): New routine.
	(Is_Private_SPARK_Mode): New routine.
	* sinfo.ads: Update the comment on the usage of field Next_Pragma.
	* snames.ads-tmpl: Add new predefined name for SPARK_Mode and
	Auto. Add new pragma Id for SPARK_Mode.
	* types.ads: Add new type SPARK_Mode_Id.

[Ada] Aspect / pragma SPARK_Mode

Commit Message

Patch