]>
Commit | Line | Data |
---|---|---|
41320549 | 1 | |
2 | extern void /*@alt char * @*/ | |
3 | mystrncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, | |
4 | size_t n) | |
d9a28762 | 5 | /*@modifies *s1@*/ /*@requires MaxSet(s1) >= ( n - 1) /\ MaxRead (s2) >= ( n - 1 ); @*/ /*@ensures MaxRead (s1) == |
dcaf75ea | 6 | MaxRead (s2) /\ MaxRead (s1) <= n; @*/; |
41320549 | 7 | |
80ee600a | 8 | |
d9a28762 | 9 | void f(char *z) /*@requires MaxRead(z) >= 2; @*/ |
41320549 | 10 | { |
11 | char x[3]; | |
12 | char y[3]; | |
13 | ||
14 | mystrncpy (x, z, 3); | |
15 | mystrncpy (y, z, 3); | |
16 | ||
17 | x[(sizeof x)] = 'i'; | |
18 | y[((sizeof y) - 1)] = '0'; | |
19 | ||
20 | } |