cubesatlab / cubedos

A flight software framework in SPARK/Ada
48 stars 5 forks source link

Add SPARK Bounded Queue implementation #36

Closed Eric-Edlund closed 1 year ago

Eric-Edlund commented 1 year ago

It's not fully proven, but has been tested. A simple fixed size queue with a circular buffer.

The queue uses pointers. It was necessary to build it using pointers instead of just a generic data type because of SPARK's pointer rules.