This refactors a line in the Receive_Signal_Power function to help
GNATprove prove the precondition to Log10.
We also suppress a warning around the DW1000_IRQ's Attach_Interrupt
where a warning is issued about the possibility of a reserved
interrupt. Since there's no way to prove that it's not reserved,
or to somehow restrict the choice, we simply suppress the message
instead and assume that the interrupt is not reserved. A reserved
interrupt should be easy to spot since it will raise a Program_Error
when attaching it, which would be hard to miss.
This refactors a line in the Receive_Signal_Power function to help GNATprove prove the precondition to Log10.
We also suppress a warning around the DW1000_IRQ's Attach_Interrupt where a warning is issued about the possibility of a reserved interrupt. Since there's no way to prove that it's not reserved, or to somehow restrict the choice, we simply suppress the message instead and assume that the interrupt is not reserved. A reserved interrupt should be easy to spot since it will raise a Program_Error when attaching it, which would be hard to miss.