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] context-insensitive and intra-procedure slicing in frama-c

  • Subject: [Frama-c-discuss] context-insensitive and intra-procedure slicing in frama-c
  • From: abiao.yang at gmail.com (Yang)
  • Date: Wed, 1 Aug 2012 22:31:58 +0800
Dear all:

I want to perform context-insensitive and intra-procedure program slicing
in frama-c.

But slicing plugin in frama-c is based on value analysis. Value analysis is
context-sensivive and path-sensitive. So the slicing result is not i really
want. I also try to solve this problem by the PDG module. But
unfortunately, PDG module also based on value analysis.

Any suggestions to solve this problem?

here is an example to describe my problem. the following max function is to
return the maximum value of a, b, and c.

int max( int a, int b, int c)
{
int maxv = a;

if( maxv < b )
maxv = b;
 if( maxv < c )
maxv = c;

return maxv;
 }

I want to obtain those statements which may influcence the return value of
this function. While in context sensitive, value analysis in frama-c will
eliminate those dead codes from this function. so the slicing result will
not include those statements in dead codes.

Others may argue that why not change those arguments while call this
function. In C libraries, those functions are to be used. May not having
been used before. But i still want to perform some special analysis to
those functions.

Looking forward to your reply.


Best regards,
 Ben
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120801/aeeca1b2/attachment.html>