search

afrl-rq / OpenUxAS

Project for multi-UAV cooperative decision making
Other
50 stars 24 forks source link

Adapt Ada code and take advantage of new SPARK features #74

Closed joffreyhuguet closed 7 months ago

joffreyhuguet commented 1 year ago

This patch makes the Ada code compatible with the changes done in GNAT and SPARK. It takes advantage of new features such as logical equality, both in containers and more generally in SPARK code, to remove lots of wrappers that were used to reduce context for provers to prove invariants on the service state.

joffreyhuguet commented 1 year ago

This is only a draft PR because the new features are not publicly available (in Community Edition or on alire).

manthonyaiello commented 9 months ago

At time of writing, this PR resolves #72 and successfully builds the OpenUxAS Ada sources. Given the conflict, we'll have to do some rebasing / cleanup before this is ready to be merged.

But there's a bigger issue: the version of SPARK delivered in GNATprove FSF 13.2.0 is inappropriate for the state of the SPARK sources reflected in this PR - so we still don't have complete proofs. We expect that in moving to a newer of SPARK, these proof failures will be resolved automatically.

Leaving this PR as a draft until cleanup is complete (at least) and probably until we have a sufficient version of SPARK to resolve the proof failures.

manthonyaiello commented 7 months ago

@VVCAS-Sean This is now in a state that's fit to be reviewed and merged. The failure on Ubuntu 20.04 is attributable to this issue, reported at Alire: https://github.com/alire-project/alire/issues/1526 - this will go away once we move away from Alire nightlies or if Alire changes the way it builds nightlies.