Re: Recommendation of safe subset of Ada to use?

[onox <denkpadje@gmail.com>]

On Saturday, May 5, 2018 at 11:23:04 PM UTC+2, joak...@kth.se wrote:
> Jere gave the following example in the other thread about how to get Ada across the chasm:
> 
> 1.  Dangling references:  Keeping a reference to an object past its lifetime 
> 
> Ada: 
> *********************************************** 
> with Ada.Text_IO; use Ada.Text_IO; 
> 
> procedure jdoodle is 
>     type Integer_Access is access all Integer; 
>     
>     function Inner(Value : aliased in out Integer) return Integer_Access is 
>     begin 
>         return Value'Access; 
>     end Inner; 
>     
>     function Outer return Integer_Access is 
>         Value : aliased Integer := 0; 
>     begin 
>         return Inner(Value); 
>     end Outer; 
>     
>     Ptr : Integer_Access := Outer;  -- !!! Dangling reference 
> begin 
>     Put_Line("Hello World"); 
> end jdoodle; 
> *********************************************** 
> Hello World 
> 
> gcc -c jdoodle.adb 
> gnatbind -x jdoodle.ali 
> gnatlink jdoodle.ali -o jdoodle 
> 
> It's a 20 line application that demonstrates a dangling pointer in Ada. That's not supposed to be able to happen unless one goes outside of Ada's type system by using Unchecked_Deallocation, Unchecked_Conversion or System.Address_To_Access_Conversion. I've tried the example with the GNAT compiler and it does not detect the issue. I do not believe this is a GNAT bug. Aliased parameters were part of the solution to be able to safely reference elements in containers and thereby avoid unnecessary copying. By making this possible was a hole in Adas type system introduced? It means that one cannot safely use all the features of Ada and be sure of memory safety instead one should stick to a subset of Ada. One subset that comes to mind is SPARK. Another is for example sticking to Ada95 or Ada 2005. Or maybe one should just ban usage of aliased parameters but then what should one do with the standard containers that one probably uses throughout one's application. I am confused. Anybody that can shed light?
> 
> /Joakim

A similar problem happens with anonymous access procedures (GNAT 7.2):

with Ada.Text_IO;

procedure A is
   type Proc_Access is access procedure (P1 : Integer);

   function Inner (Value : access procedure (P2 : Integer)) return Proc_Access is
   begin
      return Value;
   end Inner;

   function Outer (X : Integer) return Proc_Access is
      use Ada.Text_IO;

      procedure Value (Y : Integer) is
      begin
         Put_Line ("X: " & X'Image);  --  random
         Put_Line ("Y: " & Y'Image);  --  2
      end Value;
   begin
      return Inner (Value'Access);
   end Outer;

   Ptr : Proc_Access := Outer (1);
begin
   Ptr (2);
end A;