--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on August 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] context-insensitive and intra-procedure slicing in frama-c



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>