search

afrl-rq / OpenUxAS

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

daidalus_integration branch ada proofs not passing #39

Closed lhumphrey closed 2 years ago

lhumphrey commented 2 years ago

I merged in changes to the daidalus_integration branch from Sean's fork. However, the CI is failing on "Prove OpenUxAS Ada." This has no effect on the primary content of the daidalus_integration branch, since it doesn't use the Ada services, but it's not clear yet why these proofs are not passing.

lhumphrey commented 2 years ago

Updated proof session files and test.out files for Route Aggregator and Assignment Tree Branch and Bound services, since these were causing the issue. Recent changes to SPARK CE result in some new proof obligations being met, a few others not. Compare test.out files across pull requests to see the differences.