Skip to content
Snippets Groups Projects
  • Piotr Trojanek's avatar
    2ae98c3a
    [Ada] Propagate null-exclusion to anonymous access types · 2ae98c3a
    Piotr Trojanek authored
    When analyzing an array or record type declaration whose component has a
    constrained access type, e.g.:
    
       type Buffer_Acc is not null access all String;
    
       type Buffer_Rec is record
          Data : Buffer_Acc (1 .. 10);
       end record;
    
       type Buffer_Arr is array (Boolean) of Buffer_Acc (1 .. 10);
    
    we propagated various properties of the unconstrained access type (e.g.
    the designated type, access-to-constant flag), but forgot to propagate
    the null-exclusion.
    
    For GNAT it didn't make a big difference, because the (anonymous)
    component type was never subject to legality checks. The "value
    tracking" optimisation machinery, which also deals with null values,
    only works for entire objects and doesn't care about components.
    However, GNATprove uses this flag when an access-to-component object is
    dereferenced.
    
    gcc/ada/
    
    	* sem_ch3.adb (Constrain_Access): Propagate null-exclusion flag
    	from parent type.
    2ae98c3a
    History
    [Ada] Propagate null-exclusion to anonymous access types
    Piotr Trojanek authored
    When analyzing an array or record type declaration whose component has a
    constrained access type, e.g.:
    
       type Buffer_Acc is not null access all String;
    
       type Buffer_Rec is record
          Data : Buffer_Acc (1 .. 10);
       end record;
    
       type Buffer_Arr is array (Boolean) of Buffer_Acc (1 .. 10);
    
    we propagated various properties of the unconstrained access type (e.g.
    the designated type, access-to-constant flag), but forgot to propagate
    the null-exclusion.
    
    For GNAT it didn't make a big difference, because the (anonymous)
    component type was never subject to legality checks. The "value
    tracking" optimisation machinery, which also deals with null values,
    only works for entire objects and doesn't care about components.
    However, GNATprove uses this flag when an access-to-component object is
    dereferenced.
    
    gcc/ada/
    
    	* sem_ch3.adb (Constrain_Access): Propagate null-exclusion flag
    	from parent type.