Skip to content

Commit 77c6e75

Browse files
committed
Add test for address representation clauses
1 parent 98812b4 commit 77c6e75

File tree

3 files changed

+40
-0
lines changed

3 files changed

+40
-0
lines changed
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
with System; use System;
2+
with System.Storage_Elements;
3+
procedure Address_Clause is
4+
Var_Addr_1 : Integer;
5+
for Var_Addr_1'Address use System'To_Address (16#6F#);
6+
7+
Var_Addr_2 : Integer;
8+
for Var_Addr_2'Address use System.Storage_Elements.To_Address (16#80#);
9+
begin
10+
Var_Addr_1 := 1;
11+
Var_Addr_2 := 2;
12+
pragma Assert (Var_Addr_1 + Var_Addr_2 = 3);
13+
end Address_Clause;
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
Standard_Output from gnat2goto address_clause:
2+
N_Attribute_Definition_Clause "address" (Node_Id=2277) (source,analyzed)
3+
Sloc = 12399 address_clause.adb:5:4
4+
Chars = "address" (Name_Id=300000791)
5+
Name = N_Identifier "var_addr_1" (Node_Id=2274)
6+
Expression = N_Function_Call (Node_Id=2280)
7+
Entity = N_Defining_Identifier "var_addr_1" (Entity_Id=2264)
8+
Check_Address_Alignment = True
9+
N_Attribute_Definition_Clause "address" (Node_Id=2295) (source,analyzed)
10+
Sloc = 12483 address_clause.adb:8:4
11+
Chars = "address" (Name_Id=300000791)
12+
Name = N_Identifier "var_addr_2" (Node_Id=2292)
13+
Expression = N_Function_Call (Node_Id=2302)
14+
Entity = N_Defining_Identifier "var_addr_2" (Entity_Id=2282)
15+
Check_Address_Alignment = True
16+
17+
Standard_Error from gnat2goto address_clause:
18+
----------At: Process_Declaration----------
19+
----------Address representation clauses are not currently supported----------
20+
----------At: Process_Declaration----------
21+
----------Address representation clauses are not currently supported----------
22+
23+
[1] file address_clause.adb line 12 assertion: SUCCESS
24+
VERIFICATION SUCCESSFUL
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
from test_support import *
2+
3+
prove()

0 commit comments

Comments
 (0)