--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on January 2015 ---
Thank you for your reply. Here is another example from susan.c I run with command line: frama-c -slice-calls put_image susan.c -then-on "Slicing export" -print I wish get a slice related with the parameter "in", why I get nothing? the attached file is susan.c and run log file. There is any general instruction to solve how to extract a slice and avoid wrongly using the slicer? *Huizhan Yi,* Associate Professor, College of Computer, National University of Defense Technology,China Work Phone: 0731-84574650 WeiXin Num: huizhanyi QQ Num?562538519 On Mon, Jan 12, 2015 at 7:23 AM, BAUDIN Patrick <Patrick.Baudin at cea.fr> wrote: > Hi, > The given slice is correct: the Slicing plug-in ensures that, each time > the function main terminates in the original code, it terminates in the > sliced code and preserves the effects of the call. > Since the function mains never terminate, it can do what it wants, and > nothing is the more reduced slice. > The explanation is given into these messages: > [pdg] computing for function main > bts1445.i:10:[pdg] warning: no final state. Probably unreachable... > [pdg] done for function main > [slicing] Nothing to select for unreachable return stmt of main > Regards, > -- Patrick Baudin > > Le 19/12/2014 17:45, Huizhan Yi a ?crit : > > 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'...ensures that, each time the > function f terminates in the original code, it terminates in the sliced > code > > [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 > > > _______________________________________________ > Frama-c-discuss mailing listFrama-c-discuss at lists.gforge.inria.frhttp://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150112/74afa7ee/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: susan.c Type: text/x-csrc Size: 59758 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150112/74afa7ee/attachment-0001.c> -------------- next part -------------- A non-text attachment was scrubbed... Name: susan.log Type: text/x-log Size: 229680 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150112/74afa7ee/attachment-0001.bin>