--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on August 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [frama-c] def information of statement which contain a pointer value



Dear all:
 I want to get def information of a statement in frama-c. While there
exists a pointer in a statement, the results is not what I thought it
should be.
 The following stupid function is to exchange two values.

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/a2a24fed/attachment.html>