Frama-C-discuss mailing list archives

Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze) · Mon, 29 Oct 2018 18:47:07 +0100

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).
>
> 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.
>
> It's build toolset is available here: 
> 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
> 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/7f64ad06/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3797 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181029/7f64ad06/attachment-0001.bin>

Frama-C-discuss mailing list archives

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