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

Hello,

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

>
> I1.) *Frama-C Nitrogen slicing results different in CLI/exported vs GUI,
> Why?:*
>
> I had an old version of Frama-c (Nitrogen-20111001) - installed via the
> ubuntu distribution.
> However,  I observed a strange/different results when slicing.
> Specifically, in some cases
> the slices generated using frama-c and using frama-c-gui were different.
>
> For instance, consider the attached program (“print_tokens.c“), using
> slicing instructions for:
>
> GUI:  "frama-c-gui -val-ignore-recursive-calls -slevel 999 -val
> print_tokens.c -main get_token -slice-return get_token"
> CLI/Exported: "frama-c -val-ignore-recursive-calls -slevel 999 -val
> print_tokens.c -main get_token -slice-return get_token -then-on 'Slicing
> export' -print -ocode get_token_StaticSlice.txt"
>
>
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.


>
> I2.) *Frama-C Sulfur cannot pre-process program that was pre-processed by
> older versions, why?:*
>
> Is there an explanation for this scenario? or better still what is the
> solution to this problem?
>
>
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.

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.


> Q1.) *What is “slice-return” behaviour for void methods?*
> When slicing with frama-c “slice-return” , what exactly happens in the
> case that
> the method does not have a return statement, i.e. void method? Should one
> consider
> “slice-calls” instead? I am interested in getting static slices for each
> method in a c program.
>

As fram-c -slicing-help indicates, -slice-return f selects as slicing
criterion the value returned by f, In the case of a void function, there is
no such value, thus nothing contributes to this value, and slicing will
consist in eliminating all statements that are not on the call stack
between main (or the argument of -main) and f. -slice-calls f will preserve
all side-effects of f which probably makes more sense for void-returning
functions.

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/807fcaec/attachment.html>