@@ -29,6 +29,7 @@ formal verification). To formally verify the Ada code in this repository
2929open the client.gpr with GNAT Studio and then select
3030SPARK -> Prove All Sources and use Proof Level 2.
3131
32+ ```
3233Summary of SPARK analysis
3334=========================
3435
@@ -47,6 +48,7 @@ Termination . . .
4748Concurrency . . . . . .
4849---------------------------------------------------------------------------------------------------------------
4950Total 172 17 (10%) . 155 (90%) . .
51+ ```
5052
5153## Compiler and Build System installation
5254
@@ -73,6 +75,13 @@ cd obj/
7375./tls_client_main 127.0.0.1
7476```
7577
78+ On Windows, build the executables with:
79+ ``` sh
80+ gprbuild -XOS=Windows default.gpr
81+ gprbuild -XOS=Windows client.gpr
82+ ```
83+
84+
7685### GNAT FSF Compiler and GPRBuild manual installation
7786In May 2022 AdaCore announced the end of the GNAT Community releases.
7887Pre-built binaries for the GNAT FSF compiler and GPRBuild can be
@@ -82,18 +91,14 @@ Make sure the executables for the compiler and GPRBuild are on the PATH
8291and use gprbuild to build the source code.
8392
8493## Files
85- The file c_tls_client_main.c and c_tls_server_main.c are the TLS v1.3
86- server and client examples using the WolfSSL library implemented using
87- the C programming language.
88-
89- The translation of the C client example into the Ada/SPARK programming
90- language can be found in the files:
94+ The TLS v1.3 client example in the Ada/SPARK programming language
95+ using the WolfSSL library can be found in the files:
9196tls_client_main.adb
9297tls_client.ads
9398tls_client.adb
9499
95- The translation of the C server example into the Ada/SPARK programming
96- language can be found in the files:
100+ The TLS v1.3 server example in the Ada/SPARK programming language
101+ using the WolfSSL library can be found in the files:
97102tls_server_main.adb
98103tls_server.ads
99104tls_server.adb
0 commit comments