diff --git a/experiments/golden-results/SPARK-tetris-summary.txt b/experiments/golden-results/SPARK-tetris-summary.txt index f31925fff..ee00c4729 100644 --- a/experiments/golden-results/SPARK-tetris-summary.txt +++ b/experiments/golden-results/SPARK-tetris-summary.txt @@ -15,5 +15,5 @@ Raw compiler error message: -- Occurs: 5 times +===========================GNAT BUG DETECTED==============================+ -| GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map| +| GNU Ada (ada2goto) Assert_Failure failed postcondition from arrays.ads:52| Error detected at REDACTED diff --git a/experiments/golden-results/StratoX-summary.txt b/experiments/golden-results/StratoX-summary.txt index 2abf73851..788f5e5b9 100644 --- a/experiments/golden-results/StratoX-summary.txt +++ b/experiments/golden-results/StratoX-summary.txt @@ -59,15 +59,15 @@ Error message: Unsupported pragma: Check Nkind: N_Pragma -- Occurs: 8 times -Calling function: Process_Pragma_Declaration -Error message: Unsupported pragma: Obsolescent -Nkind: N_Pragma --- -Occurs: 7 times Calling function: Do_Type_Reference Error message: Type of type not a type Nkind: N_Defining_Identifier -- +Occurs: 8 times +Calling function: Process_Pragma_Declaration +Error message: Unsupported pragma: Obsolescent +Nkind: N_Pragma +-- Occurs: 6 times Calling function: Process_Declaration Error message: Use type clause declaration @@ -108,6 +108,11 @@ Calling function: Do_Itype_Definition Error message: Unknown Ekind Nkind: N_Defining_Identifier -- +Occurs: 2 times +Calling function: Do_Itype_Integer_Subtype +Error message: Non-literal bound unsupported +Nkind: N_Defining_Identifier +-- Occurs: 1 times Calling function: Do_Base_Range_Constraint Error message: unsupported lower range kind @@ -134,11 +139,6 @@ Error message: function entity not defining identifier Nkind: N_Defining_Operator_Symbol -- Occurs: 1 times -Calling function: Do_Itype_Integer_Subtype -Error message: Non-literal bound unsupported -Nkind: N_Defining_Identifier --- -Occurs: 1 times Calling function: Do_Op_Expon Error message: Exponentiation unhandled for non mod types at the moment Nkind: N_Op_Expon @@ -1718,7 +1718,7 @@ Occurs: 10 times | GNU Ada (ada2goto) Assert_Failure sinfo.adb:495 | Error detected at REDACTED -- -Occurs: 9 times +Occurs: 8 times +===========================GNAT BUG DETECTED==============================+ | GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map| Error detected at REDACTED diff --git a/experiments/golden-results/muen-summary.txt b/experiments/golden-results/muen-summary.txt index a61ba13be..c9e5130cb 100644 --- a/experiments/golden-results/muen-summary.txt +++ b/experiments/golden-results/muen-summary.txt @@ -1,4 +1,4 @@ -Occurs: 160 times +Occurs: 161 times Calling function: Process_Declaration Error message: Use type clause declaration Nkind: N_Use_Type_Clause @@ -38,11 +38,21 @@ Calling function: Process_Pragma_Declaration Error message: Unsupported pragma: Precondition Nkind: N_Pragma -- -Occurs: 6 times +Occurs: 7 times Calling function: Do_Type_Reference Error message: Type of type not a type Nkind: N_Defining_Identifier -- +Occurs: 5 times +Calling function: Do_Itype_Integer_Subtype +Error message: Non-literal bound unsupported +Nkind: N_Defining_Identifier +-- +Occurs: 5 times +Calling function: Process_Pragma_Declaration +Error message: Unsupported pragma: Postcondition +Nkind: N_Pragma +-- Occurs: 4 times Calling function: Do_Expression Error message: First of string unsupported @@ -53,16 +63,16 @@ Calling function: Do_Full_Type_Declaration Error message: type not in symbol table after declaration Nkind: N_Full_Type_Declaration -- -Occurs: 4 times -Calling function: Do_Itype_Integer_Subtype -Error message: Non-literal bound unsupported -Nkind: N_Defining_Identifier --- Occurs: 3 times Calling function: Do_Private_Type_Declaration Error message: Tagged type declaration unsupported Nkind: N_Private_Type_Declaration -- +Occurs: 3 times +Calling function: Process_Statement +Error message: Unknown expression kind +Nkind: N_Object_Renaming_Declaration +-- Occurs: 2 times Calling function: Do_Aggregate_Literal Error message: Unhandled aggregate kind: E_PRIVATE_TYPE @@ -83,11 +93,6 @@ Calling function: Process_Pragma_Declaration Error message: Unsupported pragma: Check Nkind: N_Pragma -- -Occurs: 2 times -Calling function: Process_Statement -Error message: Unknown expression kind -Nkind: N_Object_Renaming_Declaration --- Occurs: 1 times Calling function: Do_Aggregate_Literal Error message: Unhandled aggregate kind: E_RECORD_TYPE_WITH_PRIVATE @@ -113,11 +118,6 @@ Calling function: Do_Op_Expon Error message: Exponentiation unhandled for non mod types at the moment Nkind: N_Op_Expon -- -Occurs: 1 times -Calling function: Process_Pragma_Declaration -Error message: Unsupported pragma: Postcondition -Nkind: N_Pragma --- Occurs: 291 times Redacted compiler error message: violation of restriction "REDACTED" @@ -2968,14 +2968,14 @@ Occurs: 12 times | GNU Ada (ada2goto) Assert_Failure sinfo.adb:495 | Error detected at REDACTED -- -Occurs: 6 times +Occurs: 3 times +===========================GNAT BUG DETECTED==============================+ -| GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map| +| GNU Ada (ada2goto) Assert_Failure failed precondition from goto_utils.ads:147| Error detected at REDACTED -- Occurs: 3 times +===========================GNAT BUG DETECTED==============================+ -| GNU Ada (ada2goto) Assert_Failure failed precondition from goto_utils.ads:147| +| GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map| Error detected at REDACTED -- Occurs: 2 times @@ -2983,9 +2983,9 @@ Occurs: 2 times | GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784| Error detected at REDACTED -- -Occurs: 1 times +Occurs: 2 times +===========================GNAT BUG DETECTED==============================+ -| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784| +| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 | Error detected at REDACTED -- Occurs: 1 times @@ -3180,22 +3180,22 @@ Error detected at REDACTED -- Occurs: 1 times +===========================GNAT BUG DETECTED==============================+ -| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106| +| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784| Error detected at REDACTED -- Occurs: 1 times +===========================GNAT BUG DETECTED==============================+ -| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 | +| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106| Error detected at REDACTED -- Occurs: 1 times +===========================GNAT BUG DETECTED==============================+ -| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 | +| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 | Error detected at REDACTED -- Occurs: 1 times +===========================GNAT BUG DETECTED==============================+ -| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 | +| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 | Error detected at REDACTED -- Occurs: 1 times diff --git a/gnat2goto/driver/gnat2goto_itypes.adb b/gnat2goto/driver/gnat2goto_itypes.adb index 0aa541632..9f7f55604 100644 --- a/gnat2goto/driver/gnat2goto_itypes.adb +++ b/gnat2goto/driver/gnat2goto_itypes.adb @@ -7,6 +7,7 @@ with Range_Check; use Range_Check; with Symbol_Table_Info; use Symbol_Table_Info; with Tree_Walk; use Tree_Walk; with Follow; use Follow; +with Arrays; use Arrays; package body Gnat2goto_Itypes is @@ -84,6 +85,7 @@ package body Gnat2goto_Itypes is -- might become the only way to get a type definition. return (case Ekind (N) is when E_Array_Subtype => Do_Itype_Array_Subtype (N), + when E_Array_Type => Do_Itype_Array_Type (N), when E_String_Literal_Subtype => Do_Itype_String_Literal_Subtype (N), when E_Signed_Integer_Subtype => Do_Itype_Integer_Subtype (N), when E_Record_Subtype => Do_Itype_Record_Subtype (N), @@ -96,13 +98,36 @@ package body Gnat2goto_Itypes is "Unknown Ekind")); end Do_Itype_Definition; + ---------------------------- + -- Do_Itype_Array_Type -- + ---------------------------- + + function Do_Itype_Array_Type (E : Entity_Id) return Irep is + Var : constant Node_Id := + Object_Definition (Associated_Node_For_Itype (E)); + begin + case Nkind (Var) is + when N_Constrained_Array_Definition => + return Do_Constrained_Array_Definition (Var); + when N_Unconstrained_Array_Definition => + return Do_Unconstrained_Array_Definition (Var); + when others => + return Report_Unhandled_Node_Irep + (E, "Do_Itype_Array_Type", + "Unknown array type " & Node_Kind'Image (Nkind (Var))); + end case; + end Do_Itype_Array_Type; + ---------------------------- -- Do_Itype_Array_Subtype -- ---------------------------- function Do_Itype_Array_Subtype (N : Node_Id) return Irep is - (Make_Symbol_Type - (Identifier => Unique_Name (Etype (N)))); + begin + Declare_Itype (Etype (N)); + return Make_Symbol_Type + (Identifier => Unique_Name (Etype (N))); + end Do_Itype_Array_Subtype; ------------------------------------- -- Do_Itype_String_Literal_Subtype -- diff --git a/gnat2goto/driver/gnat2goto_itypes.ads b/gnat2goto/driver/gnat2goto_itypes.ads index cb484d75c..6d67b8216 100644 --- a/gnat2goto/driver/gnat2goto_itypes.ads +++ b/gnat2goto/driver/gnat2goto_itypes.ads @@ -33,4 +33,7 @@ private function Do_Modular_Integer_Subtype (N : Entity_Id) return Irep with Pre => Is_Itype (N) and then Ekind (N) = E_Modular_Integer_Subtype; + function Do_Itype_Array_Type (E : Entity_Id) return Irep + with Pre => Is_Itype (E) and Ekind (E) = E_Array_Type; + end Gnat2goto_Itypes; diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index fb095ef2c..13be156c3 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -5118,6 +5118,7 @@ package body Tree_Walk is (if Ekind (E) = E_Access_Subtype then Etype (E) else E); Type_Id : constant Symbol_Id := Intern (Type_Name); begin + Declare_Itype (E); if Global_Symbol_Table.Contains (Type_Id) then if Kind (Global_Symbol_Table.Element (Type_Id).SymType) in Class_Type then diff --git a/testsuite/gnat2goto/tests/arrays_declaration_failure1/arrays_declaration_failure1.adb b/testsuite/gnat2goto/tests/arrays_declaration_failure1/arrays_declaration_failure1.adb index 80813e6ed..6b59e1792 100644 --- a/testsuite/gnat2goto/tests/arrays_declaration_failure1/arrays_declaration_failure1.adb +++ b/testsuite/gnat2goto/tests/arrays_declaration_failure1/arrays_declaration_failure1.adb @@ -1,10 +1,12 @@ -- see also test "arrays_multidimensional_declaration_failure1" procedure Arrays_Declaration_Failure1 is - -- ERROR, "GNAT BUG DETECTED" " GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map|" A1 : Array (1..3) of Integer; - -- ERROR, "GNAT BUG DETECTED" " GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map|" A2 : Array (1..3) of Integer := (1,2,3); begin - null; + A1 (1) := 1; + pragma Assert (A1 (1) = 1); + pragma Assert (A1 (1) = 10); + pragma Assert (A2 (1) = 1); + pragma Assert (A2 (1) = 2); end Arrays_Declaration_Failure1; diff --git a/testsuite/gnat2goto/tests/arrays_declaration_failure1/test.opt b/testsuite/gnat2goto/tests/arrays_declaration_failure1/test.opt deleted file mode 100644 index 4458c6919..000000000 --- a/testsuite/gnat2goto/tests/arrays_declaration_failure1/test.opt +++ /dev/null @@ -1 +0,0 @@ -ALL XFAIL gnat2goto fails with "GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map" diff --git a/testsuite/gnat2goto/tests/arrays_declaration_failure1/test.out b/testsuite/gnat2goto/tests/arrays_declaration_failure1/test.out new file mode 100644 index 000000000..53af4fb7a --- /dev/null +++ b/testsuite/gnat2goto/tests/arrays_declaration_failure1/test.out @@ -0,0 +1,9 @@ +[precondition_instance.1] file memcpy src/dst overlap: SUCCESS +[precondition_instance.2] file memcpy source region readable: SUCCESS +[precondition_instance.3] file memcpy destination region writeable: SUCCESS +[arrays_declaration_failure1.assertion.1] line 7 Ada Check assertion: SUCCESS +[arrays_declaration_failure1.assertion.2] line 8 assertion A1 (1) = 1: SUCCESS +[arrays_declaration_failure1.assertion.3] line 9 assertion A1 (1) = 10: FAILURE +[arrays_declaration_failure1.assertion.4] line 10 assertion A2 (1) = 1: SUCCESS +[arrays_declaration_failure1.assertion.5] line 11 assertion A2 (1) = 2: FAILURE +VERIFICATION FAILED diff --git a/testsuite/gnat2goto/tests/arrays_declaration_failure2/arrays_declaration_failure2.adb b/testsuite/gnat2goto/tests/arrays_declaration_failure2/arrays_declaration_failure2.adb index 37422afe3..c9eed6abd 100644 --- a/testsuite/gnat2goto/tests/arrays_declaration_failure2/arrays_declaration_failure2.adb +++ b/testsuite/gnat2goto/tests/arrays_declaration_failure2/arrays_declaration_failure2.adb @@ -1,7 +1,8 @@ -- see also test "arrays_multidimensional_declaration_failure2" procedure Arrays_Declaration_Failure2 is - -- ERROR, "GNAT BUG DETECTED" "GNU Ada (ada2goto) Assert_Failure sinfo.adb:2232" A1 : array (Integer range 1..3) of Integer; begin - null; + A1 (1) := 10; + pragma Assert (A1 (1) = 10); + pragma Assert (A1 (1) = 20); end Arrays_Declaration_Failure2; diff --git a/testsuite/gnat2goto/tests/arrays_declaration_failure2/test.opt b/testsuite/gnat2goto/tests/arrays_declaration_failure2/test.opt deleted file mode 100644 index ca49cc86e..000000000 --- a/testsuite/gnat2goto/tests/arrays_declaration_failure2/test.opt +++ /dev/null @@ -1 +0,0 @@ -ALL XFAIL gnat2goto fails with "GNU Ada (ada2goto) Assert_Failure sinfo.adb:2232" diff --git a/testsuite/gnat2goto/tests/arrays_declaration_failure2/test.out b/testsuite/gnat2goto/tests/arrays_declaration_failure2/test.out new file mode 100644 index 000000000..cca220e9c --- /dev/null +++ b/testsuite/gnat2goto/tests/arrays_declaration_failure2/test.out @@ -0,0 +1,4 @@ +[arrays_declaration_failure2.assertion.1] line 5 Ada Check assertion: SUCCESS +[arrays_declaration_failure2.assertion.2] line 6 assertion A1 (1) = 10: SUCCESS +[arrays_declaration_failure2.assertion.3] line 7 assertion A1 (1) = 20: FAILURE +VERIFICATION FAILED diff --git a/testsuite/gnat2goto/tests/arrays_multidimensional_declaration_failure1/test.opt b/testsuite/gnat2goto/tests/arrays_multidimensional_declaration_failure1/test.opt index 4458c6919..c7f5ea13c 100644 --- a/testsuite/gnat2goto/tests/arrays_multidimensional_declaration_failure1/test.opt +++ b/testsuite/gnat2goto/tests/arrays_multidimensional_declaration_failure1/test.opt @@ -1 +1 @@ -ALL XFAIL gnat2goto fails with "GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map" +ALL XFAIL GNU Ada (ada2goto) Assert_Failure failed postcondition from arrays.ads diff --git a/testsuite/gnat2goto/tests/function_pointer/test.out b/testsuite/gnat2goto/tests/function_pointer/test.out index 9f14042dd..b2daf96d0 100644 --- a/testsuite/gnat2goto/tests/function_pointer/test.out +++ b/testsuite/gnat2goto/tests/function_pointer/test.out @@ -1,2 +1,25 @@ +Standard_Output from gnat2goto test: +----------At: Do_Itype_Definition---------- +----------Unknown Ekind---------- +N_Defining_Identifier "T6b" (Entity_Id=2491) + Parent = + Sloc = 8480 test.adb:13:4 + Chars = "T6b" (Name_Id=300001463) + Next_Entity = N_Defining_Identifier "assert_compare" (Entity_Id=2476) + Scope = N_Defining_Identifier "test" (Entity_Id=2245) + Ekind = E_Access_Subtype + Etype = N_Defining_Identifier "comparator" (Entity_Id=2304) + Associated_Node_For_Itype = N_Procedure_Specification (Node_Id=2473) + Esize = 64 (Uint = 600032832) + RM_Size = 64 (Uint = 600032832) + Alignment = 4 (Uint = 600032772) + Directly_Designated_Type = N_Defining_Identifier "T3b" (Entity_Id=2451) + Can_Never_Be_Null = True + Has_Qualified_Name = True + Is_Frozen = True + Is_Internal = True + Is_Itype = True + Size_Known_At_Compile_Time = True + [assert_compare.assertion.1] line 15 assertion Func.all(5): FAILURE VERIFICATION FAILED diff --git a/testsuite/gnat2goto/tests/procedure_pointer/test.out b/testsuite/gnat2goto/tests/procedure_pointer/test.out index 2a36440cc..1c4f300a1 100644 --- a/testsuite/gnat2goto/tests/procedure_pointer/test.out +++ b/testsuite/gnat2goto/tests/procedure_pointer/test.out @@ -1,3 +1,26 @@ +Standard_Output from gnat2goto test: +----------At: Do_Itype_Definition---------- +----------Unknown Ekind---------- +N_Defining_Identifier "T4b" (Entity_Id=2491) + Parent = + Sloc = 8525 test.adb:14:4 + Chars = "T4b" (Name_Id=300001462) + Next_Entity = N_Defining_Identifier "assert_modify" (Entity_Id=2476) + Scope = N_Defining_Identifier "test" (Entity_Id=2245) + Ekind = E_Access_Subtype + Etype = N_Defining_Identifier "modifier" (Entity_Id=2315) + Associated_Node_For_Itype = N_Procedure_Specification (Node_Id=2473) + Esize = 64 (Uint = 600032832) + RM_Size = 64 (Uint = 600032832) + Alignment = 4 (Uint = 600032772) + Directly_Designated_Type = N_Defining_Identifier "T1b" (Entity_Id=2451) + Can_Never_Be_Null = True + Has_Qualified_Name = True + Is_Frozen = True + Is_Internal = True + Is_Itype = True + Size_Known_At_Compile_Time = True + [assert_modify.assertion.1] line 17 assertion Global_Number = 5: FAILURE [increment_by.assertion.1] line 5 Ada Check assertion: SUCCESS VERIFICATION FAILED