bugbox triggered by Relaxed_Initialization variable used in aggregate

[faelys]

Hello,

I hope I'm not too much of a bother by reporting the bug here rather than the usual e-mail address. Hopefully SPARK community 2020 is young enough to still have this issue.

I get a bugbox when using a variable with Relaxed_Initialization in an aggregate, like in the example below:

procedure Toy1 with Spark_Mode is
   subtype Data_Size is Natural range 0 .. 256;
   type Data (Size : Data_Size := 0) is record
      Str : String (1 .. Size);
   end record;
   type Message is record
      Number : Natural;
      Payload : Data;
   end record;

   M : Message;
   P : Data (20) with Relaxed_Initialization;
begin
   for I in 1 .. 20 loop
      P.Str (I) := Character'Val (64 + I);
   end loop;

   M := (Number => 3,
         Payload => P);
end Toy1;

Removing Relaxed_Initialization works, but then the correct initialization of P.Str is not proved.

A workaround is to add an extra variable of type Data (20) without Relaxed_Initialization, assigned to P before the last assignment, and using that variable instead of P in the aggregate assigned to M.

In case it helps, here are the invocation and the bugbox:

% time gnatprove -Pspark -j0 --mode=all -u toy1.adb              
Phase 1 of 2: generation of Global contracts ...                               
Phase 2 of 2: flow analysis and proof ...                                      
+===========================GNAT BUG DETECTED==============================+   
| Community 2020 (20200429) (spark) Storage_Error s-intman.adb:136 explicit raise|
| Error detected at toy1.adb:18:6                                          |
| Please submit a bug report by email to report@adacore.com.               |
| GAP members can alternatively use GNAT Tracker:                          |
| https://www.adacore.com/login?mode=gap section 'Create New Ticket'.      |
| See gnatinfo.txt for full info on procedure for submitting bugs.         |
| Use a subject line meaningful to you and us to track the bug.            |
| Include the entire contents of this bug box in the report.               |
| Include the exact command that you entered.                              |
| Also include sources listed below.                                       |
| Use plain ASCII or MIME attachment(s).                                   |
+==========================================================================+

[kanigsson]

Thanks for the reproducer, we can reproduce the issue and we will look at it.

[clairedross]

This is now fixed in the development version of SPARK. Thanks again for the reproducer.