--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on October 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C usage considered by the European Space Agency; help needed



Dear Frama-C community,  my name is Maurizio Martignano (www.spazioit.com).

I perform independent SW validation and verification for ESA missions and am
currently involved with a European Space Agency project that tries to
collect a set of Static Analysis tools and offer them in a pre-packaged
ready-to-use form, for use in "blind" analysis - that is, looking at the
code as-is (with no analyser-specific annotations of any kind).

I am unsure if Frama-C fits this model - and my preliminary results with
open-source codebases seem to confirm that the tool can't be used with
"as-is" codebases. 

Here's what I did... 

I took as test bench the Crazyflie system:
<https://github.com/bitcraze/crazyflie-firmware>
https://github.com/bitcraze/crazyflie-firmware.

It's build toolset is available here:
<https://launchpad.net/gcc-arm-embedded/+download>
https://launchpad.net/gcc-arm-embedded/+download.

>From the Makefile, I constructed the following script (frama-c-abalyze.sh),
which is supposed to be called from within the "src" folder.

    #frama-c -c11 -kernel-msg-key pp -kernel-warn-error=-annot-error
-cpp-extra-args="-DUSE_RADIOLINK_CRTP -DENABLE_UART -DARM_MATH_CM4
-D__FPU_PRESENT=1 -D__TARGET_FPU_VFP -DBOARD_REV_D
-DESTIMATOR_NAME=anyEstimator -DCONTROLLER_NAME=ControllerTypeAny
-DPOWER_DISTRIBUTION_TYPE_stock -Ilib/FreeRTOS/include
-Ilib/FreeRTOS/portable/GCC/ARM_CM4F -Isrc -Iconfig -Ihal/interface
-Imodules/interface -Iutils/interface -Idrivers/interface -Iplatform
-I../vendor/CMSIS/CMSIS/Include -Idrivers/bosch/interface
-Ilib/STM32F4xx_StdPeriph_Driver/inc -Ilib/CMSIS/STM32F4xx/Include
-Ilib/STM32_USB_Device_Library/Core/inc -Ilib/STM32_USB_OTG_Driver/inc
-Ideck/interface -Ideck/drivers/interface -Iutils/interface/clockCorrection
-Iutils/interface/tdoa -Iutils/interface/lighthouse
-I../vendor/libdw1000/inc -Ilib/FatFS -Ilib/vl53l1 -Ilib/vl53l1/core/inc
-DSTM32F4XX -DSTM32F40_41xxx -DHSE_VALUE=8000000 -DUSE_STDPERIPH_DRIVER" $*
    frama-c -c11 -kernel-msg-key pp -kernel-warn-error=-annot-error
-no-cpp-frama-c-compliant -no-frama-c-stdlib -cpp-command="arm-none-eabi-gcc
-E -DUSE_RADIOLINK_CRTP -DENABLE_UART -DARM_MATH_CM4 -D__FPU_PRESENT=1
-D__TARGET_FPU_VFP -DBOARD_REV_D -DESTIMATOR_NAME=anyEstimator
-DCONTROLLER_NAME=ControllerTypeAny -DPOWER_DISTRIBUTION_TYPE_stock
-mcpu=cortex-m4 -mthumb -mfloat-abi=hard -mfpu=fpv4-sp-d16
-Ilib/FreeRTOS/include -Ilib/FreeRTOS/portable/GCC/ARM_CM4F -Isrc -Iconfig
-Ihal/interface -Imodules/interface -Iutils/interface -Idrivers/interface
-Iplatform -I../vendor/CMSIS/CMSIS/Include -Idrivers/bosch/interface
-Ilib/STM32F4xx_StdPeriph_Driver/inc -Ilib/CMSIS/STM32F4xx/Include
-Ilib/STM32_USB_Device_Library/Core/inc -Ilib/STM32_USB_OTG_Driver/inc
-Ideck/interface -Ideck/drivers/interface -Iutils/interface/clockCorrection
-Iutils/interface/tdoa -Iutils/interface/lighthouse
-I../vendor/libdw1000/inc -Ilib/FatFS -Ilib/vl53l1 -Ilib/vl53l1/core/inc
-DSTM32F4XX -DSTM32F40_41xxx -DHSE_VALUE=8000000 -DUSE_STDPERIPH_DRIVER %1 >
%2" $*

The first line calls Frama-C with its own include files and pre-processor.
The second line call Frama-C with the build system include files and
pre-processor.

Using the second line and applying it to all the *.c files in the "src"
folder which also appear in the Makefile I got many Frama-C "compilation
errors", e.g. "syntax error", "invalid user input", "User Error".

On top of that, I tried to call the "val" plugin on a file that did not show
any "compilation" error, e.g."./modules/src/log.c". I used commands like:

    ./frama-c-analyze.sh -rte -val -main logTask modules/src/log.c
    ./frama-c-analyze.sh -rte -val -main logTOCProcess modules/src/log.c
    ./frama-c-analyze.sh -rte -val -main logControlProcess modules/src/log.c

applying this type of command to all the functions in the file.

The output I managed to get had inside lines like the following:

    [value:alarm] modules/src/log.c:771: Warning: 
      assertion 'rte,mem_access' got status unknown.
    [value:alarm] modules/src/log.c:771: Warning: 
      out of bounds read. assert \valid_read(&ops->variable);
    [value:alarm] modules/src/log.c:772: Warning: 

I found this type of output not very informative, and sort of false
positive.

Did I do something wrong? Am I missing something? Did I need to use Frama-C
include and "enrich" the code with ACLS annotations?

Thank you very much in advance, Maurizio

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181029/6e00a1e3/attachment-0001.html>