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 undefined behaviour during preprocessing

Dear Rooney,

Your problem might be related to the configuration of curl, which is a 
very complex software, with several different configurable options, and 
heavy usage of libraries (not only C99, but also POSIX and functions 
which are neither C99 nor POSIX). The approach based on preprocessing 
the sources and then feeding them to Frama-C is not always ideal, so we 
propose another one, based on mimicking the build process of the 
software in order to incorporate the sources directly.

The general answer to this kind of issue is that, currently, the 
preprocessing setup of any complex set of files is not directly handled 
by Frama-C. Ongoing efforts will likely improve this in future releases, 
but currently the user must know how to build the software and transform 
the compiler commands used during build into one that is suitable for 
Frama-C. The main issue is that virtually every software is compiled via 
separate compilation (with several calls to the compiler, one for each 
object file), but some Frama-C analyses, such as EVA, require a 
whole-program setup, where all the sources (with the appropriate 
preprocessor definitions and includes) are given at once, in a single 
command.

In the case of curl (as well as almost every open source C software that 
follows GNU-style build conventions), there is a configure stage, where 
several features are optionally enabled or disabled, according to 
whether they are detected in the host system. Many of these use non-C99 
functions that are currently unavailable in the Frama-C standard 
library. In other words, you are configuring the software for a given 
environment (using your host machine), but Frama-C expects a somewhat 
idealized environment, composed mainly by C99 and some POSIX files. This 
mismatch leads to situations where headers fail to parse with Frama-C.

However, in the case of curl itself, we have already tried some work on 
it, but it was never finalized. I just committed this partial work to:

https://github.com/maroneze/open-source-case-studies

That repository is a fork of 
https://github.com/Frama-C/open-source-case-studies, whose purpose is to 
help users deal with this step of the preparation of source files, 
besides giving a more fleshed-out value analysis from the start. The 
next release of Frama-C should be followed by an update of the official 
open-source-case-studies repository, to reflect the evolution of the 
analysis scripts.

In my repository, you'll find a directory curl-7.54.1 which contains a 
copy of the curl sources, plus two extra files:

- configure_for_oscs.sh : this is a script which will call ./configure 
with a set of flags disabling some optional features; ideally we would 
like to keep them enabled, but for a first analysis, it is often simpler 
to disable these. You should run this from its directory, in order to 
create the necessary headers with proper #ifdefs, that should allow 
Frama-C to parse the sources successfully;

- GNUmakefile : this is a Makefile for running Frama-C on the sources, 
with two main targets:

   - parse: running "make parse" should parse the sources and save the 
result to curl.parse/framac.sav;

   - eva: running "make eva" should run the value analysis on the main 
function of the curl command-line application; note that this has NOT 
been properly setup yet and will result in a very imprecise analysis.

This GNUmakefile follows the style of the other makefiles available in 
open-source-case-studies. It requires Make >= 4.0. It has been tested 
with the beta release of Frama-C Sulfur 
(https://github.com/Frama-C/Frama-C-snapshot/wiki/Frama-C-Sulfur-20171101-beta), 
which should be installed and in the PATH.

Note that one of the files used by curl requires the header 
"sys/xattr.h", which is not available in the Frama-C standard library in 
Sulfur. Copying the header from the glibc should work, for instance with:

cp /usr/include/sys/xattr.h $(frama-c -print-path)/libc/sys/

(Note that such copying rarely works, so one should avoid mixing headers 
from the Frama-C libc and those in the system; but in this case in 
particular, the workaround seems fine.)


So, to sum up the situation:

1. Preprocessing and parsing software that has several optional features 
and uses external libraries is not trivial in Frama-C, so don't expect 
it to work out of the box;
2. In the case of curl in particular, we've already done part of the 
effort, so parsing should be easy, given the script and makefile:
   a. Install Frama-C Sulfur (beta);
   b. "Patch" Frama-C's standard library by adding sys/xattr.h;
   c. Run ./configure_for_oscs.sh and then `make parse`;
   d. To directly retrieve the results of the parsing, use `frama-c 
-load curl.parse/framac.sav`
3. Due to the complexity and size of curl, trying to run EVA or any 
derived plug-in (such as Slicing) on the main function of curl will give 
unusable results without proper parametrization. Unless you try with a 
different main function, possibly with -lib-entry, you'll probably be 
unable to extract much useful data.

Hopefully this should help. Do not hesitate to read the GNUmakefile to 
see what exact options are being used by the parsing, as well as the 
list of source files used. There are no guarantees that the list is 
correct and the options are the best ones; as I said, this is some work 
that has not been finalized, but should at least give you a good 
starting point.

Regards,

On 13/11/17 13:05, Rooney wrote:
>
>
> Dear Frama-C Developers,
> I’m using your project with slicing and metrics opetion, I have found 
> some problems I can not fix, while I’m facing a deadline I decided to 
> ask for help from you.
> I use the follwing command:
>
> gcc -E -C -I.  -dD -D__FRAMAC__  -nostdinc -D__FC_MACHDEP_X86_32 
> -I/usr/share/frama-c/libc -I../include -I../lib -o tool_help.i tool_help.c
> and it will creat tool_help.i, but when I use this .i file it fails 
> with frame-c with the follwing error:
>
> [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i 
> (no preprocessing)
> [kernel] Parsing tool_help.i (no preprocessing)
> [kernel] syntax error at /root/old/curl/lib/curl_setup_once.h:175:
>          173   #ifndef sread
>          174     /* */
>          175     Error Missing_definition_of_macro_sread
>  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>          176     /* */
>          177   #endif
> [kernel] Frama-C aborted: invalid user input.
>
> The code is from curl github <https://github.com/curl/curl>, (/curl/src).
> Please if you kbow what’s wrong, let me know. I have already tried 
> evry possible workaround. Thanks in advance.
>
> —
> Regards,
> Rooney
>
>
>
> _______________________________________________
> 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
Ingénieur-chercheur CEA/LIST
Laboratoire Sûreté et Sécurité des Logiciels

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20171113/44a1bf3e/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/20171113/44a1bf3e/attachment-0001.bin>