Frama-C-discuss mailing list archives

soremekun at st.cs.uni-saarland.de (Ezekiel Soremekun) · Thu, 1 Feb 2018 12:26:42 +0100

Hi Virgille, 

> 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).

Yes you are right, choosing "slicing export" in the project section of the menu showed the same slice as exported/CLI. Thanks, this clarifies things. 
I got confused by the EVA output, which is strange because I did not run EVA at all, as indicated in the command line, but now I observed this is triggered by â€œ-valâ€.

> 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.

Thanks, I tried this, but due to the old C style (pre-c99), it failed. I would stick to Nitrogen for now. 

Best regards, 
Ezekiel 

> On 31 Jan 2018, at 18:06, Virgile Prevosto <virgile.prevosto at m4x.org> wrote:
> 
> 
> 
> 2018-01-31 17:06 GMT+01:00 Ezekiel Soremekun <soremekun at st.cs.uni-saarland.de <mailto: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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180201/5d24ed6a/attachment.html>

Frama-C-discuss mailing list archives

[Frama-c-discuss] Frama-C Slicing Issues