[Ada] Crash on SPARK_Mode with illegal mode

[Pierre-Marie de Rodat <derodat at adacore dot com>]

This patch modifies the processing of aspect or pragma SPARK_Mode to avoid a
crash when the annotation appears with an illegal mode.

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

--  pack.ads

package Pack is
   package Nested_1 with SPARK_Mode => False is
   end Nested_1;

   Obj : constant String := "Illegal";

   package Nested_2 with SPARK_Mode => Obj is
   end Nested_2;

   package Nested_3 is
      pragma SPARK_Mode (True);
   end Nested_3;

   package Nested_4 is
      pragma SPARK_Mode (1.2);
   end Nested_4;
end Pack;

-----------------
-- Compilation --
-----------------

$ gcc -c pack.ads
$ gcc -c pack.ads -gnatd.F
pack.ads:2:40: entity for aspect "Spark_Mode" must be "On" or "Off"
pack.ads:7:40: entity for aspect "Spark_Mode" must be "On" or "Off"
pack.ads:11:26: argument for pragma "Spark_Mode" must be "On" or "Off"
pack.ads:15:26: argument for pragma "Spark_Mode" must be identifier
pack.ads:2:40: entity for aspect "Spark_Mode" must be "On" or "Off"
pack.ads:7:40: entity for aspect "Spark_Mode" must be "On" or "Off"
pack.ads:11:26: argument for pragma "Spark_Mode" must be "On" or "Off"
pack.ads:15:26: argument for pragma "Spark_Mode" must be identifier

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

2017-11-09  Piotr Trojanek  <trojanek@adacore.com>

	* sem_prag.adb (Analyze_Part_Of): Reword error message.
	(Get_SPARK_Mode_Type): Do not raise Program_Error in case pragma
	SPARK_Mode appears with an illegal mode, treat this as a non-existent
	mode.

Attachment: difs
Description: Text document