Test ran at 2025-07-24 12:38:36.786690+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 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... 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 Coap_Spark [mkdir] library directory for project Coap_Spark Compile [Ada] spark-higher_order.adb [Ada] spark-containers.ads [Ada] spark-conversions.ads [Ada] spark-pointers.ads [Ada] spark-pointers-abstract_sets.adb [Ada] spark-containers-formal-vectors.adb [Ada] spark.ads [Ada] spark-containers-functional-base.adb [Ada] spark-containers-formal-unbounded_hashed_sets.adb spark-pointers-abstract_sets.ads:16:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-formal-doubly_linked_lists.adb [Ada] spark-containers-formal-hashed_maps.adb spark-containers-formal-vectors.ads:34:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] spark-containers-formal-vectors.ads:921:45: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-big_integers.ads [Ada] spark-containers-functional-maps.adb spark-containers-formal-doubly_linked_lists.ads:28:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] spark-containers-formal-doubly_linked_lists.ads:1658:45: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-formal-unbounded_hashed_maps.adb spark-containers-formal-unbounded_hashed_sets.ads:57:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] spark-containers-formal-unbounded_hashed_sets.ads:1370:42: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-formal-unbounded_doubly_linked_lists.adb spark-containers-formal-hashed_maps.ads:70:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-lemmas-fixed_point_arithmetic.adb spark-lemmas-fixed_point_arithmetic.ads:19:08: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-pointers-abstract_maps.ads spark-pointers-abstract_maps.ads:17:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-formal-hashed_sets.adb spark-containers-functional-maps.ads:65:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-functional.ads [Ada] spark-cut_operations.adb spark-cut_operations.ads:23:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-formal-ordered_maps.adb spark-containers-formal-unbounded_hashed_maps.ads:57:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-formal.ads [Ada] spark-containers-formal-unbounded_vectors.adb spark-containers-formal-unbounded_doubly_linked_lists.ads:30:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] spark-containers-formal-unbounded_doubly_linked_lists.ads:1650:45: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-tests.ads [Ada] spark-containers-formal-unbounded_ordered_maps.adb spark-containers-formal-hashed_sets.ads:71:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] spark-containers-formal-hashed_sets.ads:1432:42: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-stable_sorting.adb [Ada] spark-containers-functional-sets.adb spark-containers-formal-unbounded_vectors.ads:30:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] spark-containers-formal-unbounded_vectors.ads:887:45: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-pointers-pointers_with_aliasing_separate_memory.adb spark-containers-formal-ordered_maps.ads:65:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-formal-ordered_sets.adb spark-pointers-pointers_with_aliasing_separate_memory.ads:16:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-functional-vectors.adb spark-containers-functional-sets.ads:40:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-lemmas.ads [Ada] spark-big_intervals.ads spark-containers-formal-unbounded_ordered_maps.ads:50:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-formal-holders.adb [Ada] spark-conversions-long_integer_conversions.ads [Ada] spark-containers-formal-unbounded_ordered_sets.adb spark-containers-functional-vectors.ads:48:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-types.ads [Ada] spark-containers-functional-infinite_sequences.adb [Ada] spark-pointers-pointers_with_aliasing.adb spark-pointers-pointers_with_aliasing.ads:14:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-big_reals.ads spark-containers-functional-infinite_sequences.ads:44:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] spark-containers-parameter_checks.adb spark-containers-formal-ordered_sets.ads:62:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] spark-containers-formal-ordered_sets.ads:1600:42: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] rflx-coap_client-session-fsm_allocator.adb [Ada] rflx-rflx_generic_types.ads [Ada] rflx-rflx_generic_types-generic_operators.ads [Ada] rflx-rflx_types-operations.ads [Ada] rflx-coap-option_sequence.ads spark-containers-formal-unbounded_ordered_sets.ads:47:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] spark-containers-formal-unbounded_ordered_sets.ads:1577:42: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] rflx-coap-coap_message.adb [Ada] rflx-rflx_types.ads [Ada] rflx-coap_client-session-fsm.adb [Ada] rflx-coap.ads [Ada] rflx-coap-option_type.adb [Ada] rflx-rflx_builtin_types-conversions.ads [Ada] rflx-rflx_arithmetic.adb [Ada] rflx-coap_client.ads [Ada] rflx.ads [Ada] rflx-rflx_generic_types-generic_operations.adb [Ada] rflx-rflx_scalar_sequence.adb [Ada] rflx-rflx_message_sequence.adb [Ada] rflx-coap_client-options_and_payload_data.adb [Ada] rflx-coap_client-token_data.adb [Ada] rflx-rflx_builtin_types.ads [Ada] rflx-rflx_types-operators.ads [Ada] coap_spark_config.ads [Ada] rflx-coap_client-session_environment.adb [Ada] coap_spark-content_formats.ads [Ada] coap_spark-options-list_sorting.ads [Ada] coap_spark-options.adb [Ada] coap_spark-channel.adb [Ada] coap_spark-options-text_io.adb [Ada] coap_spark-messages.adb [Ada] coap_spark-options-lists.ads [Ada] coap_spark-random.adb [Ada] coap_spark.ads [Ada] coap_spark-log.adb [Ada] rflx-coap_client-session.adb coap_spark-log.ads:9:03: warning: "Always_Terminates" is not a valid aspect identifier [enabled by default] [Ada] coap_spark-uri.adb [Ada] coap_spark-client_session.adb [Ada] coap_spark-utils.adb Build Libraries [gprlib] Coap_Spark.lexch [archive] libCoap_Spark.a [index] libCoap_Spark.a Success: Build finished successfully in 5.46 seconds. Found declared GPR file: coap_spark.gpr [alr test] Test completed SUCCESSFULLY