SPARK mode consideration

[kevlar700]

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?

#40

[kevlar700]

I had a look at optionally removing discriminants from arrays but it requires more changes and understanding than I can currently afford the time for when I can just use unchecked_conversions for the few long arrays.

The relevant code for creating arrays is at
descriptors-field.adb line 496 (Union_T)
ada_gen.adb line 2212 (New_Type_Union)

[simonjwright]

On 29 Nov 2023, at 14:27, Kevin Chadwick ***@***.***> wrote: I have seen @simonjwright <https://github.com/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 with an address.

Where was that?

[kevlar700]

Where was that?

I am not sure. My memory is usually very good but I can be mistaken. I guess it was in a particular context then, if at all.

[kevlar700]

Update: I decided to simply create multiple peripherals e.g. TIM1_Output_Peripheral,TIM1_Output_Periph and TIM1_Input_Peripheral,TIM1_Input_Periph and manage the patching manually for now. Even on the new U5 chip that we are using there are only 7 files to manage instead of 2 with L4.