Test ran at 2025-07-26 00:44:22.253520+00:00

SOLUTION:
coap_spark=0.9.0: CoAP implementation formally verified with SPARK/Ada
Origin: commit 81401167ac44c9178de4e130b1bd83228d62a3d2 from https://github.com/mgrojo/coap_spark.git
Properties:
   Author: Manuel Gomez
   Build Switches: 
   Config set: wolfssl {STATIC_PSK := true}
   Configuration: no modifiers
   Description: CoAP implementation formally verified with SPARK/Ada
   License: Apache-2.0 OR GPL-2.0-or-later
   Long_Description: CoAP-SPARK is a library implementing the Constrained Application Protocol (CoAP)
as defined in
[RFC 7252](https://www.rfc-editor.org/rfc/rfc7252), developed in the SPARK 
language, the formally verified subset of the Ada programming language.

This version implements the client side of the protocol with some limitations:
- It does not support block-wise transfers.
- It does not support retransmission of messages.
- It only supports NoSec and PreSharedKey security modes.

See LICENSING for licensing information.

   Maintainer: Manuel Gomez <mgrojo@gmail.com>
   Maintainers_Logins: mgrojo
   Name: coap_spark
   Tag: spark
   Tag: coap
   Tag: iot
   Tag: protocol
   Version: 0.9.0
   Website: https://github.com/mgrojo/coap_spark
Dependencies (direct):
   gnatprove^14.1.1
   wolfssl^5.8.0
Dependencies (solution):
   gnatprove=14.1.1
   wolfssl=5.8.0
Dependencies (graph):
   coap_spark=0.9.0 --> gnatprove=14.1.1 (^14.1.1)
   coap_spark=0.9.0 --> wolfssl=5.8.0 (^5.8.0)


LOG:
[alr test] Testing coap_spark=0.9.0
[alr test] Spawning retrieval for remote crate: alr -d -n get coap_spark=0.9.0
Note: Deploying coap_spark=0.9.0...
Note: Deploying gnatprove=14.1.1...
#=#=#                                                                          
##O#-#                                                                         
##O=#  #                                                                       

                                                                           0.0%
#####                                                                      7.7%
########                                                                  12.0%
##########                                                                14.6%
#############                                                             18.8%
##################                                                        25.2%
#####################                                                     30.0%
##########################                                                36.9%
###############################                                           44.1%
####################################                                      51.0%
#########################################                                 58.2%
##############################################                            64.8%
####################################################                      72.6%
#####################################################                     74.6%
########################################################                  78.2%
##############################################################            86.7%
###################################################################       93.4%
######################################################################## 100.0%
Note: Deploying wolfssl=5.8.0...

coap_spark=0.9.0 successfully retrieved.
Dependencies were solved as follows:

   +b gnatprove 14.1.1 (new,binary)
   +  wolfssl   5.8.0  (new)
[alr test] Spawning default test for remote crate: alr -d -n build --release -- -cargs:Ada -gnatwn
Note: Building coap_spark=0.9.0/coap_spark.gpr...
Setup
   [mkdir]        object directory for project SPARKlib
   [mkdir]        object directory for project WolfSSL
   [mkdir]        library directory for project WolfSSL
   [mkdir]        object directory for project Coap_Spark
   [mkdir]        library directory for project Coap_Spark
Compile
   [Ada]          spark_sockets.adb
   [Ada]          spark_terminal.adb
   [Ada]          wolfssl.adb
   [C]            coding.c
   [C]            sm2.c
   [C]            ge_448.c
   [C]            logging.c
   [C]            ge_low_mem.c
   [C]            sp_c32.c
   [C]            wolfevent.c
   [C]            sha512.c
   [C]            sp_x86_64.c
   [C]            pkcs12.c
   [C]            asm.c
   [C]            sp_sm2_x86_64.c
   [C]            dh.c
   [C]            misc.c
   [C]            sha3.c
   [C]            wc_xmss_impl.c
   [C]            poly1305.c
   [C]            blake2s.c
   [C]            wc_xmss.c
   [C]            arc4.c
   [C]            falcon.c
   [C]            siphash.c
   [C]            md5.c
   [C]            wc_pkcs11.c
   [C]            sha256.c
   [C]            wolfmath.c
   [C]            sp_sm2_arm32.c
   [C]            sp_sm2_armthumb.c
   [C]            blake2b.c
   [C]            chacha.c
   [C]            cpuid.c
   [C]            asn.c
   [C]            sha.c
   [C]            wc_mlkem_poly.c
   [C]            des3.c
   [C]            rc2.c
   [C]            md2.c
   [C]            error.c
   [C]            kdf.c
   [C]            signature.c
   [C]            sp_sm2_c32.c
   [C]            fe_operations.c
   [C]            wc_lms_impl.c
   [C]            wc_encrypt.c
   [C]            wc_mlkem.c
   [C]            ext_xmss.c
   [C]            ascon.c
   [C]            sp_arm32.c
   [C]            ge_operations.c
   [C]            integer.c
   [C]            ext_mlkem.c
   [C]            hash.c
   [C]            sp_int.c
   [C]            cmac.c
   [C]            sp_sm2_cortexm.c
   [C]            fe_448.c
   [C]            sm4.c
   [C]            cryptocb.c
   [C]            random.c
   [C]            sakke.c
   [C]            ecc.c
   [C]            ed448.c
   [C]            wc_lms.c
   [C]            sp_c64.c
   [C]            eccsi.c
   [C]            dilithium.c
   [C]            ripemd.c
   [C]            curve448.c
   [C]            fe_low_mem.c
   [C]            rsa.c
   [C]            tfm.c
   [C]            dsa.c
   [C]            curve25519.c
   [C]            sm3.c
   [C]            wc_port.c
   [C]            compress.c
   [C]            pwdbased.c
   [C]            sphincs.c
   [C]            sp_arm64.c
   [C]            chacha20_poly1305.c
   [C]            sp_sm2_c64.c
   [C]            sp_cortexm.c
   [C]            ed25519.c
   [C]            memory.c
   [C]            ext_lms.c
   [C]            pkcs7.c
   [C]            camellia.c
   [C]            srp.c
   [C]            wc_dsp.c
   [C]            md4.c
   [C]            hmac.c
   [C]            hpke.c
   [C]            evp.c
   [C]            aes.c
   [C]            sp_armthumb.c
   [C]            sp_sm2_arm64.c
   [C]            sp_dsp32.c
   [C]            ecc_fp.c
   [C]            ssl_load.c
   [C]            ssl_bn.c
   [C]            ssl_misc.c
   [C]            dtls13.c
   [C]            dtls.c
   [C]            wolfio.c
   [C]            ssl_sess.c
   [C]            conf.c
   [C]            tls13.c
   [C]            tls.c
   [C]            x509.c
   [C]            ssl_certman.c
   [C]            ssl_p7p12.c
   [C]            bio.c
   [C]            keys.c
   [C]            ssl_asn1.c
   [C]            internal.c
   [C]            x509_str.c
   [C]            quic.c
   [C]            ssl_crypto.c
   [C]            ocsp.c
   [C]            sniffer.c
   [C]            pk.c
   [C]            ssl.c
   [C]            crl.c
   [C]            ada_binding.c
   [Ada]          spark-containers-formal-hashed_sets.adb
spark-containers-formal-hashed_sets.adb:7:06: error: "ADA.CONTAINERS.HASH_TABLES.GENERIC_FORMAL_OPERATIONS" is not a predefined library unit
spark-containers-formal-hashed_sets.adb:9:06: error: "ADA.CONTAINERS.HASH_TABLES.GENERIC_FORMAL_KEYS" is not a predefined library unit
spark-containers-formal-hashed_sets.ads:1301:29: (style) redundant parentheses [-gnatyz]

   compilation of spark-containers-formal-hashed_sets.adb failed

gprbuild: *** compilation phase failed
stderr: Command ["gprbuild", "-s", "-j0", "-p", "-P", "/Users/runner/work/alire-crates-ci/alire-crates-ci/test/cb5bb3a3-9089-4064-b96b-8d29f1f85579/coap_spark_0.9.0_81401167/coap_spark.gpr", "-cargs:Ada", "-gnatwn"] exited with code 4
ERROR: Command ["gprbuild", "-s", "-j0", "-p", "-P", "/Users/runner/work/alire-crates-ci/alire-crates-ci/test/cb5bb3a3-9089-4064-b96b-8d29f1f85579/coap_spark_0.9.0_81401167/coap_spark.gpr", "-cargs:Ada", "-gnatwn"] exited with code 4
stderr: ALIRE.CHECKED_ERROR
stderr: Command ["gprbuild", "-s", "-j0", "-p", "-P", "/Users/runner/work/alire-crates-ci/alire-crates-ci/test/cb5bb3a3-9089-4064-b96b-8d29f1f85579/coap_spark_0.9.0_81401167/coap_spark.gpr", "-cargs:Ada", "-gnatwn"] exited with code 4
stderr: raised ALIRE.CHECKED_ERROR : alire-stored-error:1
Load address: 0x100010000
Call stack traceback locations:
0x100d1c0cc 0x100d1c12c 0x100a7066c 0x1006b5568 0x10093a594 0x10093b4f4 0x10087933c 0x100877b08 0x10089b78c 0x1008fb56c 0x1008fa99c 0x10089b868 0x10089b950 0x10087800c 0x100878174 0x100081730 0x100081070 0x1000811e4 0x10011eb38 0x100129c78 0x1000129f8 0x100017a2c

stderr: ALIRE.ROOTS.BUILD._WRAPPED_STATEMENTS.BUILD_FAILED
stderr: alire-roots.adb:202
stderr: raised ALIRE.ROOTS.BUILD._WRAPPED_STATEMENTS.BUILD_FAILED : alire-roots.adb:202
Load address: 0x100010000
Call stack traceback locations:
0x100d1c0cc 0x100d1c12c 0x100879640 0x100877b08 0x10089b78c 0x1008fb56c 0x1008fa99c 0x10089b868 0x10089b950 0x10087800c 0x100878174 0x100081730 0x100081070 0x1000811e4 0x10011eb38 0x100129c78 0x1000129f8 0x100017a2c

ERROR: Compilation failed.