forked from wolfSSL/wolfssl
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.
This commit is contained in:
@ -13,10 +13,11 @@ code to zero-out stack frames used by subprograms.
|
|||||||
Unfortunately this works well for the primary stack but not
|
Unfortunately this works well for the primary stack but not
|
||||||
for the secondary stack. The GNAT User's Guide recommends
|
for the secondary stack. The GNAT User's Guide recommends
|
||||||
avoiding the secondary stack using the restriction
|
avoiding the secondary stack using the restriction
|
||||||
No_Secondary_Stack (see the GNAT configuration file gnat.adc
|
No_Secondary_Stack (see the GNAT configuration file restricted.adc
|
||||||
which instructs compilation of the WolfSSL Ada binding under
|
which instructs compilation of the WolfSSL Ada binding under
|
||||||
this restriction). Note, however, that the examples do make use of the
|
this restriction). Note, however, that the examples do make use of the
|
||||||
secondary stack.
|
secondary stack and the Alire project does not include this restriction, for
|
||||||
|
letting users of the library to define it at their level.
|
||||||
|
|
||||||
Portability: The WolfSSL Ada binding makes no usage of controlled types
|
Portability: The WolfSSL Ada binding makes no usage of controlled types
|
||||||
and has no dependency upon the Ada.Finalization package.
|
and has no dependency upon the Ada.Finalization package.
|
||||||
@ -25,11 +26,11 @@ the restriction No_Finalization. The WolfSSL Ada binding has
|
|||||||
been developed with maximum portability in mind.
|
been developed with maximum portability in mind.
|
||||||
|
|
||||||
Not only can the WolfSSL Ada binding be used in Ada applications but
|
Not only can the WolfSSL Ada binding be used in Ada applications but
|
||||||
also SPARK applications (a subset of the Ada language suitable
|
also SPARK applications (a subset of the Ada language suitable for
|
||||||
formal verification). To formally verify the Ada code in this repository
|
formal verification). To formally verify the Ada code in this repository
|
||||||
open the client.gpr with GNAT Studio and then select
|
open the examples.gpr with GNAT Studio and then select
|
||||||
SPARK -> Prove All Sources and use Proof Level 2. Or when using the command
|
SPARK -> Prove All Sources and use Proof Level 2. Or when using the command
|
||||||
line, use `gnatprove -Pclient.gpr --level=4 -j12` (`-j12` is there in
|
line, use `gnatprove -Pexamples.gpr --level=4 -j12` (`-j12` is there in
|
||||||
order to instruct the prover to use 12 CPUs if available).
|
order to instruct the prover to use 12 CPUs if available).
|
||||||
|
|
||||||
```
|
```
|
||||||
@ -83,7 +84,7 @@ and use gprbuild to build the source code.
|
|||||||
cd wrapper/Ada
|
cd wrapper/Ada
|
||||||
gprclean
|
gprclean
|
||||||
gprbuild default.gpr
|
gprbuild default.gpr
|
||||||
gprbuild client.gpr
|
gprbuild examples.gpr
|
||||||
|
|
||||||
cd obj/
|
cd obj/
|
||||||
./tls_server_main &
|
./tls_server_main &
|
||||||
@ -93,7 +94,7 @@ cd obj/
|
|||||||
On Windows, build the executables with:
|
On Windows, build the executables with:
|
||||||
```sh
|
```sh
|
||||||
gprbuild -XOS=Windows default.gpr
|
gprbuild -XOS=Windows default.gpr
|
||||||
gprbuild -XOS=Windows client.gpr
|
gprbuild -XOS=Windows examples.gpr
|
||||||
```
|
```
|
||||||
|
|
||||||
## Files
|
## Files
|
||||||
|
@ -11,17 +11,19 @@ project Default is
|
|||||||
"../../src",
|
"../../src",
|
||||||
"../../wolfcrypt/src");
|
"../../wolfcrypt/src");
|
||||||
|
|
||||||
-- Don't build the tls client application because it makes use
|
-- Don't build the tls application examples because they make use
|
||||||
-- of the Secondary Stack due to usage of the Ada.Command_Line
|
-- of the Secondary Stack due to usage of the Ada.Command_Line
|
||||||
-- package. All other Ada source code does not use the secondary stack.
|
-- package. All other Ada source code does not use the secondary stack.
|
||||||
for Excluded_Source_Files use ("tls_client_main.adb",
|
for Excluded_Source_Files use
|
||||||
"tls_client.ads",
|
("tls_client_main.adb",
|
||||||
"tls_client.adb");
|
"tls_client.ads",
|
||||||
|
"tls_client.adb",
|
||||||
|
"tls_server_main.adb",
|
||||||
|
"tls_server.ads",
|
||||||
|
"tls_server.adb");
|
||||||
|
|
||||||
for Object_Dir use "obj";
|
for Object_Dir use "obj";
|
||||||
|
|
||||||
for Main use ("tls_server_main.adb");
|
|
||||||
|
|
||||||
package Naming is
|
package Naming is
|
||||||
for Spec_Suffix ("C") use ".h";
|
for Spec_Suffix ("C") use ".h";
|
||||||
end Naming;
|
end Naming;
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
project Client is
|
project Examples is
|
||||||
type OS_Kind is ("Windows", "Linux_Or_Mac");
|
type OS_Kind is ("Windows", "Linux_Or_Mac");
|
||||||
|
|
||||||
OS : OS_Kind := external ("OS", "Linux_Or_Mac");
|
OS : OS_Kind := external ("OS", "Linux_Or_Mac");
|
||||||
@ -12,7 +12,7 @@ project Client is
|
|||||||
|
|
||||||
for Object_Dir use "obj";
|
for Object_Dir use "obj";
|
||||||
|
|
||||||
for Main use ("tls_client_main.adb");
|
for Main use ("tls_server_main.adb", "tls_client_main.adb");
|
||||||
|
|
||||||
package Naming is
|
package Naming is
|
||||||
for Spec_Suffix ("C") use ".h";
|
for Spec_Suffix ("C") use ".h";
|
||||||
@ -75,4 +75,4 @@ project Client is
|
|||||||
for Switches ("Ada") use ("-Es"); -- To include stack traces.
|
for Switches ("Ada") use ("-Es"); -- To include stack traces.
|
||||||
end Binder;
|
end Binder;
|
||||||
|
|
||||||
end Client;
|
end Examples;
|
@ -4,7 +4,7 @@
|
|||||||
|
|
||||||
EXTRA_DIST+= wrapper/Ada/README.md
|
EXTRA_DIST+= wrapper/Ada/README.md
|
||||||
EXTRA_DIST+= wrapper/Ada/default.gpr
|
EXTRA_DIST+= wrapper/Ada/default.gpr
|
||||||
EXTRA_DIST+= wrapper/Ada/gnat.adc
|
EXTRA_DIST+= wrapper/Ada/restricted.adc
|
||||||
EXTRA_DIST+= wrapper/Ada/ada_binding.c
|
EXTRA_DIST+= wrapper/Ada/ada_binding.c
|
||||||
EXTRA_DIST+= wrapper/Ada/tls_client_main.adb
|
EXTRA_DIST+= wrapper/Ada/tls_client_main.adb
|
||||||
EXTRA_DIST+= wrapper/Ada/tls_client.adb
|
EXTRA_DIST+= wrapper/Ada/tls_client.adb
|
||||||
|
@ -122,10 +122,10 @@ package body Tls_Server with SPARK_Mode is
|
|||||||
Identity_String : constant String := "Client_identity";
|
Identity_String : constant String := "Client_identity";
|
||||||
-- Test key in hex is 0x1a2b3c4d, in decimal 439,041,101
|
-- Test key in hex is 0x1a2b3c4d, in decimal 439,041,101
|
||||||
Key_String : constant String :=
|
Key_String : constant String :=
|
||||||
Character'Val (26)
|
(Character'Val (26),
|
||||||
& Character'Val (43)
|
Character'Val (43),
|
||||||
& Character'Val (60)
|
Character'Val (60),
|
||||||
& Character'Val (77);
|
Character'Val (77));
|
||||||
-- These values are aligned with test values in wolfssl/wolfssl/test.h
|
-- These values are aligned with test values in wolfssl/wolfssl/test.h
|
||||||
-- and wolfssl-examples/psk/server-psk.c for testing interoperability.
|
-- and wolfssl-examples/psk/server-psk.c for testing interoperability.
|
||||||
|
|
||||||
|
Reference in New Issue
Block a user