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"



That's really cool ! I've upgraded frama-c from opam and succeeded
completing the analysis thanks to your flag. I will try to fix the GUI
compilation otherwise I am not sure how to exploit the data.

> (e.g. from libuv ; such stubbing might be done via ACSL specifications
Any keyword I could lookup to ? I suppose I could generate the stubs
via pygccxml/castxml ? what's the usual thing ?

>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.
Thanks for the tip, I might very well do that even if I aim at
applying those techniques on "real" software.

>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).
This was part of my plan. Le francais ne devrait pas etre un problème :)

@+
Matt


2017-06-02 20:09 GMT+02:00 Andre Maroneze <Andre.OLIVEIRAMARONEZE at cea.fr>:
> 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
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss