--- layout: fc_discuss_archives title: Message 18 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 Patrick:

Thanks for your kindly help.
I have been tried many times the option you provide these days.
"frama-c-gui -lib-entry example.c"
It seems that when i going to slicing this function. it also need to do
value analysis from the main function. So those dead codes also eliminate.

But fortunately i solved this problem by using another command:
"frama-c-gui -val -main max example.c"
(max function in the file: example.c)
while i use this command, it will not eliminate dead codes. The slicing is
result is also correct.
Thanks again.

Best regards,
 Ben

> 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>
> *>* http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> *
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120805/4c91a073/attachment.html>