Skip to content

Commit 235de82

Browse files
martin-csmartin-cs
authored
Merge branch 'master' into iss_131_ready
2 parents 8d37adf + ec134c3 commit 235de82

File tree

14 files changed

+145
-79
lines changed

14 files changed

+145
-79
lines changed

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,6 @@ Calling function: Process_Declaration
88
Error message: Unknown declaration kind
99
Nkind: N_Validate_Unchecked_Conversion
1010
--
11-
Occurs: 202 times
12-
Calling function: Process_Pragma_Declaration
13-
Error message: Unsupported pragma: Suppress initialization
14-
Nkind: N_Pragma
15-
--
1611
Occurs: 153 times
1712
Calling function: Process_Pragma_Declaration
1813
Error message: Unsupported pragma: Postcondition
@@ -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
@@ -13,11 +13,6 @@ Calling function: Process_Declaration
1313
Error message: Use type clause declaration
1414
Nkind: N_Use_Type_Clause
1515
--
16-
Occurs: 18 times
17-
Calling function: Process_Pragma_Declaration
18-
Error message: Unsupported pragma: Suppress initialization
19-
Nkind: N_Pragma
20-
--
2116
Occurs: 2 times
2217
Calling function: Do_Expression
2318
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
@@ -78,11 +78,6 @@ Calling function: Do_Expression
7878
Error message: ATTRIBUTE_ASM_OUTPUT unsupported
7979
Nkind: N_Attribute_Reference
8080
--
81-
Occurs: 2 times
82-
Calling function: Process_Pragma_Declaration
83-
Error message: Known but unsupported pragma: Linker Options
84-
Nkind: N_Pragma
85-
--
8681
Occurs: 32 times
8782
Redacted compiler error message:
8883
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: 3 times
2722
Calling function: Do_Expression
2823
Error message: ATTRIBUTE_IMAGE unsupported

‎gnat2goto/driver/tree_walk.adb

Lines changed: 65 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1457,7 +1457,10 @@ package body Tree_Walk is
14571457
when N_Quantified_Expression =>
14581458
return Report_Unhandled_Node_Irep (N, "Do_Expression",
14591459
"Quantified");
1460-
when N_Null =>
1460+
when N_Null |
1461+
-- gnat2goto does not process freeze nodes at present.
1462+
-- Possibly of use when package initialisationis considered.
1463+
N_Freeze_Entity | N_Freeze_Generic_Entity =>
14611464
return Do_Null_Expression (N);
14621465
when others =>
14631466
return Report_Unhandled_Node_Irep (N, "Do_Expression",
@@ -2879,29 +2882,36 @@ package body Tree_Walk is
28792882
-- language. Need to be detected.
28802883
Report_Unhandled_Node_Empty (N, "Do_Pragma",
28812884
"Known but unsupported pragma: Export");
2882-
when Name_Linker_Options =>
2883-
-- Used to specify the system linker parameters needed when a
2884-
-- given compilation unit is included in a partition. We want to
2885-
-- know that code manipulates the linking.
2886-
Report_Unhandled_Node_Empty (N, "Do_Pragma",
2887-
"Known but unsupported pragma: Linker Options");
28882885
when Name_Annotate |
28892886
-- Ignore here. Rather look for those when we process a node.
28902887
Name_Assertion_Policy |
28912888
-- Control the pragma Assert according to the policy identifier
28922889
-- which can be Check, Ignore, or implementation-defined.
28932890
-- Ignore means that assertions are ignored at run-time -> Ignored
2891+
Name_Compile_Time_Warning |
2892+
-- Used to issue a compile time warning from the compiler
2893+
-- front-end. The warning will be issued by the front-end but has
2894+
-- no affect on the AST. It can be ignored safely by gnat2goto.
28942895
Name_Discard_Names |
28952896
-- Used to request a reduction in storage used for the names of
28962897
-- certain entities. -> Ignored
2897-
Name_Inline |
2898+
Name_Inline |
28982899
-- Indicates that inline expansion is desired for all calls to
28992900
-- that entity. -> Ignored
2900-
Name_Inspection_Point |
2901+
Name_Inspection_Point |
29012902
-- Identifies a set of objects each of whose values is to be
29022903
-- available at the point(s) during program execution
29032904
-- corresponding to the position of the pragma in the compilation
29042905
-- unit. -> Ignored
2906+
Name_Linker_Options |
2907+
-- Used to specify the system linker parameters needed when a
2908+
-- given compilation unit is included in a partition. We want to
2909+
-- know that code manipulates the linking. The
2910+
-- goto functions produced by gnat2goto are linked by symtab2gb.
2911+
-- Currently there very few options for this linker and none that
2912+
-- apply to most linkers. Currently the pragma can ignored,
2913+
-- but in the future, if symtab2gb was to take more options
2914+
-- this pragma could be reinstated.
29052915
Name_List |
29062916
-- Takes one of the identifiers On or Off as the single
29072917
-- argument. It specifies that listing of the compilation is to be
@@ -5936,12 +5946,6 @@ package body Tree_Walk is
59365946
-- language. Need to be detected.
59375947
Put_Line (Standard_Error,
59385948
"Warning: Multi-language analysis unsupported.");
5939-
when Name_Linker_Options =>
5940-
-- Used to specify the system linker parameters needed when a
5941-
-- given compilation unit is included in a partition. We want to
5942-
-- know that code manipulates the linking.
5943-
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
5944-
"Known but unsupported pragma: Linker Options");
59455949
when Name_Machine_Attribute =>
59465950
Handle_Pragma_Machine_Attribute (N);
59475951
when Name_Check =>
@@ -5958,8 +5962,33 @@ package body Tree_Walk is
59585962
null;
59595963

59605964
when Name_Suppress_Initialization =>
5961-
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
5962-
"Unsupported pragma: Suppress initialization");
5965+
-- pragma Suppress_Initialization can be ignored if it is
5966+
-- appied to an array or scalar type which do not have a
5967+
-- default value aspect applied.
5968+
-- If these conditions are not met an unsupported pragma is
5969+
-- reported.
5970+
declare
5971+
Arg : constant Node_Id :=
5972+
First (Pragma_Argument_Associations (N));
5973+
E : constant Entity_Id := Entity
5974+
(if Present (Arg) and then
5975+
Nkind (Arg) = N_Pragma_Argument_Association
5976+
then
5977+
Expression (Arg)
5978+
else
5979+
Arg);
5980+
begin
5981+
if not ((Is_Array_Type (E) and then
5982+
not Present (Default_Aspect_Component_Value (E)))
5983+
or else
5984+
(Is_Scalar_Type (E) and then
5985+
not Present (Default_Aspect_Value (E))))
5986+
then
5987+
Report_Unhandled_Node_Empty
5988+
(N, "Process_Pragma_Declaration",
5989+
"Unsupported pragma: Suppress initialization");
5990+
end if;
5991+
end;
59635992
when Name_Obsolescent =>
59645993
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
59655994
"Unsupported pragma: Obsolescent");
@@ -5972,6 +6001,10 @@ package body Tree_Walk is
59726001
-- Control the pragma Assert according to the policy identifier
59736002
-- which can be Check, Ignore, or implementation-defined.
59746003
-- Ignore means that assertions are ignored at run-time -> Ignored
6004+
Name_Compile_Time_Warning |
6005+
-- Used to issue a compile time warning from the compiler
6006+
-- front-end. The warning will be issued by the front-end but has
6007+
-- no affect on the AST. It can be ignored safely by gnat2goto.
59756008
Name_Discard_Names |
59766009
-- Used to request a reduction in storage used for the names of
59776010
-- certain entities. -> Ignored
@@ -5980,6 +6013,17 @@ package body Tree_Walk is
59806013
-- available at the point(s) during program execution
59816014
-- corresponding to the position of the pragma in the compilation
59826015
-- unit. -> Ignored
6016+
Name_Linker_Options |
6017+
-- Used to specify the system linker parameters needed when a
6018+
-- given compilation unit is included in a partition. We want to
6019+
-- know that code manipulates the linking.Name_Linker_Options =>
6020+
-- Used to specify the system linker parameters needed when a
6021+
-- given compilation unit is included in a partition. The
6022+
-- goto functions produced by gnat2goto are linked by symtab2gb.
6023+
-- Currently there very few options for this linker and none that
6024+
-- apply to most linkers. Currently the pragma can ignored,
6025+
-- but in the future, if symtab2gb was to take more options
6026+
-- this pragma could be reinstated.
59836027
Name_List |
59846028
-- Takes one of the identifiers On or Off as the single
59856029
-- argument. It specifies that listing of the compilation is to be
@@ -6192,6 +6236,10 @@ package body Tree_Walk is
61926236
when N_Object_Declaration =>
61936237
Do_Object_Declaration (N, Block);
61946238

6239+
when N_Freeze_Entity | N_Freeze_Generic_Entity =>
6240+
-- gnat2goto does not process freeze nodes as
6241+
-- the information contained therein is not needed by gnat2goto.
6242+
null;
61956243
when others =>
61966244
Report_Unhandled_Node_Empty (N, "Process_Statement",
61976245
"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)