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] about slicing

  • Subject: [Frama-c-discuss] about slicing
  • From: huizhanyi at gmail.com (Huizhan Yi)
  • Date: Fri, 19 Dec 2014 11:45:25 -0500
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>