Merge main into feature/upgrade-gnatprove

.github/workflows/appimage.yml

@@ -18,6 +18,10 @@ jobs:
   release:
     name: Continuous
     runs-on: ubuntu-22.04
+    strategy:
+      fail-fast: false
+      matrix:
+        target: [client, server]
     steps:
        - name: Checkout
          uses: actions/checkout@v2
@@ -27,6 +31,7 @@ jobs:
          uses: mgrojo/alr2appimage-action@main
          with:
            alireVersion: 2.1.0
-           crateDir: client
+           crateDir: ${{ matrix.target }}
            alr2appimageArgs: "--terminal --use-version"
+           tagName: "${{ github.ref_name }}-continuous-${{ matrix.target }}"
            deleteExistent: true

.github/workflows/main.yml

@@ -17,13 +17,15 @@ jobs:
       fail-fast: false # Don't stop all the workflows when one of them fails.
 
       matrix:
-        os: [ubuntu-22.04, windows-latest, macos-13] # List of GitHub Actions platform to run the workflow on
+        os: [ubuntu-22.04, windows-latest, macos-14] # List of GitHub Actions platform to run the workflow on
     env:
       # For WolfSSL:
       #  set the value of the environment variable OS to Windows when running on the Windows operating system and to Linux_Or_Mac otherwise
       OS: ${{ matrix.os == 'windows-latest' && 'Windows' || 'Linux_Or_Mac' }}
       # On Windows, the validation profile fails due to "(style) incorrect line terminator [-gnatyd]"
       PROFILE: ${{ matrix.os == 'windows-latest' && 'development' || 'validation' }}
+      # Switches to enable code coverage with gcov
+      COVERAGE_SWITCHES: "-XCOVERAGE=gcov -cargs -O0 -fno-inline --coverage -largs --coverage"
 
     runs-on: ${{ matrix.os }} # Run the continuous integration workflow on each OS listed in the matrix.
 
@@ -39,58 +41,82 @@ jobs:
           version: 2.1.0 # Remove this option to use the default (latest stable release)
 
         # Build the project using the validation build profile to enforce static analysis and coding style.
-      - run: alr --non-interactive build --$PROFILE -- -cargs -fprofile-arcs -ftest-coverage -largs -lgcov --coverage -fprofile-arcs
+      - name: Build library
+        run: alr --non-interactive build --$PROFILE -- $COVERAGE_SWITCHES
         shell: bash
 
-      # Build the client using the validation build profile to enforce static analysis and coding style.
-      - run: cd client && alr --non-interactive build --profiles="*=$PROFILE" -- -cargs -fprofile-arcs -ftest-coverage -largs -lgcov --coverage -fprofile-arcs
+        # Build the test programs using the validation build profile to enforce static analysis and coding style.
+      - name: Build test client
+        run: alr -C client --non-interactive build --profiles="*=$PROFILE" -- $COVERAGE_SWITCHES
+        shell: bash
+
+      - name: Build test server
+        run: alr -C server --non-interactive build --profiles="*=$PROFILE" -- $COVERAGE_SWITCHES
         shell: bash
 
         # Install binary crates needed for testing
-      - run: alr --non-interactive install bbt~0.2.0
+      - name: Install binary crates
+        run: alr --non-interactive install bbt~0.2.0
         shell: bash
 
         # Run the instrumented testsuite. This will produce *.gcno and *.gcda files for the coverage analysis.
-
       - name: Library Aunit tests
         run: |
             cd tests
-            alr --non-interactive build --profiles="*=$PROFILE" -- -cargs -fprofile-arcs -ftest-coverage -largs -lgcov --coverage -fprofile-arcs
+            alr --non-interactive build --profiles="*=$PROFILE" -- $COVERAGE_SWITCHES
             echo "## Aunit test results" >> $GITHUB_STEP_SUMMARY
             NO_COLOR=1 bin/tests >> $GITHUB_STEP_SUMMARY
         shell: bash
 
         # On Linux we can run all the testsuite, after installing coap-server-openssl from libcoap3-bin package.
       - if: runner.os == 'Linux'
+        name: Client tests (CoAP and secure CoAP)
         run: |
             sudo apt install libcoap3-bin 
             PATH=$HOME/.alire/bin:$PATH make -C client/tests
         shell: bash
 
         # On Windows and macOS we can only run the plain CoAP tests.
       - if: runner.os == 'Windows' || runner.os == 'macOS'
+        name: Client tests (CoAP only)
         run: PATH=$HOME/.alire/bin:$PATH make -C client/tests coap_results.md
         shell: bash
 
-      - name: CoAP test results
-        run: cat client/tests/coap_results.md >> $GITHUB_STEP_SUMMARY
+        # Run server tests
+      - if: runner.os == 'Windows' || runner.os == 'Linux'
+        name: Server tests
+        run: |
+            PATH=$HOME/.alire/bin:$PATH make -C server/tests
         shell: bash
 
-      - if: runner.os == 'Linux'
-        name: Secure CoAP (coaps) test results
-        run: cat client/tests/coaps_results.md >> $GITHUB_STEP_SUMMARY
+      - if: runner.os == 'macOS'
+        name: Server tests (CoAP only on macOS)
+        run: |
+            PATH=$HOME/.alire/bin:$PATH make -C server/tests coap_results.md
+        shell: bash
+
+      - name: CoAP test results
+        run: cat client/tests/coap*_results.md server/tests/coap*_results.md >> $GITHUB_STEP_SUMMARY
         shell: bash
 
-        # Run gcov on the library, the tests and the client. This will produce *.gcov files.
-      - run: |
-          alr exec -- gcov -o obj/$PROFILE src/*.ad[sb]
-          cd tests  && alr exec -- gcov -o obj/$PROFILE src/*.ad[sb]
-          cd -
-          cd client && alr exec -- gcov -o obj/$PROFILE src/*.ad[sb]
+        # Run gcov on the library, the tests and the test programs. This will produce *.gcov files.
+        # The library source files are splitted in parts, otherwise gcov fails with
+        # an unexpected error.
+      - name: Run gcov
+        run: |
+          alr exec -- gcov -o obj/$PROFILE src/rflx*.ad[sb]
+          alr exec -- gcov -o obj/$PROFILE src/coap_spark*.ad[sb] src/workarounds.ad[sb]
+          for dir in tests client server
+          do
+            cd $dir
+            alr exec -- gcov -o obj/$PROFILE src/*.ad[sb]
+            cd -
+          done
         shell: bash
 
         # Upload results to codecov.io
-      - uses: codecov/codecov-action@v5
+      - if: runner.os == 'Linux'
+        uses: codecov/codecov-action@v5
         with:
           fail_ci_if_error: true # optional (default = false)
           name: codecov-umbrella # optional

.github/workflows/prove.yml

@@ -1,25 +1,31 @@
 name: GNATprove
 
-on:                    # Run the workflow for each of the following events:
-  push:                # - A branch is pushed or updated.
-    paths:             # When the sources or dependencies change.
+on:
+  push:
+    paths:
       - '.github/workflows/prove.yml'
       - 'src/**'
       - 'client/src/**'
+      - 'server/src/**'
       - 'alire.toml'
       - 'client/alire.toml'
+      - 'server/alire.toml'
       - 'coap_spark.gpr'
       - 'client/coap_client.gpr'
+      - 'server/coap_server.gpr'
       - 'libs/wolfssl'
   pull_request:        # - A pull-request is opened or updated.
     paths:
       - '.github/workflows/prove.yml'
       - 'src/**'
       - 'client/src/**'
+      - 'server/src/**'
       - 'alire.toml'
       - 'client/alire.toml'
+      - 'server/alire.toml'
       - 'coap_spark.gpr'
       - 'client/coap_client.gpr'
+      - 'server/coap_server.gpr'
       - 'libs/wolfssl'
   workflow_dispatch:   # - A manual run of the workflow is requested from the GitHub web interface.
   release:
@@ -28,6 +34,10 @@ on:                    # Run the workflow for each of the following events:
 jobs:
   gnatprove:
     runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        target: [client, server]
 
     steps:
     - name: Checkout repository
@@ -43,7 +53,8 @@ jobs:
 
     - name: Install GNAT package
       run: |
-        chmod +x install_package.sh && ./install_package.sh ./gnat-2021-20210519-x86_64-linux-bin $HOME/gnat-2021 com.adacore.spark2014_discovery
+        chmod +x install_package.sh
+        ./install_package.sh ./gnat-2021-20210519-x86_64-linux-bin $HOME/gnat-2021 com.adacore.spark2014_discovery
 
     # Install and setup Alire package manager
     - uses: alire-project/setup-alire@v2
@@ -53,16 +64,18 @@ jobs:
     - name: Set up environment for Colibri
       run: echo "$HOME/gnat-2021/libexec/spark/bin" >> $GITHUB_PATH
 
-    # Run GNATprove in the client to perform automatic formal verification of the SPARK code.
-    - name: Run GNATprove
+    - name: Run GNATprove (${{ matrix.target }})
+      working-directory: ${{ matrix.target }}
       run: |
-        cd client
+        set -e
         alr build --stop-after=generation
         alr gnatprove -j0 --level=4
-        # Get a summary for the action from the first (most relevant) lines of gnatprove.out
-        echo '```' >> $GITHUB_STEP_SUMMARY 
-        head -23 obj/development/gnatprove/gnatprove.out >> $GITHUB_STEP_SUMMARY 
-        echo '```' >> $GITHUB_STEP_SUMMARY
+        {
+          echo '```'
+          echo "# GNATprove summary for ${matrix_target:-${{ matrix.target }}}"
+          head -23 obj/development/gnatprove/gnatprove.out || echo "No summary available"
+          echo '```'
+        } >> $GITHUB_STEP_SUMMARY
 
 
 

README.md

@@ -2,6 +2,7 @@
 [![AppImage](https://github.com/mgrojo/coap_spark/actions/workflows/appimage.yml/badge.svg)](https://github.com/mgrojo/coap_spark/actions/workflows/appimage.yml)
 [![GNATprove](https://github.com/mgrojo/coap_spark/actions/workflows/prove.yml/badge.svg)](https://github.com/mgrojo/coap_spark/actions/workflows/prove.yml)
 [![codecov](https://codecov.io/gh/mgrojo/coap_spark/graph/badge.svg?token=2AEXL06XHU)](https://codecov.io/gh/mgrojo/coap_spark)
+[![Alire](https://img.shields.io/endpoint?url=https://alire.ada.dev/badges/coap_spark.json)](https://alire.ada.dev/crates/coap_spark.html)
 
 # CoAP-SPARK
 CoAP-SPARK is a library implementing the Constrained Application Protocol (CoAP)
@@ -14,15 +15,15 @@ implementation, mainly for academic purposes.
 
 ## Dependencies
 CoAP-SPARK uses:
-* Alire as source package manager (independently installed)
-* RecordFlux as a tool facilitating the implementation of the verifiable
+* [Alire](https://alire.ada.dev) as source package manager (independently installed)
+* [RecordFlux](https://github.com/AdaCore/RecordFlux) as a tool facilitating the implementation of the verifiable
   protocol parser and the state machine of a session (included as Git submodule)
-* WolfSSL as library for implementing the DTLS communications
+* [WolfSSL](https://github.com/wolfSSL/wolfssl) as library for implementing the DTLS communications
   (included as Git submodule)
-* GNAT 14.2.1 (toolchain managed by Alire)
-* GNATProve 14.1.1 (dependency managed by Alire)
-* Aunit for unit-testing the library (dependency managed by Alire)
-* bbt for testing (installable via Alire)
+* [GNAT](https://github.com/alire-project/GNAT-FSF-builds) 14.2.1 (toolchain managed by Alire)
+* [GNATProve](https://github.com/alire-project/GNAT-FSF-builds) 14.1.1 (dependency managed by Alire)
+* [Aunit](https://github.com/AdaCore/aunit) for unit-testing the library (dependency managed by Alire)
+* [bbt](https://github.com/LionelDraghi/bbt) for testing (installable via Alire)
 
 ## How to set-up
 
@@ -50,8 +51,8 @@ alr build
 
 For building the client and server programs:
 ```
-cd client ; alr build
-cd ../server ; alr build
+alr -C client build
+alr -C server build
 ```
 
 ## How to test
@@ -62,22 +63,28 @@ alr install bbt
 
 And then run the tests with:
 ```
-cd client/tests ; make
+make -C client/tests
+make -C server/tests
 ```
 
-See [`client/tests/coap_client_tests.md`](client/tests/coap_client_tests.md)
-for the specification of these tests.
+Thanks to `bbt`, the test specification can also work as documentation of the
+features available in the server and the client. You can see:
+
+* Client tests for [plain CoAP](client/tests/coap_client_tests.md) and 
+ [CoAP over DTLS](client/tests/coaps_client_tests.md)
+* Server tests for [plain CoAP](server/tests/coap_server_tests.md) and
+ [CoAP over DTLS](server/tests/coaps_server_tests.md)
 
 There are also some unit tests for the library. To run them, enter the `tests/`
-directory and run:
+directory and run them using Alire:
 ```
 cd tests; alr run
 ```
 
 ## How to prove
-The project (library and client) is currently proved up to the silver mode.
+The project (library, client and server) is currently proved up to the silver mode.
 
-The [`proof/`](proof/) directory constains the results of passing GNATProve. You can replay it running:
+The [`proof/`](proof/) directory contains the results of passing GNATProve. You can replay it running:
 ```
 alr gnatprove --replay
 ```
@@ -102,16 +109,17 @@ in the `PATH`, so `gnatprove` can find the `colibri` executable.
 CoAP-SPARK is a working and verified implementation of CoAP.
 
 The main objective of CoAP-SPARK is to be the subject of my Master's Thesis, but
-I think it can be used in scenarios where this limitations are not an issue:
+I think it can be used in scenarios where these limitations are not an issue:
 - There are no retransmissions.
-- Block-wise transfers are not implemented. This isn't part of main RFC 7252
-  for CoAP, but of the [RFC 7959](https://datatracker.ietf.org/doc/rfc7959/).
 - It only supports NoSec and PreSharedKey security modes.
+- Block-wise transfers are not implemented. Nevertheless, this isn't part of the
+  main RFC 7252 for CoAP, but of [RFC 7959](https://datatracker.ietf.org/doc/rfc7959/).
 
-Regarding the implemented client is able to
-substitute libcoap's coap-client when called from a project like
+Regarding the implemented client, it is able to
+substitute libcoap's coap-client, for example, when called from a project like
 [ikea-smartlight](https://github.com/slokhorst/ikea-smartlight/).
 
-The server implementation is ongoing, following the example of the client.
+The server implementation is an example of a CoAP server that can answer to CRUD
+requests, storing resources in memory.
 
 Bug reports, feedback or suggestions on how to improve the library are very welcome.

TODO.org

@@ -5,6 +5,8 @@
 - [X] Enable coverage reports after testing on GitHub action.
 - [ ] Convert Max_Number_Of_Options into a compile time option.
 - [ ] Increase coverage adding tests or removing dead code.
+- [ ] Fix Is_Valid_As_Number for numbers with correct width but out of the type range    
+      There is still a problem when the width is correct but it is still out of the range.
 
 * Client
 - [ ] Implement timeout with -B option in client
@@ -25,15 +27,17 @@
 
 * Server
 - [X] Consider implementing server state-machine and example
-  - [ ] Implement secure communications for the server
-  - [ ] Implement server logic for CRUD
-  - [ ] Add tests for the server
-  - [ ] Make the validation profile work for the server
-        either with the Workarounds package or making SPARKLib 15 to work.
-  - [ ] Add server in workflows
+  - [X] Implement secure communications for the server
+      - [X] Make it interoperable with coap-client-openssl or coap-client-gnutls
+      - [ ] Fix CoAPS test on macOS
+  - [X] Implement server logic for CRUD
+  - [X] Add tests for the server
+  - [X] Make the validation profile work for the server
+        either with the Workarounds package (chosen option) or making SPARKLib 15 to work.
+  - [X] Add server in workflows
 
 * Upgrades
-  - [x] (discarded) Upgrade to GNATProve 15 and GNAT 15
+  - [x] (discarded: colibri not working) Upgrade to GNATProve 15 and GNAT 15
   - [X] Upgrade bbt
 
 * Provers

alire.toml

@@ -13,7 +13,7 @@ This version implements client and server sides of the protocol with some limita
 
 See LICENSING for licensing information.
 """
-version = "0.10.0-dev"
+version = "0.10.0"
 
 authors = ["Manuel Gomez"]
 maintainers = ["Manuel Gomez <mgrojo@gmail.com>"]

client/coap_client.gpr

@@ -9,7 +9,6 @@ project CoAP_Client is
    for Object_Dir use "obj/" & CoAP_Client_Config.Build_Profile;
    for Create_Missing_Dirs use "True";
    for Exec_Dir use "bin";
-   for Main use ("coap_client.adb");
 
    package Compiler is
       for Default_Switches ("Ada") use CoAP_Client_Config.Ada_Compiler_Switches;