Skip to content

Commit 9ff6cfe

Browse files
martin-csmartin-cs
authored
Merge branch 'master' into translate_withed_units_once_only
2 parents b93e86c + ec134c3 commit 9ff6cfe

File tree

14 files changed

+146
-80
lines changed

14 files changed

+146
-80
lines changed

‎experiments/golden-results/StratoX-summary.txt

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -13,12 +13,7 @@ Calling function: Process_Declaration
1313
Error message: Unknown declaration kind
1414
Nkind: N_Validate_Unchecked_Conversion
1515
--
16-
Occurs: 202 times
17-
Calling function: Process_Pragma_Declaration
18-
Error message: Unsupported pragma: Suppress initialization
19-
Nkind: N_Pragma
20-
--
21-
Occurs: 152 times
16+
Occurs: 153 times
2217
Calling function: Process_Pragma_Declaration
2318
Error message: Unsupported pragma: Postcondition
2419
Nkind: N_Pragma
@@ -184,6 +179,11 @@ Error message: Unsupported pragma: Refine
184179
Nkind: N_Pragma
185180
--
186181
Occurs: 1 times
182+
Calling function: Process_Pragma_Declaration
183+
Error message: Unsupported pragma: Suppress initialization
184+
Nkind: N_Pragma
185+
--
186+
Occurs: 1 times
187187
Calling function: Process_Statement
188188
Error message: Unknown expression kind
189189
Nkind: N_Object_Renaming_Declaration

‎experiments/golden-results/Tokeneer-summary.txt

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,3 @@
1-
Occurs: 21 times
2-
Calling function: Process_Pragma_Declaration
3-
Error message: Unsupported pragma: Suppress initialization
4-
Nkind: N_Pragma
5-
--
61
Occurs: 9 times
72
Calling function: Do_Aggregate_Literal
83
Error message: Unhandled aggregate kind: E_PRIVATE_TYPE

‎experiments/golden-results/ksum-summary.txt

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,3 @@
1-
Occurs: 3 times
2-
Calling function: Process_Pragma_Declaration
3-
Error message: Unsupported pragma: Suppress initialization
4-
Nkind: N_Pragma
5-
--
61
Occurs: 41 times
72
Redacted compiler error message:
83
file "REDACTED" not found

‎experiments/golden-results/libkeccak-summary.txt

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,6 @@ Calling function: Process_Declaration
1818
Error message: Use type clause declaration
1919
Nkind: N_Use_Type_Clause
2020
--
21-
Occurs: 18 times
22-
Calling function: Process_Pragma_Declaration
23-
Error message: Unsupported pragma: Suppress initialization
24-
Nkind: N_Pragma
25-
--
2621
Occurs: 2 times
2722
Calling function: Do_Expression
2823
Error message: ATTRIBUTE_ASM_OUTPUT unsupported

‎experiments/golden-results/libsparkcrypto-summary.txt

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -83,11 +83,6 @@ Calling function: Do_Expression
8383
Error message: ATTRIBUTE_ASM_OUTPUT unsupported
8484
Nkind: N_Attribute_Reference
8585
--
86-
Occurs: 2 times
87-
Calling function: Process_Pragma_Declaration
88-
Error message: Known but unsupported pragma: Linker Options
89-
Nkind: N_Pragma
90-
--
9186
Occurs: 32 times
9287
Redacted compiler error message:
9388
file "REDACTED" not found

‎experiments/golden-results/vct-summary.txt

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,6 @@ Calling function: Do_Expression
1818
Error message: ATTRIBUTE_COPY_SIGN unsupported
1919
Nkind: N_Attribute_Reference
2020
--
21-
Occurs: 6 times
22-
Calling function: Process_Pragma_Declaration
23-
Error message: Unsupported pragma: Suppress initialization
24-
Nkind: N_Pragma
25-
--
2621
Occurs: 4 times
2722
Calling function: Process_Declaration
2823
Error message: size clause not applied by the front-end

‎gnat2goto/driver/tree_walk.adb

Lines changed: 65 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1514,7 +1514,10 @@ package body Tree_Walk is
15141514
when N_Quantified_Expression =>
15151515
return Report_Unhandled_Node_Irep (N, "Do_Expression",
15161516
"Quantified");
1517-
when N_Null =>
1517+
when N_Null |
1518+
-- gnat2goto does not process freeze nodes at present.
1519+
-- Possibly of use when package initialisationis considered.
1520+
N_Freeze_Entity | N_Freeze_Generic_Entity =>
15181521
return Do_Null_Expression (N);
15191522
when others =>
15201523
return Report_Unhandled_Node_Irep (N, "Do_Expression",
@@ -2936,29 +2939,36 @@ package body Tree_Walk is
29362939
-- language. Need to be detected.
29372940
Report_Unhandled_Node_Empty (N, "Do_Pragma",
29382941
"Known but unsupported pragma: Export");
2939-
when Name_Linker_Options =>
2940-
-- Used to specify the system linker parameters needed when a
2941-
-- given compilation unit is included in a partition. We want to
2942-
-- know that code manipulates the linking.
2943-
Report_Unhandled_Node_Empty (N, "Do_Pragma",
2944-
"Known but unsupported pragma: Linker Options");
29452942
when Name_Annotate |
29462943
-- Ignore here. Rather look for those when we process a node.
29472944
Name_Assertion_Policy |
29482945
-- Control the pragma Assert according to the policy identifier
29492946
-- which can be Check, Ignore, or implementation-defined.
29502947
-- Ignore means that assertions are ignored at run-time -> Ignored
2948+
Name_Compile_Time_Warning |
2949+
-- Used to issue a compile time warning from the compiler
2950+
-- front-end. The warning will be issued by the front-end but has
2951+
-- no affect on the AST. It can be ignored safely by gnat2goto.
29512952
Name_Discard_Names |
29522953
-- Used to request a reduction in storage used for the names of
29532954
-- certain entities. -> Ignored
2954-
Name_Inline |
2955+
Name_Inline |
29552956
-- Indicates that inline expansion is desired for all calls to
29562957
-- that entity. -> Ignored
2957-
Name_Inspection_Point |
2958+
Name_Inspection_Point |
29582959
-- Identifies a set of objects each of whose values is to be
29592960
-- available at the point(s) during program execution
29602961
-- corresponding to the position of the pragma in the compilation
29612962
-- unit. -> Ignored
2963+
Name_Linker_Options |
2964+
-- Used to specify the system linker parameters needed when a
2965+
-- given compilation unit is included in a partition. We want to
2966+
-- know that code manipulates the linking. The
2967+
-- goto functions produced by gnat2goto are linked by symtab2gb.
2968+
-- Currently there very few options for this linker and none that
2969+
-- apply to most linkers. Currently the pragma can ignored,
2970+
-- but in the future, if symtab2gb was to take more options
2971+
-- this pragma could be reinstated.
29622972
Name_List |
29632973
-- Takes one of the identifiers On or Off as the single
29642974
-- argument. It specifies that listing of the compilation is to be
@@ -6022,12 +6032,6 @@ package body Tree_Walk is
60226032
-- language. Need to be detected.
60236033
Put_Line (Standard_Error,
60246034
"Warning: Multi-language analysis unsupported.");
6025-
when Name_Linker_Options =>
6026-
-- Used to specify the system linker parameters needed when a
6027-
-- given compilation unit is included in a partition. We want to
6028-
-- know that code manipulates the linking.
6029-
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
6030-
"Known but unsupported pragma: Linker Options");
60316035
when Name_Machine_Attribute =>
60326036
Handle_Pragma_Machine_Attribute (N);
60336037
when Name_Check =>
@@ -6044,8 +6048,33 @@ package body Tree_Walk is
60446048
null;
60456049

60466050
when Name_Suppress_Initialization =>
6047-
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
6048-
"Unsupported pragma: Suppress initialization");
6051+
-- pragma Suppress_Initialization can be ignored if it is
6052+
-- appied to an array or scalar type which do not have a
6053+
-- default value aspect applied.
6054+
-- If these conditions are not met an unsupported pragma is
6055+
-- reported.
6056+
declare
6057+
Arg : constant Node_Id :=
6058+
First (Pragma_Argument_Associations (N));
6059+
E : constant Entity_Id := Entity
6060+
(if Present (Arg) and then
6061+
Nkind (Arg) = N_Pragma_Argument_Association
6062+
then
6063+
Expression (Arg)
6064+
else
6065+
Arg);
6066+
begin
6067+
if not ((Is_Array_Type (E) and then
6068+
not Present (Default_Aspect_Component_Value (E)))
6069+
or else
6070+
(Is_Scalar_Type (E) and then
6071+
not Present (Default_Aspect_Value (E))))
6072+
then
6073+
Report_Unhandled_Node_Empty
6074+
(N, "Process_Pragma_Declaration",
6075+
"Unsupported pragma: Suppress initialization");
6076+
end if;
6077+
end;
60496078
when Name_Obsolescent =>
60506079
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
60516080
"Unsupported pragma: Obsolescent");
@@ -6058,6 +6087,10 @@ package body Tree_Walk is
60586087
-- Control the pragma Assert according to the policy identifier
60596088
-- which can be Check, Ignore, or implementation-defined.
60606089
-- Ignore means that assertions are ignored at run-time -> Ignored
6090+
Name_Compile_Time_Warning |
6091+
-- Used to issue a compile time warning from the compiler
6092+
-- front-end. The warning will be issued by the front-end but has
6093+
-- no affect on the AST. It can be ignored safely by gnat2goto.
60616094
Name_Discard_Names |
60626095
-- Used to request a reduction in storage used for the names of
60636096
-- certain entities. -> Ignored
@@ -6066,6 +6099,17 @@ package body Tree_Walk is
60666099
-- available at the point(s) during program execution
60676100
-- corresponding to the position of the pragma in the compilation
60686101
-- unit. -> Ignored
6102+
Name_Linker_Options |
6103+
-- Used to specify the system linker parameters needed when a
6104+
-- given compilation unit is included in a partition. We want to
6105+
-- know that code manipulates the linking.Name_Linker_Options =>
6106+
-- Used to specify the system linker parameters needed when a
6107+
-- given compilation unit is included in a partition. The
6108+
-- goto functions produced by gnat2goto are linked by symtab2gb.
6109+
-- Currently there very few options for this linker and none that
6110+
-- apply to most linkers. Currently the pragma can ignored,
6111+
-- but in the future, if symtab2gb was to take more options
6112+
-- this pragma could be reinstated.
60696113
Name_List |
60706114
-- Takes one of the identifiers On or Off as the single
60716115
-- argument. It specifies that listing of the compilation is to be
@@ -6278,6 +6322,10 @@ package body Tree_Walk is
62786322
when N_Object_Declaration =>
62796323
Do_Object_Declaration (N, Block);
62806324

6325+
when N_Freeze_Entity | N_Freeze_Generic_Entity =>
6326+
-- gnat2goto does not process freeze nodes as
6327+
-- the information contained therein is not needed by gnat2goto.
6328+
null;
62816329
when others =>
62826330
Report_Unhandled_Node_Empty (N, "Process_Statement",
62836331
"Unknown expression kind");

‎testsuite/gnat2goto/tests/fixed_array_address_model/test.out

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,3 @@
1-
Standard_Output from gnat2goto fixed_array_address_model:
2-
----------At: Process_Pragma_Declaration----------
3-
----------Unknown pragma: compile_time_warning----------
4-
N_Pragma (Node_Id=3683) (source,analyzed)
5-
Sloc = 19196 s-atacco.ads:42:4 [fixed_array_address_model.adb:10:4]
6-
Pragma_Argument_Associations = List (List_Id=-99999824)
7-
Pragma_Identifier = N_Identifier "compile_time_warning" (Node_Id=3695)
8-
91
[fixed_array_address_model.assertion.1] line 18 Ada Check assertion: SUCCESS
102
[fixed_array_address_model.assertion.2] line 24 assertion PV.all (I) = My_Int (I): SUCCESS
113
[fixed_array_address_model.assertion.3] line 32 assertion V (I) = My_Int (V'Last - I + 1): SUCCESS

‎testsuite/gnat2goto/tests/more_pragmas/more_pragmas.adb

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
procedure More_Pragmas is
2+
-- The following pragma should not be reported as unsupported.
3+
pragma Linker_Options ("Dummy");
4+
5+
pragma Compile_Time_Warning (True, "This should not be reported as unsupported");
6+
7+
type A1 is array (1 .. 10) of Integer;
8+
-- The following pragma should not be reported as unsupported.
9+
pragma Suppress_Initialization (A1);
10+
11+
type My_Int is range 0 .. 100;
12+
-- The following pragma should not be reported as unsupported.
13+
pragma Suppress_Initialization (My_Int);
14+
15+
type A2 is array (1 .. 10) of Integer with Default_Component_Value => 0;
16+
-- The following pragma should be reported as unsupported.
17+
pragma Suppress_Initialization (A2);
18+
19+
type R is record
20+
A, B : Integer;
21+
end record;
22+
-- The following pragma should be reported as unsupported.
23+
pragma Suppress_Initialization (R);
24+
25+
type My_Int_2 is range 0 .. 100 with Default_Value => 0;
26+
-- The following pragma should be reported as unsupported.
27+
pragma Suppress_Initialization (My_int_2);
28+
29+
V : Integer := 0;
30+
-- The following pragma should be reported as unsupported.
31+
pragma Suppress_Initialization (V);
32+
33+
pragma Compile_Time_Warning (False, "This should not be reported as unsupported");
34+
begin
35+
pragma Compile_Time_Warning (True, "This should not be reported as unsupported");
36+
pragma Assert (V = 0);
37+
pragma Compile_Time_Warning (V /= 0, "This should not be reported as unsupported");
38+
end More_Pragmas;

‎testsuite/gnat2goto/tests/more_pragmas/test.out

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
Standard_Output from gnat2goto more_pragmas:
2+
----------At: Process_Pragma_Declaration----------
3+
----------Unsupported pragma: Suppress initialization----------
4+
N_Pragma (Node_Id=2315) (source,analyzed)
5+
Sloc = 8846 more_pragmas.adb:17:4
6+
Pragma_Argument_Associations = List (List_Id=-99999973)
7+
Pragma_Identifier = N_Identifier "suppress_initialization" (Node_Id=2316)
8+
Next_Rep_Item = N_Aspect_Specification (Node_Id=2313)
9+
----------At: Process_Pragma_Declaration----------
10+
----------Unsupported pragma: Suppress initialization----------
11+
N_Pragma (Node_Id=2351) (source,analyzed)
12+
Sloc = 9008 more_pragmas.adb:23:4
13+
Pragma_Argument_Associations = List (List_Id=-99999969)
14+
Pragma_Identifier = N_Identifier "suppress_initialization" (Node_Id=2352)
15+
----------At: Process_Pragma_Declaration----------
16+
----------Unsupported pragma: Suppress initialization----------
17+
N_Pragma (Node_Id=2370) (source,analyzed)
18+
Sloc = 9172 more_pragmas.adb:27:4
19+
Pragma_Argument_Associations = List (List_Id=-99999966)
20+
Pragma_Identifier = N_Identifier "suppress_initialization" (Node_Id=2371)
21+
Next_Rep_Item = N_Aspect_Specification (Node_Id=2368)
22+
----------At: Process_Pragma_Declaration----------
23+
----------Unsupported pragma: Suppress initialization----------
24+
N_Pragma (Node_Id=2384) (source,analyzed)
25+
Sloc = 9304 more_pragmas.adb:31:4
26+
Pragma_Argument_Associations = List (List_Id=-99999964)
27+
Pragma_Identifier = N_Identifier "suppress_initialization" (Node_Id=2385)
28+
29+
Standard_Error from gnat2goto more_pragmas:
30+
more_pragmas.adb:5:33: warning: This should not be reported as unsupported
31+
more_pragmas.adb:35:33: warning: This should not be reported as unsupported
32+
33+
[more_pragmas.assertion.1] line 36 assertion V = 0: SUCCESS
34+
VERIFICATION SUCCESSFUL

0 commit comments

Comments
 (0)