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



Ben,

> Why frama-c do not treated x and y to be def values?

Because x and y are not assigned.
What is reassigned is *x and *y!

Regards,
Patrick.

Le 02/08/2012 03:17, Yang a ?crit :
> 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
>
>
>
> _______________________________________________
> 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


-- 
Patrick Baudin, DILS/LSL, B?t. 862,
Point Courrier n? 174
Institut CARNOT CEA LIST,
CEA Saclay Nano-INNOV,
91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120802/746aec88/attachment.html>