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]

[no subject]

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


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

Best regards, 
Ezekiel 



> On 31 Jan 2018, at 16:02, Virgile Prevosto <virgile.prevosto at m4x.org> wrote:
> 
> Hello,
> 
> 2018-01-31 14:20 GMT+01:00 Ezekiel Soremekun <soremekun at st.cs.uni-saarland.de <mailto: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
> _______________________________________________
> 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/20180131/8d73a0ae/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: frama-c-gui.png
Type: image/png
Size: 394262 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180131/8d73a0ae/attachment-0001.png>