--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on January 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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>