--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on December 2014 ---
Hi I am working program slicing with frama-c. I compile and install frama-c-Neon-20140301. When I test some toy applications in the frama-c-Neon-20140301/tests/slicing, I find some problem. for example, such as the bts1445.i, the result log is [slicing] slicing requests in progress... [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization x ? {0} tests/slicing/bts1445.i:8:[value] entering loop for the first time [value] Recording results for main [value] done for function main [slicing] making slicing project 'Slicing'... [slicing] interpreting slicing requests from the command line... [slicing] warning: No internal slicing request from the command line. [slicing] warning: Adding an extra request on the entry point of function: main. [pdg] computing for function main tests/slicing/bts1445.i:10:[pdg] warning: no final state. Probably unreachable... [pdg] done for function main [slicing] applying all slicing requests... [slicing] applying 1 actions... [slicing] applying actions: 1/1... [slicing] exporting project to 'Slicing export'... [slicing] applying all slicing requests... [slicing] applying 0 actions... [sparecode] remove unused global declarations from project 'Slicing export tmp' [sparecode] removed unused global declarations in new project 'Slicing export' /* Generated by Frama-C */ void main(void) { return; } It seems that I do not get correct slice for main function. I try to slice it with frama-c -slice-calls main bts1445.i -then-on "Slicing export" -print It is the same result. The source code for bts1445.i is /* run.config OPT: -check -slice-calls main -then-on "Slicing export" -print OPT: -check -slice-calls f -main f -then-on "Slicing export" -print */ int x = 0; int main() { while(1) x=0; return x + 1; } int f() { while(1) x=0; return x + 1; } I think that a right slice is int x = 0; int main() { while(1) x=0; return x + 1; } Why is there the problem? There is any method to solve it? *Huizhan Yi,* Associate Professor, College of Computer, National University of Defense Technology,China Work Phone: 0731-84574650 WeiXin Num: huizhanyi QQ Num?562538519 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141219/5530476d/attachment.html>