--- layout: fc_discuss_archives title: Message 5 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 Ben,
    Did you have a look at the effect of -lib-entry option on the Value 
analysis?
    That seems to solve the problem you described on your max function.
Kind regards,
Patrick.

Le 01/08/2012 16:31, Yang a ?crit :
> 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
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120802/f947d80f/attachment.html>