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 Slicing Issues

2018-01-31 17:06 GMT+01:00 Ezekiel Soremekun <
soremekun at st.cs.uni-saarland.de>:

> Hi Virgile,
>
> GUI and command line should give identical results. Are you sure that you
> extracted the get_token code from the appropriate project in the GUI case?
> By default, the GUI displays the original project (i.e. unsliced in your
> case), and not the latest created, which is admitedly not the most
> intuitive action to do.
>
> Yes, I am sure, in the frama-c-gui I have both the slice and the original
> code side by side: attached is a screenshot of the GUI ("frama-c-gui.png").
>


I'm sorry to insist on that point, but your screenshot suggests otherwise.
Notably, the code highlighted in red at the bottom of the window indicates
that this is a project where EVA has been launched, which is not the case
by default in the project created by the slicing (and the command line you
gave in your previous mail did not indicate a relaunch of EVA on the new
project). In the GUI, you can select the project that is displayed in the
Project menu (where you should have two radio buttons, one 'default' and
one 'slicing export' or something equivalent).


> The warning about undeclared functions tend to signal that some includes
> of the stdlib are missing in print_token.c. It might have been the case
> that in Nitrogen, using the system's libc, those include were indirectly
> done, but this is not the case with Frama-C's own libc, which is now the
> default. In particular, print_token.c should include stdlib.h and string.h
> and not just stdio.h.
>
> Yes, I believe this is the issue, but how can i ensure the frama-c sulfur
> version (with opam) uses the system libc in this case ?
>
>
As mentioned by frama-c -kernel-help, you can use option
-no-frama-c-stdlib. Be aware though that standard headers usually contain
compiler and OS specific extensions that may not be understood by Frama-C.


>
> The error about the return without a value come from the fact that
> print_token.c uses a very old style (pre C99) for function declarations,
> and in particular did not bother to specify the return type of unget_char,
> which Frama-C interprets, as in C90 and before (and as gcc does, even
> though it only emits a warning about the return), as returning int. Just
> add void before unget_char to have a valid prototype.
>
> The error about numeric_case is also due to the the way print_tokens.c
> declare things: numeric_case is declared with an empty list of argument.
> Later, when it is used, its type is computed by Frama-C according to the
> typing rules for functions without argument lists, meaning in particular
> that all integral type less than int are implicitly promoted to int. When
> even later the definition is encontered, with the proper prototype, there
> is indeed a type mismatch. Again the fix is to give a proper prototype to
> numeric_case in line 15 (and actually to all the functions that don't have
> one yet below that). This should also get rid of the internal failure,
> which is a real bug, but should probably only manifest in circumstances
> like this (declaration without argument list, use of the function, and
> later definition with types incompatible with the default assigned ones),
> i.e. when the program is not conforming to the C99 standard.
>
>
> For both errors, I agree this is the issue, but I would not like to edit
> the program, as these are benchmark programs for an experiment, and any
> changes may affect the (comparative) results or be considered biased.
> Besides, there are numerous versions of such programs (>200 programs) in my
> dataset,
> so it is infeasible to actually edit all such programs.
>
> Hence, the question is - is there a way to allow for older C style (Pre
> C99/C90) in the frama-c sulfur version (just like it worked in the Nitrogen
> version).
>
>
>
No, this is not possible as far as I know. Being too lenient in what
Frama-C accepts as correctly-typed programs leads to all sorts of issues
later in the analyzes, which is why newer versions tends to be stricter in
this regard. In addition, supporting C constructions that are obsolete
since little less than 20 years will probably not be very high on our
priority list, unless of course there is such a need in a project we are
part of, or a specific demand for that in the frame of a maintenance
contract. On the other hand, patches can of course be considered for
inclusion.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180131/881b3784/attachment.html>