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