Address clause

experiments/golden-results/UKNI-Information-Barrier-summary.txt

@@ -3,16 +3,26 @@ Calling function: Do_Expression
 Error message: Unknown expression kind
 Nkind: N_Expanded_Name
 --
+Occurs: 42 times
+Calling function: Process_Declaration
+Error message: Address representation clauses are not currently supported
+Nkind: N_Attribute_Definition_Clause
+--
 Occurs: 20 times
 Calling function: Do_Expression
 Error message: In
 Nkind: N_In
 --
-Occurs: 15 times
+Occurs: 19 times
 Calling function: Do_While_Statement
 Error message: Wrong Nkind spec
 Nkind: N_Loop_Statement
 --
+Occurs: 4 times
+Calling function: Process_Statement
+Error message: Unknown expression kind
+Nkind: N_Object_Declaration
+--
 Occurs: 3 times
 Calling function: Do_Base_Range_Constraint
 Error message: unsupported upper range kind
@@ -43,6 +53,16 @@ Calling function: Do_Expression
 Error message: Unknown expression kind
 Nkind: N_Range
 --
+Occurs: 1 times
+Calling function: Do_Operator_General
+Error message: Mod of unsupported type
+Nkind: N_Op_Not
+--
+Occurs: 1 times
+Calling function: Process_Declaration
+Error message: Use package clause declaration
+Nkind: N_Use_Package_Clause
+--
 Occurs: 5 times
 Redacted compiler error message:
 "REDACTED" not declared in "REDACTED"

gnat2goto/driver/tree_walk.adb

@@ -1,6 +1,7 @@
 with Namet;                 use Namet;
 with Nlists;                use Nlists;
 with Sem;
+with Sem_Eval;              use Sem_Eval;
 with Sem_Util;              use Sem_Util;
 with Sem_Aux;               use Sem_Aux;
 with Snames;                use Snames;
@@ -4644,51 +4645,70 @@ package body Tree_Walk is
       procedure Handle_Representation_Clause (N : Node_Id);
       procedure Handle_Representation_Clause (N : Node_Id) is
          Attr_Id : constant String := Get_Name_String (Chars (N));
-         Target_Name : constant Irep := Do_Identifier (Name (N));
-         Entity_Esize : constant Uint := Esize (Entity (N));
-         Target_Type_Irep : constant Irep :=
-           Follow_Symbol_Type (Get_Type (Target_Name), Global_Symbol_Table);
-         Expression_Value : constant Uint := Intval (Expression (N));
       begin
-         pragma Assert (Kind (Target_Type_Irep) in Class_Type);
-         if Attr_Id = "size" then
-
-            --  Just check that the front-end already applied this size
-            --  clause, i .e. that the size of type-irep we already had
-            --  equals the entity type this clause is applied to (and the
-            --  size specified in this clause).
-            pragma Assert (Entity_Esize =
-                             UI_From_Int (Int (Get_Width (Target_Type_Irep)))
-                           and Entity_Esize = Expression_Value);
+         --  First check if it is an address clause which gnat2goto does not
+         --  currently handle
+         if Attr_Id = "address" then
+            Report_Unhandled_Node_Empty
+              (N, "Process_Declaration",
+               "Address representation clauses are not currently supported");
             return;
-         elsif Attr_Id = "component_size" then
-            if not Is_Array_Type (Entity (N)) then
-               Report_Unhandled_Node_Empty (N, "Process_Declaration",
-                              "Component size only supported for array types");
-               return;
-            end if;
+         elsif Attr_Id = "size" or else Attr_Id = "component_size" then
             declare
-               Array_Data : constant Irep :=
-                 Get_Data_Component_From_Type (Target_Type_Irep);
-               Target_Subtype : constant Irep :=
-                 Follow_Symbol_Type (Get_Subtype (Get_Type (Array_Data)),
-                                     Global_Symbol_Table);
-               Target_Subtype_Width : constant Uint :=
-                 UI_From_Int (Int (Get_Width (Target_Subtype)));
+               Target_Name : constant Irep := Do_Identifier (Name (N));
+               Entity_Esize : constant Uint := Esize (Entity (N));
+               Target_Type_Irep : constant Irep :=
+                 Follow_Symbol_Type
+                   (Get_Type (Target_Name), Global_Symbol_Table);
+               Expression_Value : constant Uint := Expr_Value (Expression (N));
             begin
-               if Component_Size (Entity (N)) /= Expression_Value or
-                 Target_Subtype_Width /= Expression_Value
-               then
-                  Report_Unhandled_Node_Empty (N, "Process_Declaration",
-                      "Having component sizes be different from the size of " &
-                      "their underlying type is currently not supported");
+               pragma Assert (Kind (Target_Type_Irep) in Class_Type);
+               if Attr_Id = "size" then
+
+                  --  Just check that the front-end already applied this size
+                  --  clause, i .e. that the size of type-irep we already had
+                  --  equals the entity type this clause is applied to (and the
+                  --  size specified in this clause).
+                  pragma Assert
+                    (Entity_Esize =
+                       UI_From_Int (Int (Get_Width (Target_Type_Irep)))
+                     and Entity_Esize = Expression_Value);
+                  return;
+               elsif Attr_Id = "component_size" then
+                  if not Is_Array_Type (Entity (N)) then
+                     Report_Unhandled_Node_Empty
+                       (N, "Process_Declaration",
+                        "Component size only supported for array types");
+                     return;
+                  end if;
+                  declare
+                     Array_Data : constant Irep :=
+                       Get_Data_Component_From_Type (Target_Type_Irep);
+                     Target_Subtype : constant Irep :=
+                       Follow_Symbol_Type (Get_Subtype (Get_Type (Array_Data)),
+                                           Global_Symbol_Table);
+                     Target_Subtype_Width : constant Uint :=
+                       UI_From_Int (Int (Get_Width (Target_Subtype)));
+                  begin
+                     if Component_Size (Entity (N)) /= Expression_Value or
+                       Target_Subtype_Width /= Expression_Value
+                     then
+                        Report_Unhandled_Node_Empty
+                          (N, "Process_Declaration",
+                           "Having component sizes be different from the "
+                           & "size of their underlying type "
+                           & "is currently not supported");
+                     end if;
+                  end;
+                  return;
                end if;
             end;
-            return;
          end if;
 
-         Report_Unhandled_Node_Empty (N, "Process_Declaration",
-                              "Representation clause unsupported: " & Attr_Id);
+         Report_Unhandled_Node_Empty
+           (N, "Process_Declaration",
+            "Representation clause unsupported: " & Attr_Id);
+
       end Handle_Representation_Clause;
 
    begin

testsuite/gnat2goto/tests/address_clause/address_clause.adb

@@ -0,0 +1,13 @@
+with System; use System;
+with System.Storage_Elements;
+procedure Address_Clause is
+   Var_Addr_1 : Integer;
+   for Var_Addr_1'Address use System'To_Address (16#6F#);
+
+   Var_Addr_2 : Integer;
+   for Var_Addr_2'Address use System.Storage_Elements.To_Address (16#80#);
+begin
+   Var_Addr_1 := 1;
+   Var_Addr_2 := 2;
+   pragma Assert (Var_Addr_1 + Var_Addr_2 = 3);
+end Address_Clause;

testsuite/gnat2goto/tests/address_clause/test.out

@@ -0,0 +1,24 @@
+Standard_Output from gnat2goto address_clause:
+N_Attribute_Definition_Clause "address" (Node_Id=2277) (source,analyzed)
+ Sloc = 8303  address_clause.adb:5:4
+ Chars = "address" (Name_Id=300000791)
+ Name = N_Identifier "var_addr_1" (Node_Id=2274)
+ Expression = N_Function_Call (Node_Id=2280)
+ Entity = N_Defining_Identifier "var_addr_1" (Entity_Id=2264)
+ Check_Address_Alignment = True
+N_Attribute_Definition_Clause "address" (Node_Id=2295) (source,analyzed)
+ Sloc = 8387  address_clause.adb:8:4
+ Chars = "address" (Name_Id=300000791)
+ Name = N_Identifier "var_addr_2" (Node_Id=2292)
+ Expression = N_Function_Call (Node_Id=2302)
+ Entity = N_Defining_Identifier "var_addr_2" (Entity_Id=2282)
+ Check_Address_Alignment = True
+
+Standard_Error from gnat2goto address_clause:
+----------At: Process_Declaration----------
+----------Address representation clauses are not currently supported----------
+----------At: Process_Declaration----------
+----------Address representation clauses are not currently supported----------
+
+[1] file address_clause.adb line 12 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/address_clause/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()

testsuite/gnat2goto/tests/size_integer_and_objects/check_size.adb

@@ -0,0 +1,38 @@
+procedure Check_Size is
+   Size_1 : constant := -23 + 31;
+   Size_2 : constant Integer := 35 - 3;
+   Size_3 : constant := 2 * Size_1;
+
+   type T_1 is new Integer range 0 .. 47;
+   for T_1'Size use Size_1;
+
+   type T_2 is range 0 .. 2**16 + 1;
+   for T_2'Size use Size_2;
+
+   type Unsigned_8 is mod 2**8;
+   for Unsigned_8'Size use Size_3;
+
+   Var_T_1 : T_1;
+   Var_T_2 : T_2;
+
+   Var_Size_1 : Integer range 0 .. 47;
+   for Var_Size_1'Size use Size_1;
+
+   Var_Size_2 : Integer range 0 .. 2**16 + 1;
+   for Var_Size_2'Size use Size_2;
+
+   Var_U8 : Unsigned_8;
+   for Var_U8'Size use Size_1;
+
+begin
+   Var_T_1 := 30;
+   Var_T_2 := 40;
+   pragma Assert (Integer (Var_T_1) + Integer (Var_T_2) = 70);
+
+   Var_Size_1 := 10;
+   Var_Size_2 := 20;
+   pragma Assert (Var_Size_1 + Var_Size_2 = 30);
+
+   Var_U8 := 255;
+   pragma Assert (Var_U8 + 1 = 0);
+end Check_Size;

testsuite/gnat2goto/tests/size_integer_and_objects/test.opt

@@ -0,0 +1 @@
+ALL XFAIL gnat2goto fails when Size representation clause applied to standard types and their derivations or to objects.

testsuite/gnat2goto/tests/size_integer_and_objects/test.out

@@ -0,0 +1,19 @@
++===========================GNAT BUG DETECTED==============================+
+| GNU Ada (ada2goto) Assert_Failure tree_walk.adb:4673                     |
+| Error detected at check_size.adb:1:11                                    |
+| Please submit a bug report; see https://gcc.gnu.org/bugs/ .              |
+| Use a subject line meaningful to you and us to track the bug.            |
+| Include the entire contents of this bug box in the report.               |
+| Include the exact command that you entered.                              |
+| Also include sources listed below.                                       |
++==========================================================================+
+
+Please include these source files with error report
+Note that list may not be accurate in some cases,
+so please double check that the problem can still
+be reproduced with the set of files listed.
+Consider also -gnatd.n switch (see debug.adb).
+
+check_size.adb
+
+compilation abandoned

testsuite/gnat2goto/tests/size_integer_and_objects/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()

testsuite/gnat2goto/tests/size_mod_type/check_size_mod.adb

@@ -0,0 +1,19 @@
+procedure Check_Size_Mod is
+   S1 : constant := 39 - 7;
+   S2 : constant Integer := -100 + 164;
+
+   type Unsigned_8 is mod 2 ** 8;
+   for Unsigned_8'Size use S1;
+
+   type Unsigned_4 is mod 2 ** 4;
+   for Unsigned_4'Size use S2;
+
+   V1 : Unsigned_8;
+   V2 : Unsigned_4;
+begin
+   V1 := 255;
+   V2 := 15;
+
+   pragma Assert (V1 + 1 = 0);
+   pragma Assert (V2 + 2 = 1);
+end Check_Size_Mod;

testsuite/gnat2goto/tests/size_mod_type/test.out

@@ -0,0 +1,3 @@
+[1] file check_size_mod.adb line 17 assertion: SUCCESS
+[2] file check_size_mod.adb line 18 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/size_mod_type/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()