Merge main into feature/upgrade-gnatprove #19
Closed
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- Not passing formal verification yet.
The use of `SPARK.Containers.Formal.Unbounded_Hashed_Maps` is not compatible with `pragma Restrictions (No_Streams)`, consequently, it has been removed from the code generated by RecordFlux. See AdaCore/RecordFlux#1310
…ct orientation This is to avoid accessing global data from an access to subprogram, which is forbidden by SPARK. The message was: ``` coap_server.adb:67:29: error: access to subprogram with global effects is not allowed in SPARK ```
…ailing verification conditions For `Resources`, the key type is changed to String and the map to ordered map to avoid other failing VCs.
* Get back the URI_Part as key for resources.
…s not Failure nor Success.
… which is not Failure nor Success." This reverts commit cdc60fe. This breaks other checks for communication errors.
…ssion anyway This will keep the socket in a valid state (`Is_Valid = True`).
This reverts part of 68615c7 since, in fact, it got back some VC failures.
And misc changes.
* Implement delete method * Improve command line parsing * Adjust some error responses
Consequently, moved to the library sources. Related to ticket CS0040544 #4830 (GAP).
* Name all the steps * Use bash for server tests
Remove also need of `pkill`.
It was valid to open this port on Windows and macOS. Change to a test about the validity of the port number itself. Detected a problem with the precondition for the non-SPARK function used for converting from string to number. The 'Width is always one more than the actual width for positive numbers (character for the minus sign).
- Update build commands in GitHub Actions to utilize gcov for coverage. - Modify project files to include coverage compiler and linker options. - Implement coverage dumping in server handling for testing. - Add coverage packages for gcov and none scenarios. - Adjust Makefile to streamline secure arguments for tests.
* Build always with the same set of switches, to avoid recompilations that break the coverage files. * `--coverage` is enough, it implies the other switches that were used. * Use the external COVERAGE variable only for the server, where it is required by the two implementations of the `Coverage` package.
* Remove redundancy in `coap_client.gpr`
…rent source directories instead of different names
…inux, which is the most complete testsuite
… unreachable code.
This reverts commit 6e9531c. It is having problems to run in the GitHub action.
This reverts commit a24b80b. No longer needed after previous reversion.
…long payload is no problem there.
Although it passes verification in the GitHub action, `rflx-coap_server-main_loop-fsm.adb` is the only file that locally is not proving.
All verification conditions are proved
CoAP server support in the library and example program
The behaviour of coap-server has changed from Ubuntu 22 to Ubuntu 24 and putting to a resource already existent no longer raises method not allowed. The root path does, so it is used in the test.
This solves an interoperability problem between our server and the libcoap's clients in DTLS mode.
Updated UML model with server entities (work in progress).
Alire badge, links to dependencies and clarifications.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## feature/upgrade-gnatprove #19 +/- ##
==============================================================
+ Coverage 76.90% 89.89% +12.98%
==============================================================
Files 46 52 +6
Lines 1559 1940 +381
==============================================================
+ Hits 1199 1744 +545
+ Misses 360 196 -164 ☔ View full report in Codecov by Sentry. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.