00001 /* f.c */
00002 #include "f.h"
00003 void f()
00004 {
00005         char tmp[56]; /*@\label{lst:f_tmp}@*/
00006 }