From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail From: Simon Wright Newsgroups: comp.lang.ada Subject: Re: How to configure GNAT GPL on x86-64 Linux for ARM ELF development Date: Fri, 25 May 2018 08:55:39 +0100 Organization: A noiseless patient Spider Message-ID: References: Mime-Version: 1.0 Content-Type: text/plain Injection-Info: h2725194.stratoserver.net; posting-host="9c58e02725f24ca1d1b99fef641db2a7"; logging-data="4264"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19BZfWw+AURFL96U7O5RWpDm1wkxEkEZPo=" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (darwin) Cancel-Lock: sha1:bDAcaurRTG2/KE1SXSssQfVPHPs= sha1:RySBNbRVqNwurkxPrDWzw9OiZ2I= Xref: reader02.eternal-september.org comp.lang.ada:52666 Date: 2018-05-25T08:55:39+01:00 List-Id: Adam Jensen writes: > I am trying the "Digital Output" example described here: > > > 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