diff --git a/experiments/golden-results/UKNI-Information-Barrier-summary.txt b/experiments/golden-results/UKNI-Information-Barrier-summary.txt index 6b7d237a7..e5435d8db 100644 --- a/experiments/golden-results/UKNI-Information-Barrier-summary.txt +++ b/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" diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index b1f155fe7..d020c0ca9 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/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 diff --git a/testsuite/gnat2goto/tests/address_clause/address_clause.adb b/testsuite/gnat2goto/tests/address_clause/address_clause.adb new file mode 100644 index 000000000..cf3ee727d --- /dev/null +++ b/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; diff --git a/testsuite/gnat2goto/tests/address_clause/test.out b/testsuite/gnat2goto/tests/address_clause/test.out new file mode 100644 index 000000000..f698fa58e --- /dev/null +++ b/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 diff --git a/testsuite/gnat2goto/tests/address_clause/test.py b/testsuite/gnat2goto/tests/address_clause/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/address_clause/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/size_integer_and_objects/check_size.adb b/testsuite/gnat2goto/tests/size_integer_and_objects/check_size.adb new file mode 100644 index 000000000..9a70b2b0b --- /dev/null +++ b/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; diff --git a/testsuite/gnat2goto/tests/size_integer_and_objects/test.opt b/testsuite/gnat2goto/tests/size_integer_and_objects/test.opt new file mode 100644 index 000000000..eff20f6ec --- /dev/null +++ b/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. \ No newline at end of file diff --git a/testsuite/gnat2goto/tests/size_integer_and_objects/test.out b/testsuite/gnat2goto/tests/size_integer_and_objects/test.out new file mode 100644 index 000000000..bb8f6db13 --- /dev/null +++ b/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 diff --git a/testsuite/gnat2goto/tests/size_integer_and_objects/test.py b/testsuite/gnat2goto/tests/size_integer_and_objects/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/size_integer_and_objects/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/size_mod_type/check_size_mod.adb b/testsuite/gnat2goto/tests/size_mod_type/check_size_mod.adb new file mode 100644 index 000000000..1b6ac2907 --- /dev/null +++ b/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; diff --git a/testsuite/gnat2goto/tests/size_mod_type/test.out b/testsuite/gnat2goto/tests/size_mod_type/test.out new file mode 100644 index 000000000..9ca6c9427 --- /dev/null +++ b/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 diff --git a/testsuite/gnat2goto/tests/size_mod_type/test.py b/testsuite/gnat2goto/tests/size_mod_type/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/size_mod_type/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove()