--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on August 2012 ---
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>