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] Support LLVM database "compile_commands.json"

Thanks for the files!

I have some good news and some bad news: the good news is, I was able to 
parse it. The bad news (for me at least), is that EVA could not go very 
far, due to a recursive call not far from the beginning of the program. 
This can be amended, but I don't hold much hope for a full static 
analysis on this kind of code, given the amount of dependencies, 
libraries which would have to be stubbed, etc. Still, it is good to know 
that we are at least able to parse it.

First of all, let me take advantage of this moment to praise the new 
environment verifications added in Phosphorus, namely one that checks 
that the extended integer types defined in the C standard are consistent 
with those of the machdep currently used by Frama-C. These tests emit 
warnings such as:

/usr/include/stdint.h:40:[kernel] warning: bad type 'long' (32 bits) for 
typedef 'int64_t';
                   check for mismatch between -machdep flag and headers used

This was not present in the previous release, and I indeed had a type 
error similar (though not exactly the same) to the one you described 
when running Frama-C 14 - Silicon.

The issue is that, by default, Frama-C assumes that the code is being 
compiled for x86-32, but the preprocessed files were produced by a 
64-bit compiler. This generated mismatches between Frama-C's types and 
those in the files, which eventually led to inconsistent types later. 
The new release detects this inconsistency and warns about them, so 
simply adding "-machdep x86_64" to the command-line allowed me to parse 
everything. This does not solve everything, however: if you do so, there 
are still several dozens of messages of this type:

/usr/include/x86_64-linux-gnu/bits/byteswap.h:47:[kernel] warning: 
Calling undeclared function __builtin_bswap32. Old style K&R code?
/usr/include/x86_64-linux-gnu/bits/byteswap.h:111:[kernel] warning: 
Calling undeclared function __builtin_bswap64. Old style K&R code?

This is an unfortunate consequence of the fact that files preprocessed 
by GCC often include its builtins. However, Frama-C has a GCC-specific 
machdep, thus using "-machdep gcc_x86_64" (instead of "-machdep x86_64") 
allows such warnings to disappear.

Note that there are still a few built-ins that are not supported by 
Frama-C, such as _Static_assert, __builtin_isnan, __builtin_isinf_sign, 
etc. Ideally, they should have a prototype and a minimal specification 
(e.g. if you want to run EVA, they need ACSL assigns clauses). However, 
it is possible that these functions are present in the code but not 
actually used during the analysis, so you may want to do it later, only 
for the functions actually called during execution.

Also, you'll encounter several warnings related to variadic functions, 
such as:

src/nvim/fileio.c:3852:[variadic] warning: Call to function function 
sprintf with non-static format argument: no specification will be generated.

This is due to the fact that most calls use gettext, and therefore the 
strings are not static, so the Variadic plug-in (which automatically 
generates specifications for variadic functions) will not be able to do 
much. You may want to use option -variadic-no-translation to disable it 
and avoid the warnings, but note that some analyses might then become 
unsound. E.g., if you then run EVA on a program containing calls to 
sprintf, you may get a warning such as:

[kernel] warning: Neither code nor specification for function sprintf, 
generating default assigns from the prototype

This means that Frama-C did not find a specification for the function 
and created its own (since it is needed by EVA), but this generation is 
not guaranteed to be sound.


Finally, I strongly recommend using the Frama-C save feature to store 
the result of parsing, for later reuse (either on the GUI, or by other 
analyses). There is a large amount of files to be parsed, and due to 
preprocessing, there are several (redundant) lines that further increase 
parsing time. To do it once and for all, you just need to do this:

frama-c <kernel/parsing options, such as -machdep, etc.> <list of source 
files> -save parsed.sav

frama-c -load parsed.sav <other analysis options, such as -val, 
-metrics, ...>

or, to see the parsed result in the GUI:

frama-c-gui -load parsed.sav


Overall, though, if you intend to try a thorough analysis with EVA, 
first you'd have to remove/stub recursive calls, then stub calls to 
external library functions (e.g. from libuv ; such stubbing might be 
done via ACSL specifications), then consider issues related to 
concurrency/interrupts/signals, possibly consider how to model the 
environment (e.g. filesystem, network, user interaction, etc.)...

If you just want to see how EVA works on an almost-ideal case (embedded 
software), I'd recommend case study debie1-e-free from the 
open-source-case-studies repository. You can easily modify the provided 
Makefile and obtain different analysis results, and try to add some ACSL 
specifications here and there and see how they impact the analysis. It's 
a small code base, but in my opinion a much better environment to "get a 
feeling about formal methods", without having to deal with several 
concurrent issues all at once.

If you want a tutorial oriented towards functional specifications, based 
on deductive verification, I'd recommend ACSL by Example. Finally, there 
is a tutorial on the WP plug-in (deductive verification) on 
https://github.com/AllanBlanchard/tutoriel_wp/ (the original version is 
in French only, but it is being translated into English).


On 02/06/17 18:21, Matt wrote:
> first of all thanks for your help. I did try to look into it but
> couldn't come up with a solution yet.
> I wanted to try the brand new frama-c but it's not on opam yet  (EDIT:
> looks ok now https://github.com/ocaml/opam-repository/pull/9379) and
> building from source fails on ubuntu for the same reason as
> https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2017-January/005200.html
> . Not sure how to patch that as I am not familiar with ocaml (yet).
>
> As you discovered gcc7 should work if you compile your own libmpack-c
> until they tag a release. I don't use it though.
>
>
> The result of compiling https://github.com/teto/neovim/tree/framac
> (neovim-dev + one commit to bypass a framac error) was compiled with:
> gcc --version
> gcc (Ubuntu 6.3.0-12ubuntu2) 6.3.0 20170406
>
> and should be available publicly at
> https://www.dropbox.com/s/rz7zqgpfdk17u4e/build.tar.gz?dl=0 (it's my
> "neovim/build" folder, ~250Mo) . If you have no dropbox account, click
> on the "small/hidden" link to skip the dropbox popup asking for
> registration.
>
> I launch frama-c via the script ./frama.sh at
> https://github.com/teto/neovim/tree/framac . something akin to
> "./frama.sh -verbose=40 -kernel-verbose=40".
>
> I have some time to investigate problems within my reach/help with
> adding it to the case studies. First I would like to understand the
> high level problem here:
> the files are already processed so how come the source uses 2
> different definitions of an integer ? Is it a problem with the neovim
> preprocessing options ?
>
> Best regards and once again thanks for your time.
>
> Matt
>

-- 
André Maroneze
Ingénieur-chercheur CEA/LIST
Laboratoire Sûreté et Sécurité des Logiciels


-------------- 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/20170602/a721ac18/attachment-0001.bin>