Skip to content

Commit 2c13a66

Browse files
martin-csmartin-cs
authored
Merge branch 'master' into nondet_model
2 parents 6639ba6 + ec134c3 commit 2c13a66

File tree

14 files changed

+146
-74
lines changed

14 files changed

+146
-74
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: 163 times
2217
Calling function: Process_Pragma_Declaration
2318
Error message: pragma Export: Multi-language analysis unsupported
@@ -194,6 +189,11 @@ Error message: Unsupported pragma: Refine
194189
Nkind: N_Pragma
195190
--
196191
Occurs: 1 times
192+
Calling function: Process_Pragma_Declaration
193+
Error message: Unsupported pragma: Suppress initialization
194+
Nkind: N_Pragma
195+
--
196+
Occurs: 1 times
197197
Calling function: Process_Statement
198198
Error message: Unknown expression kind
199199
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: 1 times
72
Calling function: Process_Pragma_Declaration
83
Error message: pragma Import: Multi-language analysis unsupported

‎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: 9 times
2217
Calling function: Process_Pragma_Declaration
2318
Error message: pragma Import: Multi-language analysis 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: 66 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1499,7 +1499,10 @@ package body Tree_Walk is
14991499
when N_Quantified_Expression =>
15001500
return Report_Unhandled_Node_Irep (N, "Do_Expression",
15011501
"Quantified");
1502-
when N_Null =>
1502+
when N_Null |
1503+
-- gnat2goto does not process freeze nodes at present.
1504+
-- Possibly of use when package initialisationis considered.
1505+
N_Freeze_Entity | N_Freeze_Generic_Entity =>
15031506
return Do_Null_Expression (N);
15041507
when others =>
15051508
return Report_Unhandled_Node_Irep (N, "Do_Expression",
@@ -2794,29 +2797,36 @@ package body Tree_Walk is
27942797
-- language. Need to be detected.
27952798
Report_Unhandled_Node_Empty (N, "Do_Pragma",
27962799
"Known but unsupported pragma: Export");
2797-
when Name_Linker_Options =>
2798-
-- Used to specify the system linker parameters needed when a
2799-
-- given compilation unit is included in a partition. We want to
2800-
-- know that code manipulates the linking.
2801-
Report_Unhandled_Node_Empty (N, "Do_Pragma",
2802-
"Known but unsupported pragma: Linker Options");
28032800
when Name_Annotate |
28042801
-- Ignore here. Rather look for those when we process a node.
28052802
Name_Assertion_Policy | Name_Check_Policy |
28062803
-- Control the pragma Assert according to the policy identifier
28072804
-- which can be Check, Ignore, or implementation-defined.
28082805
-- Ignore means that assertions are ignored at run-time -> Ignored
2806+
Name_Compile_Time_Warning |
2807+
-- Used to issue a compile time warning from the compiler
2808+
-- front-end. The warning will be issued by the front-end but has
2809+
-- no affect on the AST. It can be ignored safely by gnat2goto.
28092810
Name_Discard_Names |
28102811
-- Used to request a reduction in storage used for the names of
28112812
-- certain entities. -> Ignored
2812-
Name_Inline |
2813+
Name_Inline |
28132814
-- Indicates that inline expansion is desired for all calls to
28142815
-- that entity. -> Ignored
2815-
Name_Inspection_Point |
2816+
Name_Inspection_Point |
28162817
-- Identifies a set of objects each of whose values is to be
28172818
-- available at the point(s) during program execution
28182819
-- corresponding to the position of the pragma in the compilation
28192820
-- unit. -> Ignored
2821+
Name_Linker_Options |
2822+
-- Used to specify the system linker parameters needed when a
2823+
-- given compilation unit is included in a partition. We want to
2824+
-- know that code manipulates the linking. The
2825+
-- goto functions produced by gnat2goto are linked by symtab2gb.
2826+
-- Currently there very few options for this linker and none that
2827+
-- apply to most linkers. Currently the pragma can ignored,
2828+
-- but in the future, if symtab2gb was to take more options
2829+
-- this pragma could be reinstated.
28202830
Name_List |
28212831
-- Takes one of the identifiers On or Off as the single
28222832
-- argument. It specifies that listing of the compilation is to be
@@ -5950,7 +5960,7 @@ package body Tree_Walk is
59505960
-- given compilation unit is included in a partition. We want to
59515961
-- know that code manipulates the linking.
59525962
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
5953-
"Known but unsupported pragma: Linker Options");
5963+
"Known but unsupported pragma: Linker Options");
59545964
when Name_Machine_Attribute =>
59555965
Handle_Pragma_Machine_Attribute (N);
59565966
when Name_Check =>
@@ -5967,8 +5977,33 @@ package body Tree_Walk is
59675977
null;
59685978

59695979
when Name_Suppress_Initialization =>
5970-
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
5971-
"Unsupported pragma: Suppress initialization");
5980+
-- pragma Suppress_Initialization can be ignored if it is
5981+
-- appied to an array or scalar type which do not have a
5982+
-- default value aspect applied.
5983+
-- If these conditions are not met an unsupported pragma is
5984+
-- reported.
5985+
declare
5986+
Arg : constant Node_Id :=
5987+
First (Pragma_Argument_Associations (N));
5988+
E : constant Entity_Id := Entity
5989+
(if Present (Arg) and then
5990+
Nkind (Arg) = N_Pragma_Argument_Association
5991+
then
5992+
Expression (Arg)
5993+
else
5994+
Arg);
5995+
begin
5996+
if not ((Is_Array_Type (E) and then
5997+
not Present (Default_Aspect_Component_Value (E)))
5998+
or else
5999+
(Is_Scalar_Type (E) and then
6000+
not Present (Default_Aspect_Value (E))))
6001+
then
6002+
Report_Unhandled_Node_Empty
6003+
(N, "Process_Pragma_Declaration",
6004+
"Unsupported pragma: Suppress initialization");
6005+
end if;
6006+
end;
59726007
when Name_Obsolescent =>
59736008
Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
59746009
"Unsupported pragma: Obsolescent");
@@ -6013,6 +6048,10 @@ package body Tree_Walk is
60136048
-- Control the pragma Assert according to the policy identifier
60146049
-- which can be Check, Ignore, or implementation-defined.
60156050
-- Ignore means that assertions are ignored at run-time -> Ignored
6051+
Name_Compile_Time_Warning |
6052+
-- Used to issue a compile time warning from the compiler
6053+
-- front-end. The warning will be issued by the front-end but has
6054+
-- no affect on the AST. It can be ignored safely by gnat2goto.
60166055
Name_Discard_Names |
60176056
-- Used to request a reduction in storage used for the names of
60186057
-- certain entities. -> Ignored
@@ -6021,6 +6060,17 @@ package body Tree_Walk is
60216060
-- available at the point(s) during program execution
60226061
-- corresponding to the position of the pragma in the compilation
60236062
-- unit. -> Ignored
6063+
Name_Linker_Options |
6064+
-- Used to specify the system linker parameters needed when a
6065+
-- given compilation unit is included in a partition. We want to
6066+
-- know that code manipulates the linking.Name_Linker_Options =>
6067+
-- Used to specify the system linker parameters needed when a
6068+
-- given compilation unit is included in a partition. The
6069+
-- goto functions produced by gnat2goto are linked by symtab2gb.
6070+
-- Currently there very few options for this linker and none that
6071+
-- apply to most linkers. Currently the pragma can ignored,
6072+
-- but in the future, if symtab2gb was to take more options
6073+
-- this pragma could be reinstated.
60246074
Name_List |
60256075
-- Takes one of the identifiers On or Off as the single
60266076
-- argument. It specifies that listing of the compilation is to be
@@ -6233,6 +6283,10 @@ package body Tree_Walk is
62336283
when N_Object_Declaration =>
62346284
Do_Object_Declaration (N, Block);
62356285

6286+
when N_Freeze_Entity | N_Freeze_Generic_Entity =>
6287+
-- gnat2goto does not process freeze nodes as
6288+
-- the information contained therein is not needed by gnat2goto.
6289+
null;
62366290
when others =>
62376291
Report_Unhandled_Node_Empty (N, "Process_Statement",
62386292
"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)