--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on December 2014 ---
I have seen some documents about frama-c. It seems that sometimes some slicing problems originate from its dependence analysis, such as value analysis and PDG. So I want to know whether in frama-c, there are some mechanisms/pragmas that enable users to give fragma-c tool some hints and help frama-c improve its value analysis and PDG? *Huizhan Yi,* Associate Professor, College of Computer, National University of Defense Technology,China Work Phone: 0731-84574650 WeiXin Num: huizhanyi QQ Num?562538519 On Fri, Dec 19, 2014 at 11:45 AM, Huizhan Yi <huizhanyi at gmail.com> wrote: > 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/20141229/6fc86a8a/attachment.html>