[Ada] Obscure messages due to freezing of contracts

[Arnaud Charlet <charlet at adacore dot com>]

This patch classifies a misplaced constituent as a critical error and stops the
compilation. This ensures that the missing link between a constituent and state
will not cause obscure cascaded errors.

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

--  pack.ads

package Pack
   with Spark_Mode     => On,
        Abstract_State => Top_State,
        Initializes    => Top_State
is
   procedure Do_Something (Value   : in out Natural;
                           Success :    out Boolean)
   with Global  => (In_Out => Top_State),
        Depends => (Value     =>+ Top_State,
                    Success   => (Value, Top_State),
                    Top_State =>+ Value);
end Pack;

--  pack.adb

package body Pack
   with SPARK_Mode    => On,
        Refined_State => (Top_State => (Count, A_Pack.State))
is
   package A_Pack
      with Abstract_State => State,
           Initializes    => State
   is
      procedure A_Proc (Test : in out Natural)
         with Global   => (In_Out =>  State),
              Depends  => (Test   =>+ State,
                           State  =>+ Test);
   end A_Pack;

   package body A_Pack
      with Refined_State => (State => Total)
   is
      Total : Natural := 0;

      procedure A_Proc (Test : in out Natural)
         with Refined_Global  => (In_Out => Total),
              Refined_Depends => ((Test  =>+ Total,
                                   Total =>+ Test)) is
      begin
         if Total > Natural'Last - Test   then
            Total := abs (Total - Test);
         else
            Total := Total + Test;
         end if;
         Test := Total;
      end A_Proc;
   end A_Pack;

   Count : Natural := 0;

   procedure Do_Something (Value   : in out Natural;
                           Success :    out Boolean)
      with Refined_Global  => (In_Out  =>  (Count, A_Pack.State)),
           Refined_Depends => (Value        =>+ (Count, A_Pack.State),
                               Success      =>  (Value, Count, A_Pack.State),
                               Count        =>+ null,
                               A_Pack.State =>+ (Count, Value)) is
   begin
      Count := Count rem 128;
      if Count <= Value then
         Value := Count + (Value - Count) / 2;
      else
         Value := Value + (Count - Value) / 2;
      end if;
      A_Pack.A_Proc (Value);
      Success := Value /= 0;
   end Do_Something;
end Pack;

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

$ gcc -c pack.adb
pack.adb:3:09: body "A_Pack" declared at line 15 freezes the contract of "Pack"
pack.adb:3:09: all constituents must be declared before body at line 15
pack.adb:3:41: "Count" is undefined
compilation abandoned due to previous error

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

2015-11-12  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Constituent): Stop the
	analysis after detecting a misplaced constituent as this is a
	critical error.

Attachment: difs
Description: Text document