--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on January 2018 ---
Hi, I have two issues (I1 & I2) and one other question (Q1) concerning slicing with Frama-c : 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" and the two slicing results saved to files (get_tokens_gui_slice.txt) and one the GUI (âget_tokens_clii_slice.txtâ), both files attached below. You can observe that both slices of get_token are significantly different. Is there a particular reason why this is the case, why both slices are different? and how do I solve this? The aim is to obtain the slices from CLI because my experiments involve hundreds of programs. I2.) Frama-C Sulfur cannot pre-process program that was pre-processed by older versions, why?: In order to solve problem (1) above, I installed the latest version of Frama-C (Sulfur-20171101) via opam. However, now I am experiencing a totally different problem, Frama-c can not pre-process the same program (âprint_tokens.câ) that was successfully pre-processed with the old version. I suspect this problem is due to some compiler or library issues with the new version of frama-c. Using the instruction: "frama-c -slevel 10 -val print_tokens.c -kernel-msg-key pp" I have obtained the errors in the file attached below - "sulfur_preprocesing_error.txtâ. First, I get some warnings about "Old style K&R codeâ. Then some user errors and a failure because Frama-c "Cannot resolve variable token_ptrâ. I have searched online for some hours and tried using different frama-c configurations, -cpp-command/ -cpp-ext flags, but to no avail. Is there an explanation for this scenario? or better still what is the solution to this problem? 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. Best regards, Ezekiel -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180131/261191a7/attachment-0005.html> -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: sulfur_preprocesing_error.txt URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180131/261191a7/attachment-0003.txt> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180131/261191a7/attachment-0006.html> -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: get_tokens_gui_slice.txt URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180131/261191a7/attachment-0004.txt> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180131/261191a7/attachment-0007.html> -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: get_tokens_cli_slice.txt URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180131/261191a7/attachment-0005.txt> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180131/261191a7/attachment-0008.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: print_tokens.c Type: application/octet-stream Size: 21038 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180131/261191a7/attachment-0001.obj> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180131/261191a7/attachment-0009.html>