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



Thanks so much for your timely reply.
Yeah, only those values x and y point-to are reassigned.
I want to obtain the out parameters of a function. In this function, x and
y are out parameters, x and y are pointers and the argument values x and y
point-to also reassigned in the function body.

Because x and y are not treated as def values. I don't know how to
automatically identify which parameter is out parameter in a function.

Any other solutions to this problem?

Best regards,

Ben

>* 1 int swap( int *x, int *y)*>* 2 {*>* 3 int temp1 = *x;*>* 4 int temp2 = *y;*>* 5 *x = temp2;*>* 6 *y = temp1;*>* 7 }*>**>* In this function, x and y are pointers to int value. In line 5 and 6, x and*>* y are reassigned to new values respectively. In my previous view, I thought*>* x and y are def value in these two statement. But when I use Usedef module*>* in frama-c to get the def values of these two statement. none defs*>* returend. Why frama-c do not treated x and y to be def values?*>**>* Looking forward to your reply.*>**>**>* Best regards,*>*   Ben*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120802/6ef78a99/attachment-0001.html>