[Ada] Warn on weal elaboration model for SPARK

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

This patch introduces a check which ensures that SPARK elaboration code is
processed using the static elaboration model as it guarantees the highest
degree of safety.

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

--  spark_pack.ads

package SPARK_Pack with SPARK_Mode is
   pragma Elaborate_Body;

   type Root is tagged null record;
   procedure Prim (Obj : Root);

   type Child is new Root with null record;
   procedure Prim (Obj : Child);
end SPARK_Pack;

--  spark_pack.adb

with Ada.Text_IO; use Ada.Text_IO;

package body SPARK_Pack with SPARK_Mode is
   procedure Prim (Obj : Root) is
   begin
      Put_Line ("Root.Prim");
   end Prim;

   procedure Prim (Obj : Child) is
   begin
      Put_Line ("Child.Prim");
   end Prim;
end SPARK_Pack;

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

$ echo "Static model"
$ gcc -c spark_pack.adb
$ echo "Relaxed static model"
$ gcc -c spark_pack.adb        -gnatJ
$ echo "Dynamic model"
$ gcc -c spark_pack.adb -gnatE
$ echo "Relaxed dynamic model"
$ gcc -c spark_pack.adb -gnatE -gnatJ
Static model
Relaxed static model
spark_pack.ads:7:04: warning: SPARK elaboration checks require static
  elaboration model
spark_pack.ads:7:04: warning: relaxed elaboration model is in effect
Dynamic model
spark_pack.ads:4:09: warning: SPARK elaboration checks require static
  elaboration model
spark_pack.ads:4:09: warning: dynamic elaboration model is in effect
Relaxed dynamic model
spark_pack.ads:4:09: warning: SPARK elaboration checks require static
  elaboration model
spark_pack.ads:4:09: warning: dynamic elaboration model is in effect

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

2017-12-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_elab.adb: Update the terminology and switch sections.
	(Check_SPARK_Model_In_Effect): New routine.
	(Check_SPARK_Scenario): Verify the model in effect for SPARK.
	(Process_Conditional_ABE_Call_SPARK): Verify the model in effect for
	SPARK.
	(Process_Conditional_ABE_Instantiation_SPARK): Verify the model in
	effect for SPARK.
	(Process_Conditional_ABE_Variable_Assignment_SPARK): Verify the model
	in effect for SPARK.

Attachment: difs
Description: Text document