gnatprove -P cf_ada_spark.gpr --ERROR

[pierreciv]

Hello, We have this error, using spark on the ada-code of the Crazyflie:

:~/Documents/GT/Certyflie$ gnatprove -P cf_ada_spark.gpr --RTS=/usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4 --mode=prove modules/pid.ads

warning: attribute "Target" of your project file is currently ignored by gnatprove warning: to specify target properties, specify option "-gnateT" using "Builder.Global_Compilation_Switches" Phase 1 of 2: generation of Global contracts ... Phase 2 of 2: flow analysis and proof ... safety.ads:16:16: medium: float overflow check might fail safety.ads:18:16: medium: float overflow check might fail safety.ads:56:21: medium: range check might fail +===========================GNAT BUG DETECTED==============================+ | GPL 2017 (20170515) (spark) Program_Error why-gen-expr.adb:338 explicit raise| | Error detected at imu.adb:119:32 | | Please submit a bug report by email to report@adacore.com. | | GAP members can alternatively use GNAT Tracker: | | http://www.adacore.com/ section 'send a report'. | | See gnatinfo.txt for full info on procedure for submitting bugs. | | Use a subject line meaningful to you and us to track the bug. | | Include the entire contents of this bug box in the report. | | Include the exact command that you entered. | | Also include sources listed below. | | Use plain ASCII or MIME attachment(s). | +==========================================================================+

Please include these source files with error report Note that list may not be accurate in some cases, so please double check that the problem can still be reproduced with the set of files listed. Consider also -gnatd.n switch (see debug.adb).

/usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/system.ads /home/pierrecivit/Documents/GT/Certyflie/hal/imu.adb /home/pierrecivit/Documents/GT/Certyflie/hal/imu.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/ada.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/a-numeri.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/a-reatim.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-osinte.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-multip.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-bb.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-bbpara.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/interfac.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/i-stm32.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/i-stm32-rcc.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-stm32.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-bbbopa.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-bbmcpa.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/i-stm32-pwr.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-stoele.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-bbthre.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-bbcppr.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-bbtime.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-bbinte.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-bbbosu.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-bbthqu.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-bcprmu.ads /home/pierrecivit/Documents/GT/Certyflie/utils/filter.ads /home/pierrecivit/Documents/GT/Certyflie/types/types.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/components/src/motion/mpu9250/mpu9250.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/hal/src/hal.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/hal/src/hal-i2c.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/hal/src/hal-time.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/a-nuelfu.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-gcmain.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-libsin.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-libpre.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/stm32.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/boards/crazyflie/src/stm32-board.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/devices/stm32f40x/stm32-device.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/svd/stm32f40x/stm32_svd.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/dma/stm32-dma.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/svd/stm32f40x/stm32_svd-dma.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/stm32-gpio.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/svd/stm32f40x/stm32_svd-gpio.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/stm32-exti.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/hal/src/hal-gpio.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/stm32-adc.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/svd/stm32f40x/stm32_svd-adc.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/uart_stm32f4/stm32-usarts.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/hal/src/hal-uart.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/svd/stm32f40x/stm32_svd-usart.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/stm32-spi.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/svd/stm32f40x/stm32_svd-spi.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/hal/src/hal-spi.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/stm32-i2s.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/hal/src/hal-audio.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/stm32-timers.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/stm32-dac.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/svd/stm32f40x/stm32_svd-dac.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/i2c_stm32f4/stm32-i2c.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/svd/stm32f40x/stm32_svd-i2c.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/stm32-rtc.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/hal/src/hal-real_time_clock.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/drivers/crc_stm32f4/stm32-crc.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/arch/ARM/STM32/svd/stm32f40x/stm32_svd-crc.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/components/src/motion/ak8963/ak8963.ads /home/pierrecivit/Documents/GT/Certyflie/Ada_Drivers_Library/middleware/src/ravenscar-common/ravenscar_time.ads /home/pierrecivit/Documents/GT/Certyflie/config/config.ads /home/pierrecivit/Documents/GT/Certyflie/modules/console.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/a-sytaco.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-taskin.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/a-except.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-parame.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-stalib.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/a-unccon.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-traent.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-tasinf.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-taspri.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/a-taside.ads /home/pierrecivit/Documents/GT/Certyflie/modules/crtp.ads /home/pierrecivit/Documents/GT/Certyflie/lib/generic_queue.ads /usr/gnat/arm-eabi/lib/gnat/ravenscar-full-stm32f4/gnat/s-unstyp.ads

imu.ads:95:45: warning: no Global contract available for "Milliseconds" imu.ads:95:45: warning: assuming "Milliseconds" has no effect on global items imu.ads:99:57: warning: no Global contract available for "Milliseconds" imu.ads:99:57: warning: assuming "Milliseconds" has no effect on global items imu.ads:121:58: warning: no Global contract available for "Milliseconds" imu.ads:121:58: warning: assuming "Milliseconds" has no effect on global items compilation abandoned gnatprove: error during flow analysis and proof

about my version of gnatprove : :~/Documents/GT/Certyflie$ gnatprove --version 2017 (20170515)

Have you any suggestion ? Thank you for your time.

[yannickmoy]

Can you tell us which branch of Certyflie you are using? And to be sure, what code do you find on line 119 of imu.adb? thanks

[pierreciv]

~/Documents/GT/Certyflie$ git status Sur la branche ravenscar-cf-stable Votre branche est à jour avec 'origin/ravenscar-cf-stable'. Fichiers non suivis: (utilisez "git add ..." pour inclure dans ce qui sera validé)

gnatinspect.db

aucune modification ajoutée à la validation mais des fichiers non suivis sont présents (utilisez "git add" pour les suivre)

[yoogx]

@yannickmoy just to clarify, the checkout has been done a few minutes before the bug report, so we are up-to-date with the current ravenscar-cf-stable

[pierreciv]

line 119 of imu.adb

IMU_Acc_Lp_Att_Factor := IMU_ACC_IIR_LPF_ATT_FACTOR;

[yannickmoy]

OK I can reproduce...

[yoogx]

And I confirm the bug is also present in Pro 17.2

[yannickmoy]

I cannot reproduce with the dev version of SPARK. A possible workaround is to use the switch --no-global-generation, which prevents completely the generation of Global (and similar flow) contracts on subrpograms. Let us know if this workaround is good for you.

[ptroja]

A less radical workaround is to annotate Get_Time and Get_Date in Ada_Drivers_Library/arch/ARM/STM32/drivers/stm32-rtc.ads with Global => null.

I didn't investigate in depth, but the correct contracts seem to be Global => STM32_SVD.RTC.RTC_Periph (I think), and that's what the tool synthesized (again, I think). But somehow these contracts cause trouble for the VC generation, while the explicit Global => null and its implicit equivalent that comes from the --no-global-generation switch allow the VC generation to proceed.

[yannickmoy]

Closing the issue as we cannot reproduce on dev version, and two workarounds were given.