Skip to content

Commit ec134c3

Browse files
martin-csmartin-cs
authored
Merge pull request #351 from tjj2017/more_pragmas
More pragmas
2 parents 680ef4b + 50f03af commit ec134c3

File tree

14 files changed

+137
-78
lines changed

14 files changed

+137
-78
lines changed

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,6 @@ 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-
--
2116
Occurs: 153 times
2217
Calling function: Process_Pragma_Declaration
2318
Error message: Unsupported pragma: Postcondition
@@ -189,6 +184,11 @@ Error message: Unsupported pragma: Refine
189184
Nkind: N_Pragma
190185
--
191186
Occurs: 1 times
187+
Calling function: Process_Pragma_Declaration
188+
Error message: Unsupported pragma: Suppress initialization
189+
Nkind: N_Pragma
190+
--
191+
Occurs: 1 times
192192
Calling function: Process_Statement
193193
Error message: Unknown expression kind
194194
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: 57 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -2926,29 +2926,36 @@ package body Tree_Walk is
29262926
-- language. Need to be detected.
29272927
Report_Unhandled_Node_Empty (N, "Do_Pragma",
29282928
"Known but unsupported pragma: Export");
2929-
when Name_Linker_Options =>
2930-
-- Used to specify the system linker parameters needed when a
2931-
-- given compilation unit is included in a partition. We want to
2932-
-- know that code manipulates the linking.
2933-
Report_Unhandled_Node_Empty (N, "Do_Pragma",
2934-
"Known but unsupported pragma: Linker Options");
29352929
when Name_Annotate |
29362930
-- Ignore here. Rather look for those when we process a node.
29372931
Name_Assertion_Policy |
29382932
-- Control the pragma Assert according to the policy identifier
29392933
-- which can be Check, Ignore, or implementation-defined.
29402934
-- Ignore means that assertions are ignored at run-time -> Ignored
2935+
Name_Compile_Time_Warning |
2936+
-- Used to issue a compile time warning from the compiler
2937+
-- front-end. The warning will be issued by the front-end but has
2938+
-- no affect on the AST. It can be ignored safely by gnat2goto.
29412939
Name_Discard_Names |
29422940
-- Used to request a reduction in storage used for the names of
29432941
-- certain entities. -> Ignored
2944-
Name_Inline |
2942+
Name_Inline |
29452943
-- Indicates that inline expansion is desired for all calls to
29462944
-- that entity. -> Ignored
2947-
Name_Inspection_Point |
2945+
Name_Inspection_Point |
29482946
-- Identifies a set of objects each of whose values is to be
29492947
-- available at the point(s) during program execution
29502948
-- corresponding to the position of the pragma in the compilation
29512949
-- unit. -> Ignored
2950+
Name_Linker_Options |
2951+
-- Used to specify the system linker parameters needed when a
2952+
-- given compilation unit is included in a partition. We want to
2953+
-- know that code manipulates the linking. The
2954+
-- goto functions produced by gnat2goto are linked by symtab2gb.
2955+
-- Currently there very few options for this linker and none that
2956+
-- apply to most linkers. Currently the pragma can ignored,
2957+
-- but in the future, if symtab2gb was to take more options
2958+
-- this pragma could be reinstated.
29522959
Name_List |
29532960
-- Takes one of the identifiers On or Off as the single
29542961
-- argument. It specifies that listing of the compilation is to be
@@ -6012,12 +6019,6 @@ package body Tree_Walk is
60126019
-- language. Need to be detected.
60136020
Put_Line (Standard_Error,
60146021
"Warning: Multi-language analysis unsupported.");
6015-
when Name_Linker_Options =>
6016-
-- Used to specify the system linker parameters needed when a
6017-
-- given compilation unit is included in a partition. We want to
6018-
-- know that code manipulates the linking.
6019-
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
6020-
"Known but unsupported pragma: Linker Options");
60216022
when Name_Machine_Attribute =>
60226023
Handle_Pragma_Machine_Attribute (N);
60236024
when Name_Check =>
@@ -6034,8 +6035,33 @@ package body Tree_Walk is
60346035
null;
60356036

60366037
when Name_Suppress_Initialization =>
6037-
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
6038-
"Unsupported pragma: Suppress initialization");
6038+
-- pragma Suppress_Initialization can be ignored if it is
6039+
-- appied to an array or scalar type which do not have a
6040+
-- default value aspect applied.
6041+
-- If these conditions are not met an unsupported pragma is
6042+
-- reported.
6043+
declare
6044+
Arg : constant Node_Id :=
6045+
First (Pragma_Argument_Associations (N));
6046+
E : constant Entity_Id := Entity
6047+
(if Present (Arg) and then
6048+
Nkind (Arg) = N_Pragma_Argument_Association
6049+
then
6050+
Expression (Arg)
6051+
else
6052+
Arg);
6053+
begin
6054+
if not ((Is_Array_Type (E) and then
6055+
not Present (Default_Aspect_Component_Value (E)))
6056+
or else
6057+
(Is_Scalar_Type (E) and then
6058+
not Present (Default_Aspect_Value (E))))
6059+
then
6060+
Report_Unhandled_Node_Empty
6061+
(N, "Process_Pragma_Declaration",
6062+
"Unsupported pragma: Suppress initialization");
6063+
end if;
6064+
end;
60396065
when Name_Obsolescent =>
60406066
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
60416067
"Unsupported pragma: Obsolescent");
@@ -6048,6 +6074,10 @@ package body Tree_Walk is
60486074
-- Control the pragma Assert according to the policy identifier
60496075
-- which can be Check, Ignore, or implementation-defined.
60506076
-- Ignore means that assertions are ignored at run-time -> Ignored
6077+
Name_Compile_Time_Warning |
6078+
-- Used to issue a compile time warning from the compiler
6079+
-- front-end. The warning will be issued by the front-end but has
6080+
-- no affect on the AST. It can be ignored safely by gnat2goto.
60516081
Name_Discard_Names |
60526082
-- Used to request a reduction in storage used for the names of
60536083
-- certain entities. -> Ignored
@@ -6056,6 +6086,17 @@ package body Tree_Walk is
60566086
-- available at the point(s) during program execution
60576087
-- corresponding to the position of the pragma in the compilation
60586088
-- unit. -> Ignored
6089+
Name_Linker_Options |
6090+
-- Used to specify the system linker parameters needed when a
6091+
-- given compilation unit is included in a partition. We want to
6092+
-- know that code manipulates the linking.Name_Linker_Options =>
6093+
-- Used to specify the system linker parameters needed when a
6094+
-- given compilation unit is included in a partition. The
6095+
-- goto functions produced by gnat2goto are linked by symtab2gb.
6096+
-- Currently there very few options for this linker and none that
6097+
-- apply to most linkers. Currently the pragma can ignored,
6098+
-- but in the future, if symtab2gb was to take more options
6099+
-- this pragma could be reinstated.
60596100
Name_List |
60606101
-- Takes one of the identifiers On or Off as the single
60616102
-- argument. It specifies that listing of the compilation is to be

‎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)