[Ada] Obscure messages due to freezing of contracts

[Ada] Obscure messages due to freezing of contracts

[Arnaud Charlet]

[-- Attachment #1: Type: text/plain, Size: 2946 bytes --]

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 #2: difs --]
[-- Type: text/plain, Size: 859 bytes --]

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 230236)
+++ sem_prag.adb	(working copy)
@@ -25408,6 +25408,14 @@
                         SPARK_Msg_N
                           ("\all constituents must be declared before body #",
                            N);
+
+                        --  A misplaced constituent is a critical error because
+                        --  pragma Refined_Depends or Refined_Global depends on
+                        --  the proper link between a state and a constituent.
+                        --  Stop the compilation, as this leads to a multitude
+                        --  of misleading cascaded errors.
+
+                        raise Program_Error;
                      end if;
 
                   --  The constituent is a valid state or object