Skip to content

Commit e6f09b8

Browse files
committed
Ada: fixes for the No_Secondary_Stack restriction
- Align README.md and GPR files with the fact that the server no longer compiles with the No_Secondary_Stack restriction. - Fix include.am to reference the new name for the adc file.
1 parent 98eda78 commit e6f09b8

File tree

5 files changed

+24
-21
lines changed

5 files changed

+24
-21
lines changed

wrapper/Ada/README.md

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,11 @@ code to zero-out stack frames used by subprograms.
1313
Unfortunately this works well for the primary stack but not
1414
for the secondary stack. The GNAT User's Guide recommends
1515
avoiding the secondary stack using the restriction
16-
No_Secondary_Stack (see the GNAT configuration file gnat.adc
16+
No_Secondary_Stack (see the GNAT configuration file restricted.adc
1717
which instructs compilation of the WolfSSL Ada binding under
1818
this restriction). Note, however, that the examples do make use of the
19-
secondary stack.
19+
secondary stack and the Alire project does not include this restriction, for
20+
letting users of the library to define it at their level.
2021

2122
Portability: The WolfSSL Ada binding makes no usage of controlled types
2223
and has no dependency upon the Ada.Finalization package.
@@ -25,11 +26,11 @@ the restriction No_Finalization. The WolfSSL Ada binding has
2526
been developed with maximum portability in mind.
2627

2728
Not only can the WolfSSL Ada binding be used in Ada applications but
28-
also SPARK applications (a subset of the Ada language suitable
29+
also SPARK applications (a subset of the Ada language suitable for
2930
formal verification). To formally verify the Ada code in this repository
30-
open the client.gpr with GNAT Studio and then select
31+
open the examples.gpr with GNAT Studio and then select
3132
SPARK -> Prove All Sources and use Proof Level 2. Or when using the command
32-
line, use `gnatprove -Pclient.gpr --level=4 -j12` (`-j12` is there in
33+
line, use `gnatprove -Pexamples.gpr --level=4 -j12` (`-j12` is there in
3334
order to instruct the prover to use 12 CPUs if available).
3435

3536
```
@@ -83,7 +84,7 @@ and use gprbuild to build the source code.
8384
cd wrapper/Ada
8485
gprclean
8586
gprbuild default.gpr
86-
gprbuild client.gpr
87+
gprbuild examples.gpr
8788

8889
cd obj/
8990
./tls_server_main &
@@ -93,7 +94,7 @@ cd obj/
9394
On Windows, build the executables with:
9495
```sh
9596
gprbuild -XOS=Windows default.gpr
96-
gprbuild -XOS=Windows client.gpr
97+
gprbuild -XOS=Windows examples.gpr
9798
```
9899

99100
## Files

wrapper/Ada/default.gpr

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -11,17 +11,19 @@ project Default is
1111
"../../src",
1212
"../../wolfcrypt/src");
1313

14-
-- Don't build the tls client application because it makes use
14+
-- Don't build the tls application examples because they make use
1515
-- of the Secondary Stack due to usage of the Ada.Command_Line
1616
-- package. All other Ada source code does not use the secondary stack.
17-
for Excluded_Source_Files use ("tls_client_main.adb",
18-
"tls_client.ads",
19-
"tls_client.adb");
17+
for Excluded_Source_Files use
18+
("tls_client_main.adb",
19+
"tls_client.ads",
20+
"tls_client.adb",
21+
"tls_server_main.adb",
22+
"tls_server.ads",
23+
"tls_server.adb");
2024

2125
for Object_Dir use "obj";
2226

23-
for Main use ("tls_server_main.adb");
24-
2527
package Naming is
2628
for Spec_Suffix ("C") use ".h";
2729
end Naming;
Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
project Client is
1+
project Examples is
22
type OS_Kind is ("Windows", "Linux_Or_Mac");
33

44
OS : OS_Kind := external ("OS", "Linux_Or_Mac");
@@ -12,7 +12,7 @@ project Client is
1212

1313
for Object_Dir use "obj";
1414

15-
for Main use ("tls_client_main.adb");
15+
for Main use ("tls_server_main.adb", "tls_client_main.adb");
1616

1717
package Naming is
1818
for Spec_Suffix ("C") use ".h";
@@ -75,4 +75,4 @@ project Client is
7575
for Switches ("Ada") use ("-Es"); -- To include stack traces.
7676
end Binder;
7777

78-
end Client;
78+
end Examples;

wrapper/Ada/include.am

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44

55
EXTRA_DIST+= wrapper/Ada/README.md
66
EXTRA_DIST+= wrapper/Ada/default.gpr
7-
EXTRA_DIST+= wrapper/Ada/gnat.adc
7+
EXTRA_DIST+= wrapper/Ada/restricted.adc
88
EXTRA_DIST+= wrapper/Ada/ada_binding.c
99
EXTRA_DIST+= wrapper/Ada/tls_client_main.adb
1010
EXTRA_DIST+= wrapper/Ada/tls_client.adb

wrapper/Ada/tls_server.adb

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -122,10 +122,10 @@ package body Tls_Server with SPARK_Mode is
122122
Identity_String : constant String := "Client_identity";
123123
-- Test key in hex is 0x1a2b3c4d, in decimal 439,041,101
124124
Key_String : constant String :=
125-
Character'Val (26)
126-
& Character'Val (43)
127-
& Character'Val (60)
128-
& Character'Val (77);
125+
(Character'Val (26),
126+
Character'Val (43),
127+
Character'Val (60),
128+
Character'Val (77));
129129
-- These values are aligned with test values in wolfssl/wolfssl/test.h
130130
-- and wolfssl-examples/psk/server-psk.c for testing interoperability.
131131

0 commit comments

Comments
 (0)