Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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

  • Subject: [Frama-c-discuss] Frama-C usage considered by the European Space Agency; help needed
  • From: Maurizio.Martignano at spazioit.com (Maurizio Martignano)
  • Date: Mon, 29 Oct 2018 15:47:39 +0100
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>