1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
|
<A NAME="line0"></A><html><head>
<title>mstringnn.c</title>
</head><body>
<h3>mstringnn.c</h3>
<PRE>
<A NAME="line1"></A>typedef /*@abstract@*/ /*@null@*/ char *mstring;
<A NAME="line2"></A>
<A NAME="line3"></A>static mstring mstring_createNew (int x) ;
<A NAME="line4"></A>
<A NAME="line5"></A>mstring mstring_space1 (void)
<A NAME="line6"></A>{
<A NAME="line7"></A> mstring m = mstring_createNew (1);
<A NAME="line8"></A>
<A NAME="line9"></A> /* error, since m could be NULL */
<A NAME="line10"></A> *m = ' '; *(m + 1) = '\0';
<A NAME="line11"></A> return m;
<A NAME="line12"></A>}
<A NAME="line13"></A>
<A NAME="line14"></A>static /*@notnull@*/ mstring mstring_createNewNN (int x) ;
<A NAME="line15"></A>
<A NAME="line16"></A>mstring mstring_space2 (void)
<A NAME="line17"></A>{
<A NAME="line18"></A> mstring m = mstring_createNewNN (1);
<A NAME="line19"></A>
<A NAME="line20"></A> /* no error, because of notnull annotation */
<A NAME="line21"></A> *m = ' '; *(m + 1) = '\0';
<A NAME="line22"></A> return m;
<A NAME="line23"></A>}
</pre>
</body></html>
|