1 #include <stdio.h>
2 #include <stdlib.h>
3 
foo1(void)4 char *foo1(void)
5 {
6   static char buf[1000];
7 
8   strcpy(buf, "hello");
9   return buf;
10 }
11 
foo2(void)12 /*@observer@*/ char *foo2(void)
13 {
14   static char buf[1000];
15 
16   strcpy(buf, "hello");
17   return buf;
18 }
19 
f(char outstr[])20 char *f (char outstr[])
21 {
22   return outstr;
23 }
24 
g(char * outstr)25 char *g (char *outstr)
26 {
27   return outstr;
28 }
29