Handle component always initialized in precise UC

Author: clairedross

src/why/gnat2why-unchecked_conversion.adb

@@ -647,12 +647,14 @@ package body Gnat2Why.Unchecked_Conversion is
 
  elsif Is_Record_Type (Typ) then
  declare
- Comps : constant Component_Sets.Set := Get_Component_Set (Typ);
- Assocs :
+ Comps : constant Component_Sets.Set :=
+ Get_Component_Set (Typ);
+ Assocs :
  W_Field_Association_Array (1 .. Integer (Comps.Length));
- Flags :
+ Flags  :
  W_Field_Association_Array (1 .. Integer (Comps.Length));
- Index : Positive := 1;
+ Index : Positive := 1;
+ F_Index : Positive := 1;
  begin
  for Comp of Comps loop
  declare
@@ -670,9 +672,12 @@ package body Gnat2Why.Unchecked_Conversion is
  Field =>
  To_Why_Id (Comp, Local => False, Rec => Typ),
  Value => +F_Value.Value);
+ Index := Index + 1;
 
- if Do_Validity then
- Flags (Index) :=
+ if Do_Validity
+ and then not Comp_Has_Only_Valid_Values (Comp, Typ).Ok
+ then
+ Flags (F_Index) :=
  New_Field_Association
  (Domain => EW_Term,
  Field =>
@@ -682,9 +687,9 @@ package body Gnat2Why.Unchecked_Conversion is
  Rec => Base_Retysp (Typ),
  From_Tree => Validity_Tree),
  Value => +F_Value.Valid_Flag);
+ F_Index := F_Index + 1;
  end if;
  end;
- Index := Index + 1;
  end loop;
 
  return
@@ -703,7 +708,7 @@ package body Gnat2Why.Unchecked_Conversion is
  (if Do_Validity
  then
  New_Record_Aggregate
- (Associations => Flags,
+ (Associations => Flags (1 .. F_Index - 1),
  Typ => Get_Validity_Tree_Type (Typ))
  else Why_Empty));
  end;

testsuite/gnatprove/tests/1075__precise_uc_potentially_invalid/ex_zero_byte_parsing_possible.adb

@@ -0,0 +1,40 @@
+with Ada.Unchecked_Conversion;
+procedure Ex_Zero_Byte_Parsing_Possible with SPARK_Mode is
+ type Bit_Array is array (Positive range <>) of Boolean;
+ type T2_Bit_Array is new Bit_Array (1 .. 64) with Pack;
+
+ type T2_Kind_1 is record
+ G1 : Integer;
+ G2 : Natural; -- Might have invalid values
+ end record
+ with Size => 64;
+ for T2_Kind_1 use
+ record
+ G1 at 0 range 0 .. 31;
+ G2 at 0 range 32 .. 63;
+ end record;
+
+ package Model with Ghost is
+ function T2_From_Bytes is new Ada.Unchecked_Conversion
+ (T2_Bit_Array, T2_Kind_1)
+ with Potentially_Invalid;
+
+ function Is_Valid (X : T2_Bit_Array) return Boolean is
+ (T2_From_Bytes (X)'Valid_Scalars);
+ end Model;
+
+ procedure Parse_T2_Kind_1 (X : aliased T2_Bit_Array) with
+ Pre => Model.Is_Valid (X);
+
+ procedure Parse_T2_Kind_1 (X : aliased T2_Bit_Array) is
+ Z : aliased constant T2_Kind_1 with
+ Import,
+ Address => X'Address,
+ Potentially_Invalid;
+ begin
+ pragma Assert (Z.G2'Valid); -- This is not provable yet
+ end Parse_T2_Kind_1;
+
+begin
+ null;
+end;

testsuite/gnatprove/tests/1075__precise_uc_potentially_invalid/test.out

@@ -0,0 +1,11 @@
+ex_zero_byte_parsing_possible.adb:18:16: info: types in unchecked conversion have the same size (Trivial)
+ex_zero_byte_parsing_possible.adb:19:10: info: type is suitable as source for unchecked conversion (Trivial)
+ex_zero_byte_parsing_possible.adb:19:24: info: type is suitable for unchecked conversion (Trivial)
+ex_zero_byte_parsing_possible.adb:22:16: info: implicit aspect Always_Terminates on "Is_Valid" has been proved, subprogram will terminate
+ex_zero_byte_parsing_possible.adb:26:14: warning: subprogram "Parse_T2_Kind_1" has no effect
+ex_zero_byte_parsing_possible.adb:30:07: info: address in address clause is compatible with object alignment (Trivial)
+ex_zero_byte_parsing_possible.adb:30:07: info: object is suitable for aliasing via address clause (Trivial)
+ex_zero_byte_parsing_possible.adb:32:20: info: object is suitable for aliasing via address clause (Trivial)
+ex_zero_byte_parsing_possible.adb:32:20: info: type is suitable as source for unchecked conversion (Trivial)
+ex_zero_byte_parsing_possible.adb:32:20: info: types of aliased objects have the same size (Trivial)
+ex_zero_byte_parsing_possible.adb:35:22: medium: assertion might fail