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

  • Subject: [Frama-c-discuss] Frama-C Slicing Issues
  • From: soremekun at st.cs.uni-saarland.de (Ezekiel Soremekun)
  • Date: Wed, 31 Jan 2018 14:20:00 +0100
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>