[feature] Allow use of discriminants of unchecked unions in non-executable ghost code

[clairedross]

Summary

We want it to be possible to mention the discriminants of record type with the Unchecked_Union aspect inside ghost code whose assertion level depends on Static. The syntax and semantics would be exactly the same as for other references to discriminants. The fact that the discriminant is not represented in practice is not a problem as the code cannot be enabled at runtime.

It would also be interesting to state that the expected semantics of predefined equality on Unchecked_Union types is not to raise Program_Error when called inside such a context. It does not change much for execution, as this will never be executed, but it has an impact for static analysis.

   type My_Rec (Is_Int : Boolean := False) is record
      case Is_Int is
         when True =>
            F_Int : Integer;
         when False =>
            F_Float : Float;
      end case;
   end record with
     Unchecked_Union;
   
   function Read_F_Int (X : My_Rec) return Integer with
     Pre => (Static => X.Is_Int);
   
   function Read_F_Int (X : My_Rec) return Integer is (X.F_Int);
   
   procedure Write_F_Int_If_B (X : in out My_Rec; B : Boolean) with
     Post => (Static => (if B then X = (True, 12) else X = X'Old));
   
   procedure Write_F_Int_If_B (X : in out My_Rec; B : Boolean) is
   begin
      if B then
         X := (True, 12);
      end if;
   end Write_F_Int_If_B;

Motivation

Unchecked unions are currently badly handled in SPARK. As per Ada semantics, it is necessary to track the value of the discriminants of such objects, as the fields should only be accessed when the discriminants allow it. However, as these discriminants do not actually occur in the object, they cannot be mentioned. This is a major issue because it prevents users from writing contracts that mention them. As a result, it is not possible to have a verified subprogram that accesses a component of an object of an unchecked union type that it takes as a parameter or accesses globally.

Caveats and alternatives

This actually changes the semantics of Ada, at least inside non-executable contracts.

[sttaft]

Caveats and alternatives
This actually changes the semantics of Ada, at least inside non-executable contracts.

That seems OK, since SPARK does several things at analysis time that Ada does not do. Also, from a practical manner, Ada doesn't have the notion of a Static "level" in a pre/postcondition (though seems worth considering), so these references would not be "seen" by standard Ada compilers.