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

  • Subject: [Frama-c-discuss] context-insensitive and intra-procedure slicing in frama-c
  • From: abiao.yang at gmail.com (Yang)
  • Date: Sun, 5 Aug 2012 14:28:29 +0800
  • In-reply-to: <CAA1cxui_S=MvBY6TqrTDDPW=vLrePizAkrC_ayq--0rjEPp57A@mail.gmail.com>
  • References: <CAA1cxui_S=MvBY6TqrTDDPW=vLrePizAkrC_ayq--0rjEPp57A@mail.gmail.com>
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>