noexpand always false.

[splint.git] / imports / stdio.lcl

/*
** stdio.lcl
**
** based on /usr/include/stdio.h on red-cross
*/

imports <stdlib> ;

/*
** we need to allow casts to and from these types...
** they should be exposed, but unknown type.
*/

immutable type FILE;

typedef void *va_list;
typedef void *fpos_t;

FILE *stdin;
FILE *stdout;
FILE *stderr;

constant int EOF ;

| int : char | getc (FILE *stream )
{
   ensures true;
}

| int : char | getchar (void)
{
   ensures true;
}

| int : void | putc (| int : char | c, FILE *stream)
{
   ensures true;
}

int putchar (|int : char| c)
{
   ensures true;
}

| int : bool | feof (FILE *stream)
{
   ensures true;
}

| int : bool | ferror (FILE *stream )
{
   ensures true;
}

int fileno (FILE *stream)
{
   ensures true;
}

int _filbuf (FILE *p)
{
   ensures true;
}

int _flsbuf (unsigned char x, FILE *p)
{
   ensures true;
}

void clearerr (FILE *stream)
{
   ensures true;
}
 
| int : void | fclose (FILE *stream )
{
   ensures true;
}

FILE * fdopen (int filedes, char *ttype)
{
   ensures true;
}

| int : void | fflush (FILE *stream )
{
   ensures true;
}

| int : char | fgetc (FILE *stream )
{
   ensures true;
}

int fgetpos (FILE *stream, fpos_t *pos )
{
   ensures true;
}

char *fgets (char *s, int n, FILE *stream )
{
   ensures true;
}


FILE *fopen (char *filename, char *ttype )
{
   ensures true;
}

printflike
| int : void | fprintf (FILE *stream, char *format, ...)
{
   ensures true;
}

printflike
| int : void | sprintf (FILE *stream, char *format, ...)
{
   ensures true;
}

| int : void | fputc (| int : char | c, FILE *stream )
{
   ensures true;
}

| int : void | fputs( char *s, FILE *stream )
{
   ensures true;
}

size_t fread (void *ptr, size_t size,
	      size_t nitems, FILE *stream )
{
   ensures true;
}
 
FILE *freopen (char *filename, char *ttype,
	       FILE *stream)
{
   ensures true;
}

scanflike
int fscanf (FILE *stream, char *format, ... )
{
   ensures true;
}

| int : void | fseek (FILE *stream, long offset, int ptrname)
{
   ensures true;
}

int fsetpos (FILE *stream, fpos_t *pos)
{
   ensures true;
}

long ftell (FILE *stream)
{
   ensures true;
}

size_t fwrite (void *ptr, size_t size,
	       size_t nitems, FILE *stream)
{
   ensures true;
}

char *gets (char *s)
{
   ensures true;
}
 
void perror (char *s)
{
   ensures true;
}

FILE  *popen (char *command, char *ttype)
{
   ensures true;
}

| int : void | ungetc(char c, FILE *stream)
{
   ensures true;
}

printflike
| int : void | printf (char *format, ...)
{
   ensures true;
}
 
| int : void | puts (char *s)
{
   ensures true;
}
 
| int : bool | remove (char *filename)
{
   ensures true;
}

| int : bool | rename (char *from, char *to)
{
   ensures true;
}

void rewind (FILE *stream)
{
   ensures true;
}

scanflike
| int : void | scanf (char *format, ...)
{
   ensures true;
}
 
void setbuf (FILE *stream, char *buf)
{
   ensures true;
}

int setvbuf (FILE *stream, char *buf,
	     int ttype, size_t size )
{
   ensures true;
}

scanflike
| int : void | sscanf (char *s, char *format, ...)
{
   ensures true;
}

FILE *tmpfile( void )
{
   ensures true;
}
 
char *tmpnam (char *s)
{
   ensures true;
}