Frama-C-discuss mailing list archives

Maurizio.Martignano at spazioit.com (Maurizio Martignano) · Mon, 29 Oct 2018 20:27:53 +0100

Dear Mr. Maroneze,

               Thank you so much for you fast reply and feedback.

Indeed your answer closes all the open points and doubts I had about the
attempt/test we were trying to perform.

Once again, thank you very much,

Maurizio Martignano

From: Frama-c-discuss <frama-c-discuss-bounces at lists.gforge.inria.fr> On
Behalf Of Andre Maroneze
Sent: 29 October 2018 18:47
To: frama-c-discuss at lists.gforge.inria.fr
Subject: Re: [Frama-c-discuss] Frama-C usage considered by the European
Space Agency; help needed

Dear Mr. Martignano,

Configuring Frama-C for a complex build is something we are continuously
working on, but which still requires some amount of manual work.

In your case, the fact that a cross-compiler is needed simply to be able to
parse the sources (e.g. due to the presence of inline assembly), makes
things more difficult.

We currently recommend the following procedure for complex builds:

- Install bear (Build EAR, https://github.com/rizsotto/Bear);

- Run "bear make" instead of "make", this should proceed as normal, but also
create a "compile_commands.json" file;

- (make sure Frama-C was installed with optional dependency yojson) Run
`frama-c -json-compilation-database compile_commands.json <list of source
files>` ; this should automatically set the required -D/-I flags, which
might help with parsing.

There will still be a number of issues to take into account:

- The target platform, ARM, currently has no machdep (machine-dependent
parameters) definition in Frama-C; the plug-in developer manual
(http://frama-c.com/download/frama-c-plugin-development-guide.pdf) contains
a section mentioning some details about the creation of a custom machdep; as
a first approximation, using the existing x86 32-bit machdep should help
bootstrap parsing, even if a correct analysis will require writing a custom
machdep;

- The code has GCC-specific syntax, such as empty initializers (struct s a =
{}), which requires the use of a GCC-compatible machdep, for instance
"-machdep gcc_x86_32" might help with parsing;

- Some files use unsupported GCC extensions; for instance, usddeck.c uses
what Clang calls a 'variable length array in structure';

- Some files, such as i2c_drv.c (and its header) use non-portable code, e.g.
i2c_drv.h declares i2cdrvCreateMessage with an argument of type I2cDirection
(an enum), while the definition in i2c_drv.c gives the same argument type
uint8_t;

- Some definitions are currently absent from Frama-C's libc, such as the NAN
macro. Supplying them, or skipping the files requiring them, is necessary
for parsing to succeed.

Overall, the code is not C99-compliant and uses several GCC extensions,
which makes parsing harder. In its current form, it is not an ideal target
for Frama-C, however most of these issues should be easy to fix, especially
if code portability is desirable. A first step towards more portable code is
to add "-pedantic -pedantic-errors" to GCC's command line and try to avoid
them whenever possible.

On a side note, I noticed the code uses FreeRTOS, which is based on
interruptions and tasks. Plug-ins such as Eva cannot currently handle them
natively, so usage of other plugins (e.g. Mthread), or stubs to emulate
calls to these tasks might be necessary.

Concerning your command lines:

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

Note that usage of the Eva plugin (-val) obviates the RTE plugin (-rte):
when using Eva, it will automatically generate alarms for RTEs which it
cannot prove, so you should remove the "-rte" option from the command line
whenever "-val" is present.

Also, if you are using Eva to analyze library code or perform an analysis
that is not whole-program (that it, starting from some place other than the
program's main function), you might want to add the "-lib-entry" option to
Eva, to obtain a more representative initial state, where global variables
may contain any value, other than being zero-initialized. This will not
improve precision, but should give a more representative result of "code
being called from anywhere", as is often the case with library functions.

> Did I need to use Frama-C include and "enrich" the code with ACLS
annotations?

Using the Frama-C standard library is preferred (the method I described
previously is intended to preserve usage of Frama-C's libc), since many
functions already contain ACSL specifications. However, in complex
situations you may need to use an external library. Producing preprocessed
code (e.g. with gcc's -E option) is a possibility; when preprocessed .i
files are given to Frama-C, it will try parsing them as preprocessed, which
may avoid some issues with cross-compilation, but the code will lack
specifications.

Overall, Frama-C differs from syntactic-based static analysis tools, which
only look for syntactic patterns and are thus able to handle partial code
more easily. In particular, the Eva plug-in, which you tried, is based on
whole-program analysis and uses much richer semantic information from the
program, but in exchange requires a more complete set of files and function
definitions to operate automatically. Adding stubs and/or ACSL
specifications for library functions is always an option, but requires some
work.

I hope this clarifies a bit and provides some answers to your questions.
Please note that analyzing a complete application is quite an endeavor; this
kind of analysis is often performed as part of collaborations between the
Frama-C team and other institutions, so we can provide more extensive
technical support and further develop the platform, when necessary to
improve the analysis results.

Best regards,

On 29/10/2018 15:47, Maurizio Martignano wrote:

Dear Frama-C community,  my name is Maurizio Martignano (www.spazioit.com
<http://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

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
<mailto:Frama-c-discuss at lists.gforge.inria.fr> 
https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
AndrÃ© Maroneze
Researcher/Engineer CEA/List
Software Reliability and Security Laboratory
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181029/11d3ee37/attachment-0001.html>

Frama-C-discuss mailing list archives

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