Declare implicit array types #335
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,10 +1,12 @@ | ||
| -- see also test "arrays_multidimensional_declaration_failure1" | ||
| procedure Arrays_Declaration_Failure1 is | ||
| A1 : Array (1..3) of Integer; | ||
|
|
||
| A2 : Array (1..3) of Integer := (1,2,3); | ||
| begin | ||
| 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; |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,9 @@ | ||
| [precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS | ||
| [precondition_instance.2] file <internal> memcpy source region readable: SUCCESS | ||
| [precondition_instance.3] file <internal> 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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,7 +1,8 @@ | ||
| -- see also test "arrays_multidimensional_declaration_failure2" | ||
| procedure Arrays_Declaration_Failure2 is | ||
| A1 : array (Integer range 1..3) of Integer; | ||
| begin | ||
| A1 (1) := 10; | ||
| pragma Assert (A1 (1) = 10); | ||
| pragma Assert (A1 (1) = 20); | ||
| end Arrays_Declaration_Failure2; |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1 +1 @@ | ||
| ALL XFAIL GNU Ada (ada2goto) Assert_Failure failed postcondition from arrays.ads |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,2 +1,25 @@ | ||
| Standard_Output from gnat2goto test: | ||
|
Contributor
There was a problem hiding this comment. What's going on with these two tests? This looks like the tests are now producing missing feature reports which they were not before.... Were this test and procedure_pointer both passing before this change?
Contributor
There was a problem hiding this comment. It’s basically just Itypes that we never supported, but we just “happened” to pass these tests without missing feature reports or crashes because we don’t actually use these types anywhere in the resulting goto program. I.e. as a side effect of some of the changes we’ve made in this PR some things that didn’t work before now visibly don’t work.
Contributor
There was a problem hiding this comment. OK. There's recently been some debate on #327 about whether we should or should not add "missing feature" reports to expected outputs - I'm not sure we came to a conclusion. In this case, it's probably better to accept it in the expected output and keep the test passing, rather than turn a passing test into an xfail. |
||
| ----------At: Do_Itype_Definition---------- | ||
| ----------Unknown Ekind---------- | ||
| N_Defining_Identifier "T6b" (Entity_Id=2491) | ||
| Parent = <empty> | ||
| 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 | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,3 +1,26 @@ | ||
| Standard_Output from gnat2goto test: | ||
| ----------At: Do_Itype_Definition---------- | ||
| ----------Unknown Ekind---------- | ||
| N_Defining_Identifier "T4b" (Entity_Id=2491) | ||
| Parent = <empty> | ||
| 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 |
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Most of the golden results changes appear to be just things moving around for some weird reason. Very few actual changes.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That looks like a move, but actually its because "Do_Type_Reference" went from 7 -> 8 times...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@chrisr-diffblue Yes, I believe this is because some of the nodes that we now handle were not handled before. This means that some nodes in these projects now propagate, and they might result into some previously unreported errors showing up.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@chrisr-diffblue Keep in mind that the changes made in this PR cause gnat2goto to not crash in some circumstances where it would’ve crashed before, so it’s producing more output and potentially some additional missing but unrelated features as well.