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

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>