Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / include / io_frontend.h @ 4d841db7

History | View | Annotate | Download (744 Bytes)

1 22fe1c93 ploc
#ifndef _IO_FRONTEND
2
#define _IO_FRONTEND
3
4 375cbca2 ploc
/* Print a prompt ? ************************/
5 22fe1c93 ploc
extern int ISATTY;
6
7
/* Standard Input procedures **************/
8
9
/*@ assigns *n; */
10 6fa45cb6 ploc
extern _Bool _get_bool(FILE* file, char* n);
11 22fe1c93 ploc
12
/*@ assigns *n; */
13 6fa45cb6 ploc
extern int _get_int(FILE* file, char* n);
14 22fe1c93 ploc
15
/*@ assigns *n; */
16 6fa45cb6 ploc
extern double _get_double(FILE* file, char* n);
17 22fe1c93 ploc
18
/* Standard Output procedures **************/
19
/*@ assigns \nothing; */
20 6fa45cb6 ploc
extern void _put_bool(FILE* file, char* n, _Bool _V);
21 22fe1c93 ploc
22
/*@ assigns \nothing; */
23 6fa45cb6 ploc
extern void _put_int(FILE* file, char* n, int _V);
24 22fe1c93 ploc
25
/*@ assigns \nothing; */
26 9a7268ba ploc
extern void _put_float(FILE* file, char* n, float _V, int PREC);
27
28
/*@ assigns \nothing; */
29
extern void _put_double(FILE* file, char* n, double _V, int PREC);
30 22fe1c93 ploc
31
#endif