File: stdio.h

package info (click to toggle)
splint 1%3A3.1.2%2Bdfsg-5
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid
  • size: 21,004 kB
  • sloc: ansic: 150,869; yacc: 3,465; sh: 3,034; makefile: 2,157; lex: 412
file content (148 lines) | stat: -rw-r--r-- 5,102 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
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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
/*
** stdio.h - Unix Specification
*/

/*
** evans 2001-12-30: added from http://www.opengroup.org/onlinepubs/007908799/xsh/stdio.h.html
*/

/*@constant unsignedintegraltype BUFSIZ@*/ 
/*@constant unsignedintegraltype FILENAME_MAX@*/
/*@constant unsignedintegraltype FOPEN_MAX@*/
/*@constant _Bool _IOFBF@*/
/*@constant _Bool _IOLBF@*/
/*@constant _Bool _IONBF@*/
/*@constant unsignedintegraltype L_ctermid@*/
/*@constant unsignedintegraltype L_cuserid@*/
/*@constant unsignedintegraltype L_tmpnam@*/
/*@constant unsignedintegraltype SEEK_CUR@*/
/*@constant unsignedintegraltype SEEK_END@*/
/*@constant unsignedintegraltype SEEK_SET@*/
/*@constant unsignedintegraltype TMP_MAX@*/

/*@constant observer char *P_tmpdir@*/

void clearerr (FILE *stream) /*@modifies *stream@*/ ;

/*@dependent@*/ char *ctermid (/*@returned@*/ /*@null@*/ char *) /*@*/ ;
   /* Result may be static pointer if parameter is NULL, otherwise is fresh. */

  //     *@requires maxSet(s) >= ( L_ctermid - 1) @*/ *ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 */
  /*DRL 9-11-2001 I've modified the definition in ansi.h to remove modifies SystemState and I've added a requires and ensures*/ ;
  
/*check returns*/     
/* cuserid is in the 1988 version of POSIX but removed in 1990 */

char *cuserid (/*@null@*/ /*@out@*/ /*@returned@*/ char *s)
  /*@warn legacy "cuserid is obsolete"@*/ 
  /*@modifies *s@*/
     // *@requires maxSet(s) >= ( L_ctermid - 1) @*/ *@ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0  /\ maxRead(result) <= ( L_ctermid - 1) /\ maxRead(result) >= 0 @*/
     ;

/* in standard.h: int fclose (FILE *stream) @modifies *stream, errno, fileSystem;@ */
  
/*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type)
    /*@modifies errno, fileSystem@*/;

/* feof, ferror fflush, fgetc, fgetpos, fgets - in standard.h */

int fileno (/*@notnull@*/ FILE *)
  /*:errorcode -1:*/ 
  /*@modifies errno@*/ ;

void flockfile (/*@notnull@*/ FILE *f)
   /*@modifies f, fileSystem@*/ ;

/* fopen, fprintf, fputc, fread, frepoen, fscanf, etc. in standard.h */


int fseeko (FILE *stream, off_t offset, int whence)
   /*:errorcode -1:*/
   /*@modifies stream, errno@*/ ;

off_t ftello(FILE *stream)
   /*:errorcode -1:*/ /*@modifies errno*/ ;

int ftrylockfile(FILE *stream)
   /*:errorcode !0:*/
   /*@modifies stream, fileSystem, errno*/ ;

void funlockfile (FILE *stream)
   /*@modifies stream, fileSystem*/ ;

int getc_unlocked(FILE *stream)
   /*@warn multithreaded "getc_unlocked is a thread unsafe version of getc"@*/
   /*@modifies *stream, fileSystem, errno@*/ ;

int getchar_unlocked (void)
   /*@warn multithreaded "getchar_unlocked is a thread unsafe version of getchar"@*/
   /*@globals stdin@*/
   /*@modifies *stdin, fileSystem@*/ ;

/*@unchecked@*/ char *optarg;
/*@unchecked@*/ int optind;
/*@unchecked@*/ int optopt;
/*@unchecked@*/ int opterr;
/*@unchecked@*/ int optreset;

int getopt (int argc, char * const *argv, const char *optstring)
   /*@warn legacy@*/ 
   /*@globals optarg, optind, optopt, opterr, optreset@*/
   /*@modifies optarg, optind, optopt@*/
   /*@requires maxRead(argv) >= (argc - 1) @*/
   ;

int getw (FILE *stream)
   /*@warn legacy@*/ 
   /*:errorcode EOF:*/
   /*@modifies fileSystem, *stream, errno@*/ ;

int pclose(FILE *stream)
   /*:errorcode -1:*/
   /*@modifies fileSystem, *stream, errno@*/ ;

/*@dependent@*/ /*@null@*/ FILE *popen (const char *command, const char *mode)
   /*:errorcode NULL:*/
   /*@modifies fileSystem, errno@*/ ;

int putc_unlocked (int, FILE *stream)
   /*@warn multithreaded "putc_unlocked is a thread unsafe version of putc"@*/
   /*:errorcode EOF:*/
   /*@modifies fileSystem, *stream, errno@*/ ;

int putchar_unlocked(int)
   /*@warn multithreaded "putchar_unlocked is a thread unsafe version of putchar"@*/
   /*:errorcode EOF:*/
   /*@modifies fileSystem, *stdout, errno@*/ ;

int putw(int, FILE *stream)
   /*@warn legacy@*/ 
   /*:errorcode EOF:*/
   /*@modifies fileSystem, *stdout, errno@*/ ;

int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;
void rewind (FILE *stream) /*@modifies *stream, fileSystem, errno@*/ ;
  
/* evans 2002-07-09: snprintf moved to standard.h (its in ISO C99 now) */

/*@null@*/ char *tempnam (char *dir, /*@null@*/ char *pfx) 
    /*@modifies internalState, errno@*/
    /*@ensures maxSet(result) >= 0 /\ maxRead(result) >= 0 @*/
    /*@warn toctou "Between the time a pathname is created and the file is opened, it is possible for some other process to create a file with the same name. Use tmpfile instead."*/
    /*drl added errno 09-19-001 */
    ;


/*@null@*/ FILE *tmpfile (void) 
   /*@modifies fileSystem, errno@*/
   /*drl added errno 09-19-001 */
   ;

/*@observer@*/ char *tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) 
   /*@modifies *s, internalState @*/
   //      *@requires maxSet(s) >= (L_tmpnam - 1) @*
   /*@warn toctou "Between the time a pathname is created and the file is opened, another process may create a file with the same name. Use tmpfile instead."*/
   ;