This pull request includes commits that cover several topics.
reorganization of the Ada source code
improvements to the Ada source code
fix for github actions
enhancement of the ATBB proofs
The Ada sources have been reorganized into subdirectories that largely match those of the C++ code in order to make navigation easier.
The Ada sources have also been improved to increase readability. As part of this improvement, we have activated compiler switches that enforce style checks. These checks include enforcing consistent casing for identifier names (Ada is a case-insensitive language). To help make this checks pass and to ensure that the overall style of the Ada code is consistent with language standards, we introduced changes to how LmcpGen generates Ada code that were included in https://github.com/afrl-rq/LmcpGen/pull/31 (which has been merged).
Github Actions changed some settings related to security that broke our builds. This has been fixed.
The proofs for ATBB have been enhanced such that they have nearly reached silver level. Note that because the version of gnatprove included in GNAT Community 2020 crashes on some of these proofs, they have been excluded from the current "test" suite run during continuous integration. We expect to activate these proofs once Community 2021 is released.
Proof Status
In this PR, the following proofs are expected to fail (the failure has been recorded in test.out, which serves as the basis for comparison by the proof script in continuous integration):
This pull request includes commits that cover several topics.
The Ada sources have been reorganized into subdirectories that largely match those of the C++ code in order to make navigation easier.
The Ada sources have also been improved to increase readability. As part of this improvement, we have activated compiler switches that enforce style checks. These checks include enforcing consistent casing for identifier names (Ada is a case-insensitive language). To help make this checks pass and to ensure that the overall style of the Ada code is consistent with language standards, we introduced changes to how LmcpGen generates Ada code that were included in https://github.com/afrl-rq/LmcpGen/pull/31 (which has been merged).
Github Actions changed some settings related to security that broke our builds. This has been fixed.
The proofs for ATBB have been enhanced such that they have nearly reached silver level. Note that because the version of
gnatproveincluded in GNAT Community 2020 crashes on some of these proofs, they have been excluded from the current "test" suite run during continuous integration. We expect to activate these proofs once Community 2021 is released.Proof Status
In this PR, the following proofs are expected to fail (the failure has been recorded in
test.out, which serves as the basis for comparison by the proof script in continuous integration):Automation Request Validator:
Route Aggregator:
The second and last unproved checks in Route Aggregator are legitimate: Euclidean_Plan has not been implemented yet.
No proofs are attempted for ATBB using Community 2020 during continuous integration.