Re: How to configure GNAT GPL on x86-64 Linux for ARM ELF development

[Simon Wright <simon@pushface.org>]

Adam Jensen <hanzer@riseup.net> writes:

> I am trying the "Digital Output" example described here:
> <http://www.inspirel.com/articles/Ada_On_Cortex_Digital_Output.html>
>
> Compilation seems to be successful with these commands: 
> gprbuild -c -u -f utils.adb --target=arm-eabi --RTS=zfp-stm32f4
> gprbuild -c -u -f pins.adb --target=arm-eabi --RTS=zfp-stm32f4
> gprbuild -c -u -f program.adb --target=arm-eabi --RTS=zfp-stm32f4
>
> But linking fails like this:
> arm-eabi-ld -T ../flash.ld -o program.elf program.o pins.o utils.o
> pins.o: In function `pins__enable_output':
> pins.adb:(.text+0x20): undefined reference to `__gnat_last_chance_handler'
> pins.o: In function `pins__write':
> pins.adb:(.text+0x7a): undefined reference to `__gnat_last_chance_handler'

From the tutorial, towards the end,

   You should notice the -gnatp option when compiling the pins.adb
   file. This option instructs the compiler not to generate calls to
   range check functions that verify whether the values that are
   assigned to variables or converted between types fall within expected
   ranges and if not, an appropriate standard exception is raised. We
   have decided not to rely on the Ada run-time library and without this
   option the final program would not link properly (try it, you can
   also check the assembly output for the pins.adb file and see that
   indeed there are some calls to other, language-supporting
   subprograms).

and then

   Instead, we can verify the code and conclude that all values are safe
   and therefore resign from run-time range checks altogether, which in
   the embedded context is a more robust approach anyway. Later on we
   will see how to automate such analysis, which with bigger programs
   could be much less straightforward when done manually. For the time
   being, we will rely on manual verification and the -gnatp option in
   such cases.

I think Maciej is referring to proof techniques, which is laudable, but
I find it necessary to let the exceptions happen if I make a mistake;
I've tended to have a 'heartbeat' LED flash, so that if the last chance
handler (which disables interrupts and loops) happens I can at least see
that something's wrong.

AdaCore's Certyflie[1] implementation for the Crazyflie brings some
SPARK proof to the drone's firmware, but (a) it only applies to the
application layer, not the drivers, (b) it crashes the 2017 CE SPARK
package, (c) without expert assistance, I can't get my head round the
contortions necessary to do SPARK (particularly the real-time aspects).

[1] https://github.com/AdaCore/Certyflie