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