File: sizeof.c

package info (click to toggle)
splint 1%3A3.1.2%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: buster
  • size: 21,012 kB
  • ctags: 23,302
  • sloc: ansic: 150,869; yacc: 3,465; sh: 3,034; makefile: 2,160; lex: 412
file content (20 lines) | stat: -rw-r--r-- 447 bytes parent folder | download | duplicates (7) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
 

extern void /*@alt char * @*/
  mystrncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2,
size_t n) 
  /*@modifies *s1@*/      /*@requires MaxSet(s1) >= ( n - 1) /\ MaxRead (s2) >= ( n - 1 ); @*/ /*@ensures MaxRead (s1) ==
MaxRead (s2) /\ MaxRead (s1) <= n; @*/; 


 void f(char *z) /*@requires MaxRead(z) >= 2; @*/
{
char x[3];
char y[3];

mystrncpy (x, z, 3);
mystrncpy (y, z, 3);

x[(sizeof x)] = 'i';
y[((sizeof y) - 1)] = '0';

}