--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on December 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] about slicing



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>