Recommendation of safe subset of Ada to use?

[joakimds@kth.se]

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