SPARK mode consideration

After discovering that Spark supports overlays. I was just investigating whether it would be possible for svd2ada generated files to pass SPARK mode compliance checks.

With arrays off. Most discriminant records dissappear. For STM32 a couple remain such as for timers and USB_OTG.

Most of these are easily solved by removing the by value option for arrays if a --no-discriminant flag is passed. It would seem that --no-arrays would create a lot of client code duplication. I have seen @simonjwright use --no-arrays. I am not sure how he avoids e.g. 30 item case statements for EXTI/Interrupts etc.. Unless he overlays a 32 bit value or boolean array with an address or unchecked_conversion in the client code?

However, I am unsure of how to solve e.g. the Timer discriminant issue for svd functionality. Whereby depending upon the mode that the timer is in (Input/Output) then the bits of the CCMR1 register differ. The C code just has multiple defines with little/no protection. Is that the only way to make it SPARK compatible or does any one have any ideas?

I wonder if @Fabien-Chouteau unchecked_conversion work could play into solving this?

https://github.com/AdaCore/svd2ada/issues/40

Start by reviewing issue #40 and the svd2ada handling related to --no-discriminant, --no-arrays, and alternateRegister; compare generated STM32 timer and USB_OTG records against SPARK compliance checks. Done would require an agreed implementation path for the remaining discriminant cases and a defined compliance test.