File: wolfssl.ads

package info (click to toggle)
wolfssl 5.8.4-1
  • links: PTS
  • area: main
  • in suites: forky, sid
  • size: 117,604 kB
  • sloc: ansic: 1,584,954; asm: 481,206; sh: 11,586; cs: 6,596; xml: 3,878; perl: 3,291; makefile: 2,058; ada: 1,891; javascript: 748; python: 636; cpp: 131; ruby: 118; objc: 80; tcl: 73
file content (694 lines) | stat: -rw-r--r-- 30,861 bytes parent folder | download | duplicates (5)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
-- wolfssl.ads
--
-- Copyright (C) 2006-2023 wolfSSL Inc.
--
-- This file is part of wolfSSL.
--
-- wolfSSL is free software; you can redistribute it and/or modify
-- it under the terms of the GNU General Public License as published by
-- the Free Software Foundation; either version 2 of the License, or
-- (at your option) any later version.
--
-- wolfSSL is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-- GNU General Public License for more details.
--
-- You should have received a copy of the GNU General Public License
-- along with this program; if not, write to the Free Software
-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
--

with GNAT.Sockets;
with Interfaces.C.Strings;

--  This package is annotated "with SPARK_Mode" that SPARK can verify
--  the API of this package is used correctly.
package WolfSSL with SPARK_Mode is

   type Subprogram_Result is new Integer;
   Success : constant Subprogram_Result;
   Failure : constant Subprogram_Result;

   function Initialize return Subprogram_Result;
   --  Initializes the wolfSSL library for use. Must be called once per
   --  application and before any other call to the library.

   function Finalize return Subprogram_Result;
   --  Un-initializes the wolfSSL library from further use.
   --  Doesn't have to be called, though it will free any resources
   --  used by the library.

   subtype unsigned is Interfaces.C.unsigned;

   subtype char_array is Interfaces.C.char_array;  --  Remove?
   subtype chars_ptr is Interfaces.C.Strings.chars_ptr;

   subtype Byte_Type  is Interfaces.C.char;
   subtype Byte_Index is Interfaces.C.size_t range 0 .. 16_000;
   subtype Byte_Array is Interfaces.C.char_array;

   type Context_Type is limited private;
   --  Instances of this type are called SSL Contexts.

   function Is_Valid (Context : Context_Type) return Boolean;
   --  Indicates if the SSL Context has successfully been initialized.
   --  If initialized, the SSL Context has allocated resources
   --  that needs to be deallocated before application exit.

   type Method_Type is limited private;

   function TLSv1_2_Server_Method return Method_Type;
   --  This function is used to indicate that the application is a server
   --  and will only support the TLS 1.2 protocol.

   function TLSv1_2_Client_Method return Method_Type;
   --  This function is used to indicate that the application is a client
   --  and will only support the TLS 1.2 protocol.

   function TLSv1_3_Server_Method return Method_Type;
   --  This function is used to indicate that the application is a server
   --  and will only support the TLS 1.3 protocol.

   function TLSv1_3_Client_Method return Method_Type;
   --  This function is used to indicate that the application is a client
   --  and will only support the TLS 1.3 protocol.

   function DTLSv1_2_Server_Method return Method_Type;
   --  This function is used to indicate that the application is a server
   --  and will only support the DTLS 1.2 protocol.

   function DTLSv1_2_Client_Method return Method_Type;
   --  This function is used to indicate that the application is a client
   --  and will only support the DTLS 1.2 protocol.

   function DTLSv1_3_Server_Method return Method_Type;
   --  This function is used to indicate that the application is a server
   --  and will only support the DTLS 1.3 protocol.

   function DTLSv1_3_Client_Method return Method_Type;
   --  This function is used to indicate that the application is a client
   --  and will only support the DTLS 1.3 protocol.

   procedure Create_Context (Method  : Method_Type;
                             Context : out Context_Type);
   --  This function creates a new SSL context, taking a desired SSL/TLS
   --  protocol method for input.
   --  If successful Is_Valid (Context) = True, otherwise False.

   procedure Free (Context : in out Context_Type) with
      Pre  => Is_Valid (Context),
      Post => not Is_Valid (Context);
   --  This function frees an allocated SSL Context object.

   type Mode_Type is private;

   function "or" (Left, Right : Mode_Type) return Mode_Type;

   Verify_None : constant Mode_Type;
   --  Client mode: the client will not verify the certificate received
   --  from the server and the handshake will continue as normal.
   --
   --  Server mode: the server will not send a certificate request to
   --  the client. As such, client verification will not be enabled.

   Verify_Peer : constant Mode_Type;
   --  Client mode: the client will verify the certificate received from
   --  the server during the handshake. This is turned on by default
   --  in wolfSSL, therefore, using this option has no effect.
   --
   --  Server mode: the server will send a certificate request to
   --  the client and verify the client certificate received.

   Verify_Fail_If_No_Peer_Cert : constant Mode_Type;
   --  Client mode: no effect when used on the client side.
   --
   --  Server mode: the verification will fail on the server side if
   --  the client fails to send a certificate when requested to do so
   --  (when using Verify_Peer on the SSL server).

   Verify_Client_Once : constant Mode_Type;

   Verify_Post_Handshake : constant Mode_Type;

   Verify_Fail_Except_Psk : constant Mode_Type;
   --  Client mode: no effect when used on the client side.
   --
   --  Server mode: the verification is the same as
   --  Verify_Fail_If_No_Peer_Cert except in the case of a PSK connection.
   --  If a PSK connection is being made then the connection
   --  will go through without a peer cert.

   Verify_Default : constant Mode_Type;

   procedure Set_Verify (Context : Context_Type;
                         Mode    : Mode_Type) with
      Pre => Is_Valid (Context);
   --  This function sets the verification method for remote peers

   function Get_Verify (Context : Context_Type) return Mode_Type;

   type File_Format is private;

   Format_Asn1    : constant File_Format;
   Format_Pem     : constant File_Format;
   Format_Default : constant File_Format;

   function Use_Certificate_File (Context : Context_Type;
                                  File    : String;
                                  Format  : File_Format)
                                  return Subprogram_Result with
      Pre => Is_Valid (Context);
   --  This function loads a certificate file into the SSL context.
   --  The file is provided by the file argument. The format argument
   --  specifies the format type of the file, either ASN1 or
   --  PEM file types. Please see the examples for proper usage.

   function Use_Certificate_Buffer (Context : Context_Type;
                                    Input   : char_array;
                                    Format  : File_Format)
                                    return Subprogram_Result with
      Pre => Is_Valid (Context);
   --  This function loads a certificate buffer into the SSL Context.
   --  It behaves like the non-buffered version (Use_Certificate_File),
   --  only differing in its ability to be called with a buffer as input
   --  instead of a file. The buffer is provided by the Input argument.
   --  Format specifies the format type of the buffer; ASN1 or PEM.
   --  Please see the examples for proper usage.

   function Use_Private_Key_File (Context : Context_Type;
                                  File    : String;
                                  Format  : File_Format)
                                  return Subprogram_Result with
      Pre => Is_Valid (Context);
   --  This function loads a private key file into the SSL context.
   --  The file is provided by the File argument. The Format argument
   --  specifies the format type of the file - ASN1 or PEM.
   --  Please see the examples for proper usage.

   function Use_Private_Key_Buffer (Context : Context_Type;
                                    Input   : Byte_Array;
                                    Format  : File_Format)
                                    return Subprogram_Result with
      Pre => Is_Valid (Context);
   --  This function loads a private key buffer into the SSL Context.
   --  It behaves like the non-buffered version (Use_Private_Key_File),
   --  only differing in its ability to be called with a buffer as input
   --  instead of a file. The buffer is provided by the Input argument.
   --  Format specifies the format type of the buffer; ASN1 or PEM.
   --  Please see the examples for proper usage.

   function Load_Verify_Locations (Context : Context_Type;
                                   File    : String;
                                   Path    : String)
                                   return Subprogram_Result with
      Pre => Is_Valid (Context);
   --  This function loads PEM-formatted CA certificate files into
   --  the SSL context. These certificates will be treated as trusted
   --  root certificates and used to verify certs received from peers
   --  during the SSL handshake. The root certificate file,
   --  provided by the File argument, may be a single certificate or
   --  a file containing multiple certificates. If multiple CA certs
   --  are included in the same file, wolfSSL will load them in the same
   --  order they are presented in the file. The path argument is
   --  a pointer to the name of a directory that contains certificates
   --  of trusted root CAs. If the value of File is not empty "",
   --  path may be specified as "" if not needed. If path is specified
   --  and NO_WOLFSSL_DIR was not defined when building the library,
   --  wolfSSL will load all CA certificates located in the given
   --  directory. This function will attempt to load all files in
   --  the directory. This function expects PEM formatted CERT_TYPE file
   --  with header "--BEGIN CERTIFICATE--".

   function Load_Verify_Buffer (Context : Context_Type;
                                Input   : Byte_Array;
                                Format  : File_Format)
                                return Subprogram_Result with
      Pre => Is_Valid (Context);
   --  This function loads a CA certificate buffer into the SSL
   --  Context. It behaves like the non-buffered version, only differing
   --  in its ability to be called with a buffer as input instead of
   --  a file. The buffer is provided by the Input argument.
   --  Format specifies the format type of the buffer; ASN1 or PEM.
   --  More than one CA certificate may be loaded
   --  per buffer as long as the format is in PEM.
   --  Please see the examples for proper usage.

   type WolfSSL_Type is limited private;
   --  Instances of this type are called SSL Sessions.

   function Is_Valid (Ssl : WolfSSL_Type) return Boolean;
   --  Indicates if the SSL Session has successfully been initialized.
   --  If initialized, the SSL Session has allocated resources
   --  that needs to be deallocated before application exit.

   procedure Create_WolfSSL (Context : Context_Type;
                             Ssl     : out WolfSSL_Type) with
      Pre => Is_Valid (Context);
   --  This function creates a new SSL session, taking an already created
   --  SSL context as input.
   --  If successful Is_Valid (Ssl) = True, otherwise False.

   function Use_Certificate_File (Ssl     : WolfSSL_Type;
                                  File    : String;
                                  Format  : File_Format)
                                  return Subprogram_Result with
      Pre => Is_Valid (Ssl);
   --  This function loads a certificate file into the SSL session.
   --  The certificate file is provided by the file argument.
   --  The format argument specifies the format type of the file
   --  either ASN1 or PEM.

   function Use_Certificate_Buffer (Ssl     : WolfSSL_Type;
                                    Input   : char_array;
                                    Format  : File_Format)
                                    return Subprogram_Result with
      Pre => Is_Valid (Ssl);
   --  This function loads a certificate buffer into the SSL session
   --  object. It behaves like the non-buffered version, only differing
   --  in its ability to be called with a buffer as input instead
   --  of a file. The buffer is provided by the Input argument.
   --  Format specifies the format type of the buffer; ASN1 or PEM.
   --  Please see the examples for proper usage.

   function Use_Private_Key_File (Ssl     : WolfSSL_Type;
                                  File    : String;
                                  Format  : File_Format)
                                  return Subprogram_Result with
      Pre => Is_Valid (Ssl);
   --  This function loads a private key file into the SSL session.
   --  The key file is provided by the File argument. The Format argument
   --  specifies the format type of the file - ASN1 or PEM.

   function Use_Private_Key_Buffer (Ssl     : WolfSSL_Type;
                                    Input   : Byte_Array;
                                    Format  : File_Format)
                                    return Subprogram_Result with
      Pre => Is_Valid (Ssl);
   --  This function loads a private key buffer into the SSL session
   --  object. It behaves like the non-buffered version, only differing
   --  in its ability to be called with a buffer as input instead
   --  of a file. The buffer is provided by the Input argument.
   --  Format specifies the format type of the buffer; ASN1 or PEM.
   --  Please see the examples for proper usage.

   function DTLS_Set_Peer
     (Ssl     : WolfSSL_Type;
      Address : GNAT.Sockets.Sock_Addr_Type)
      return Subprogram_Result with
     Pre => Is_Valid (Ssl);
   --  This function wraps the corresponding WolfSSL C function to allow
   --  clients to use Ada socket types when implementing a DTLS client.

   type PSK_Client_Callback is access function
     (Ssl            : WolfSSL_Type;
      Hint           : chars_ptr;
      Identity       : chars_ptr;
      Id_Max_Length  : unsigned;
      Key            : chars_ptr;
      Key_Max_Length : unsigned)
      return unsigned with
     Convention => C;
     --  Return value is the key length on success or zero on error.
     --  parameters:
     --  Ssl - Pointer to the wolfSSL structure
     --  Hint - A stored string that could be displayed to provide a
     --         hint to the user.
     --  Identity - The ID will be stored here.
     --  Id_Max_Length - Size of the ID buffer.
     --  Key - The key will be stored here.
     --  Key_Max_Length - The max size of the key.
     --
     --  The implementation of this callback will need `SPARK_Mode => Off`
     --  since it will require the code to use the C memory model.

   procedure Set_PSK_Client_Callback
     (Ssl      : WolfSSL_Type;
      Callback : PSK_Client_Callback) with
     Pre => Is_Valid (Ssl);
     -- Sets the PSK client side callback.

   
   type PSK_Server_Callback is access function
     (Ssl            : WolfSSL_Type;
      Identity       : chars_ptr;
      Key            : chars_ptr;
      Key_Max_Length : unsigned)
      return unsigned with
     Convention => C;
     --  Return value is the key length on success or zero on error.
     --  PSK server callback parameters:
     --  Ssl - Reference to the wolfSSL structure
     --  Identity - The ID will be stored here. 
     --  Key - The key will be stored here.
     --  Key_Max_Length - The max size of the key.
     --
     --  The implementation of this callback will need `SPARK_Mode => Off`
     --  since it will require the code to use the C memory model.

   procedure Set_PSK_Server_Callback
     (Ssl      : WolfSSL_Type;
      Callback : PSK_Server_Callback) with
     Pre => Is_Valid (Ssl);
     -- Sets the PSK Server side callback.
   
   procedure Set_Context_PSK_Server_Callback
     (Context  : Context_Type;
      Callback : PSK_Server_Callback) with
     Pre => Is_Valid (Context);
     --  Sets the PSK callback for the server side in the WolfSSL Context. 
   
   function Attach (Ssl    : WolfSSL_Type;
                    Socket : Integer)
                    return Subprogram_Result with
      Pre => Is_Valid (Ssl);
   --  Attach wolfSSL to the socket.
   --
   --  This function assigns a file descriptor (Socket) as
   --  the input/output facility for the SSL connection.
   --  Typically this will be a socket file descriptor.

   procedure Keep_Arrays (Ssl : WolfSSL_Type) with
      Pre => Is_Valid (Ssl);
   --  Normally, at the end of the SSL handshake, wolfSSL frees
   --  temporary arrays. Calling this function before the handshake
   --  begins will prevent wolfSSL from freeing temporary arrays.
   --  Temporary arrays may be needed for things such as
   --  wolfSSL_get_keys() or PSK hints. When the user is done with
   --  temporary arrays, either Free_Arrays(..) may be called to free
   --  the resources immediately, or alternatively the resources will
   --  be freed when the associated SSL object is freed.

   procedure Free_Arrays (Ssl : WolfSSL_Type) with
      Pre => Is_Valid (Ssl);
   --  Normally, at the end of the SSL handshake, wolfSSL frees temporary
   --  arrays. If Keep_Arrays(..) has been called before the handshake,
   --  wolfSSL will not free temporary arrays. This function explicitly
   --  frees temporary arrays and should be called when the user is done
   --  with temporary arrays and does not want to wait for the SSL object
   --  to be freed to free these resources.

   function Accept_Connection (Ssl : WolfSSL_Type)
                               return Subprogram_Result with
      Pre => Is_Valid (Ssl);
   --  The name of this function is not Accept (..) because the word
   --  "accept" is a reserved keyword in the Ada language.
   --
   --  This function is called on the server side and waits for an
   --  SSL client to initiate the SSL/TLS handshake. When this function
   --  is called, the underlying communication channel has already been
   --  set up. This function works with both blocking and
   --  non-blocking I/O. When the underlying I/O is non-blocking,
   --  Accept_Connection (..) will return when the underlying I/O could
   --  not satisfy the needs of Accept_Connection (..) to continue
   --  the handshake. In this case, a call to Get_Error(..) will
   --  yield either Error_Want_Read or Error_Want_Write.
   --  The calling process must then repeat the call to
   --  Accept_Connection (..) when data is available to read and
   --  wolfSSL will pick up where it left off. When using a
   --  non_blocking socket, nothing needs to be done, but select() can
   --  be used to check for the required condition.
   --  If the underlying I/O is blocking, Accept_Connection (..) will
   --  only return once the handshake has been finished or
   --  an error occurred.

   --  This record type has discriminants with default values to be able
   --  to compile this code under the restriction No Secondary Stack.
   type Read_Result (Success : Boolean := False;
                     Last    : Byte_Index := Byte_Index'Last) is record
      case Success is
         when True  => Buffer : Byte_Array (1 .. Last);
         when False => Code : Subprogram_Result; --  Error code
      end case;
   end record;

   function Read (Ssl : WolfSSL_Type) return Read_Result with
      Pre => Is_Valid (Ssl);
   --  This function reads a number of bytes from the SSL session (ssl)
   --  internal read buffer into the buffer data. The bytes read are
   --  removed from the internal receive buffer.
   --  If necessary Read(..) will negotiate an SSL/TLS session
   --  if the handshake has not already
   --  been performed yet by Connect(..) or Accept_Connection (..).
   --  The SSL/TLS protocol uses SSL records which have a maximum size
   --  of 16kB (the max record size can be controlled by the
   --  MAX_RECORD_SIZE define in /wolfssl/internal.h). As such, wolfSSL
   --  needs to read an entire SSL record internally before it is able
   --  to process and decrypt the record. Because of this, a call to
   --  Read(..) will only be able to return the maximum buffer
   --  size which has been decrypted at the time of calling. There may
   --  be additional not-yet-decrypted data waiting in the internal
   --  wolfSSL receive buffer which will be retrieved and decrypted with
   --  the next call to Read(..).

   --  This record type has discriminants with default values to be able
   --  to compile this code under the restriction No Secondary Stack.
   type Write_Result (Success : Boolean := False) is record
      case Success is
         when True  => Bytes_Written : Byte_Index;
         when False => Code : Subprogram_Result; --  Error code
      end case;
   end record;

   function Write (Ssl  : WolfSSL_Type;
                   Data : Byte_Array) return Write_Result with
      Pre => Is_Valid (Ssl);
   --  The number of bytes written is returned.
   --  This function writes bytes from the buffer, Data,
   --  to the SSL connection, ssl. If necessary, Write(..) will
   --  negotiate an SSL/TLS session if the handshake has not already
   --  been performed yet by Connect(..) or Accept_Connection(..).
   --  Write(..) works with both blocking and non-blocking I/O.
   --  When the underlying I/O is non-blocking, Write(..) will return
   --  when the underlying I/O could not satisfy the needs of Write(..)
   --  to continue. In this case, a call to Get_Error(..) will
   --  yield either Error_Want_Read or Error_Want_Write.
   --  The calling process must then repeat the call to Write(..)
   --  when the underlying I/O is ready. If the underlying I/O is
   --  blocking, Write(..) will only return once the buffer data
   --  has been completely written or an error occurred.

   function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result with
      Pre => Is_Valid (Ssl);
   --  This function shuts down an active SSL/TLS connection using
   --  the SSL session, ssl. This function will try to send a
   --  "close notify" alert to the peer. The calling application can
   --  choose to wait for the peer to send its "close notify" alert
   --  in response or just go ahead and shut down the underlying
   --  connection after directly calling wolfSSL_shutdown (to save
   --  resources). Either option is allowed by the TLS specification.
   --  If the underlying connection will be used again in the future,
   --  the complete two_directional shutdown procedure must be performed
   --  to keep synchronization intact between the peers.
   --  Shutdown(..) works with both blocking and non_blocking I/O.
   --  When the underlying I/O is non_blocking, Shutdown(..) will
   --  return an error if the underlying I/O could not satisfy the needs
   --  of Shutdown(..) to continue. In this case, a call to
   --  Get_Error(..) will yield either Error_Want_Read or
   --  Error_Want_Write. The calling process must then repeat
   --  the call to Shutdown() when the underlying I/O is ready.

   procedure Free (Ssl : in out WolfSSL_Type) with
      Pre  => Is_Valid (Ssl),
      Post => not Is_Valid (Ssl);
   --  Frees the resources allocated by the SSL session object.

   function Connect (Ssl : WolfSSL_Type) return Subprogram_Result with
      Pre => Is_Valid (Ssl);
   --  This function is called on the client side and initiates
   --  an SSL/TLS handshake with a server. When this function is called,
   --  the underlying communication channel has already been set up.
   --  Connect(..) works with both blocking and non_blocking I/O.
   --  When the underlying I/O is non_blocking, Connect(..) will
   --  return when the underlying I/O could not satisfy the needs
   --  of wolfSSL_connect to continue the handshake. In this case,
   --  a call to Get_Error(..) will yield either
   --  Error_Want_Read or SSL_ERROR_WANT_WRITE. The calling process
   --  must then repeat the call to Connect(..) when
   --  the underlying I/O is ready and wolfSSL will pick up where
   --  it left off. When using a non_blocking socket, nothing needs
   --  to be done, but select() can be used to check for the required
   --  condition. If the underlying I/O is blocking, Connect(..)
   --  will only return once the handshake has been finished or an error
   --  occurred. wolfSSL takes a different approach to certificate
   --  verification than OpenSSL does. The default policy for the client
   --  is to verify the server, this means that if you don't load CAs
   --  to verify the server you'll get a connect error,
   --  unable to verify. It you want to mimic OpenSSL behavior
   --  of having SSL_connect succeed even if verifying the server fails
   --  and reducing security you can do this by calling:
   --  Set_Verify (Ctx, Verify_None, 0); before calling
   --  Create_WolfSSL(...); Though it's not recommended.

   type Error_Code is new Integer;

   Error_Want_Read  : constant Error_Code;
   Error_Want_Write : constant Error_Code;

   function Get_Error (Ssl    : WolfSSL_Type;
                       Result : Subprogram_Result) return Error_Code;
   --  This function returns a unique error code describing why
   --  the previous API function call (Connect, Accept_Connection,
   --  Read, Write, etc.) resulted in an error return code.
   --  After Get_Error is called and returns the unique error code,
   --  wolfSSL_ERR_error_string() may be called to get a human readable
   --  error string.

   subtype Error_Message_Index is Natural range 0 .. 80;
   --  The default error message length is 80 in WolfSSL unless
   --  configured to another value. See the result
   --  of the Max_Error_Size function.

   type Error_Message (Last : Error_Message_Index := 0) is record
      Text : String (1 .. Last);
   end record;

   function Error (Code : Error_Code) return Error_Message;
   --  This function converts an error code returned by Get_Error(..)
   --  into a more human readable error string. Code is the error code
   --  returned by Get_error(). The maximum length of error strings is
   --  80 characters by default, as defined by MAX_ERROR_SZ
   --  is wolfssl/wolfcrypt/error.h.

   function Max_Error_Size return Natural;
   --  Returns the value of the defined MAX_ERROR_SZ integer
   --  in wolfssl/wolfcrypt/error.h.

private
   pragma SPARK_Mode (Off);

   subtype int is Interfaces.C.int; use type int;

   type Opaque_Method  is limited null record;
   type Opaque_Context is limited null record;
   type Opaque_WolfSSL is limited null record;

   --  Access-to-object types with convention C uses the same amount of
   --  memory for storing pointers as is done in the C programming
   --  language. The following access type definitions are used in
   --  the Ada binding to the WolfSSL library:
   type Context_Type is access Opaque_Context with Convention => C;
   type Method_Type  is access Opaque_Method  with Convention => C;
   type WolfSSL_Type is access Opaque_WolfSSL with Convention => C;

   subtype Unsigned_32 is Interfaces.Unsigned_32; use type Unsigned_32;

   type Mode_Type is new Unsigned_32;

   --  The following imported subprograms are used to initialize
   --  the constants defined in the public part of this package
   --  specification. They cannot therefore be moved to the body
   --  of this package.

   function WolfSSL_Verify_None return int with
     Convention    => C,
     External_Name => "get_wolfssl_verify_none",
     Import        => True;

   function WolfSSL_Verify_Peer return int with
     Convention    => C,
     External_Name => "get_wolfssl_verify_peer",
     Import        => True;

   function WolfSSL_Verify_Fail_If_No_Peer_Cert return int with
     Convention    => C,
     External_Name => "get_wolfssl_verify_fail_if_no_peer_cert",
     Import        => True;

   function WolfSSL_Verify_Client_Once return int with
     Convention    => C,
     External_Name => "get_wolfssl_verify_client_once",
     Import        => True;

   function WolfSSL_Verify_Post_Handshake return int with
     Convention    => C,
     External_Name => "get_wolfssl_verify_post_handshake",
     Import        => True;

   function WolfSSL_Verify_Fail_Except_Psk return int with
     Convention    => C,
     External_Name => "get_wolfssl_verify_fail_except_psk",
     Import        => True;

   function WolfSSL_Verify_Default return int with
     Convention    => C,
     External_Name => "get_wolfssl_verify_default",
     Import        => True;

   Verify_None : constant Mode_Type := Mode_Type (WolfSSL_Verify_None);
   Verify_Peer : constant Mode_Type := Mode_Type (WolfSSL_Verify_Peer);

   Verify_Fail_If_No_Peer_Cert : constant Mode_Type :=
     Mode_Type (WolfSSL_Verify_Fail_If_No_Peer_Cert);

   Verify_Client_Once : constant Mode_Type :=
     Mode_Type (WolfSSL_Verify_Client_Once);

   Verify_Post_Handshake : constant Mode_Type :=
     Mode_Type (WolfSSL_Verify_Post_Handshake);

   Verify_Fail_Except_Psk : constant Mode_Type :=
     Mode_Type (WolfSSL_Verify_Fail_Except_Psk);

   Verify_Default : constant Mode_Type :=
     Mode_Type (WolfSSL_Verify_Default);

   type File_Format is new Unsigned_32;

   function WolfSSL_Filetype_Asn1 return int with
     Convention    => C,
     External_Name => "get_wolfssl_filetype_asn1",
     Import        => True;

   function WolfSSL_Filetype_Pem return int with
     Convention    => C,
     External_Name => "get_wolfssl_filetype_pem",
     Import        => True;

   function WolfSSL_Filetype_Default return int with
     Convention    => C,
     External_Name => "get_wolfssl_filetype_default",
     Import        => True;

   Format_Asn1 : constant File_Format :=
     File_Format (WolfSSL_Filetype_Asn1);

   Format_Pem : constant File_Format :=
     File_Format (WolfSSL_Filetype_Pem);

   Format_Default : constant File_Format :=
     File_Format (WolfSSL_Filetype_Default);

   function Get_WolfSSL_Success return int with
     Convention    => C,
     External_Name => "get_wolfssl_success",
     Import        => True;

   function Get_WolfSSL_Failure return int with
     Convention    => C,
     External_Name => "get_wolfssl_failure",
     Import        => True;

   Success : constant Subprogram_Result :=
      Subprogram_Result (Get_WolfSSL_Success);

   Failure : constant Subprogram_Result :=
      Subprogram_Result (Get_WolfSSL_Failure);

   function Get_WolfSSL_Error_Want_Read return int with
     Convention    => C,
     External_Name => "get_wolfssl_error_want_read",
     Import        => True;

   function Get_WolfSSL_Error_Want_Write return int with
     Convention    => C,
     External_Name => "get_wolfssl_error_want_write",
     Import        => True;

   Error_Want_Read  : constant Error_Code :=
      Error_Code (Get_WolfSSL_Error_Want_Read);

   Error_Want_Write : constant Error_Code :=
      Error_Code (Get_WolfSSL_Error_Want_Write);

end WolfSSL;