Skip to content

Commit 3f1ea29

Browse files
tautschnigtautschnig
committed
clang-format compatible preprocessor instructions
1 parent 80e2aa8 commit 3f1ea29

File tree

1 file changed

+72
-72
lines changed

1 file changed

+72
-72
lines changed

‎src/ansi-c/library/stdio.c

Lines changed: 72 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -75,27 +75,27 @@ inline FILE *fopen(const char *filename, const char *mode)
7575
__CPROVER_HIDE:;
7676
(void)*filename;
7777
(void)*mode;
78-
#ifdef __CPROVER_STRING_ABSTRACTION
78+
#ifdef __CPROVER_STRING_ABSTRACTION
7979
__CPROVER_assert(__CPROVER_is_zero_string(filename), "fopen zero-termination of 1st argument");
8080
__CPROVER_assert(__CPROVER_is_zero_string(mode), "fopen zero-termination of 2nd argument");
81-
#endif
81+
#endif
8282

8383
FILE *fopen_result;
8484

8585
__CPROVER_bool fopen_error=__VERIFIER_nondet___CPROVER_bool();
8686

87-
#if !defined(__linux__) || defined(__GLIBC__)
87+
#if !defined(__linux__) || defined(__GLIBC__)
8888
fopen_result=fopen_error?NULL:malloc(sizeof(FILE));
89-
#else
89+
#else
9090
// libraries need to expose the definition of FILE; this is the
9191
// case for musl
9292
fopen_result=fopen_error?NULL:malloc(sizeof(int));
93-
#endif
93+
#endif
9494

95-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
95+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
9696
__CPROVER_set_must(fopen_result, "open");
9797
__CPROVER_cleanup(fopen_result, fclose_cleanup);
98-
#endif
98+
#endif
9999

100100
return fopen_result;
101101
}
@@ -112,11 +112,11 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f)
112112
__CPROVER_HIDE:;
113113
(void)*filename;
114114
(void)*mode;
115-
#if !defined(__linux__) || defined(__GLIBC__)
115+
#if !defined(__linux__) || defined(__GLIBC__)
116116
(void)*f;
117-
#else
117+
#else
118118
(void)*(char*)f;
119-
#endif
119+
#endif
120120

121121
return f;
122122
}
@@ -137,13 +137,13 @@ int __VERIFIER_nondet_int();
137137

138138
inline int fclose(FILE *stream)
139139
{
140-
__CPROVER_HIDE:;
141-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
140+
__CPROVER_HIDE:;
141+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
142142
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
143143
"fclose file must be open");
144144
__CPROVER_clear_must(stream, "open");
145145
__CPROVER_set_must(stream, "closed");
146-
#endif
146+
#endif
147147
int return_value=__VERIFIER_nondet_int();
148148
free(stream);
149149
return return_value;
@@ -166,18 +166,18 @@ inline FILE *fdopen(int handle, const char *mode)
166166
__CPROVER_HIDE:;
167167
(void)handle;
168168
(void)*mode;
169-
#ifdef __CPROVER_STRING_ABSTRACTION
169+
#ifdef __CPROVER_STRING_ABSTRACTION
170170
__CPROVER_assert(__CPROVER_is_zero_string(mode),
171171
"fdopen zero-termination of 2nd argument");
172-
#endif
172+
#endif
173173

174-
#if !defined(__linux__) || defined(__GLIBC__)
174+
#if !defined(__linux__) || defined(__GLIBC__)
175175
FILE *f=malloc(sizeof(FILE));
176-
#else
176+
#else
177177
// libraries need to expose the definition of FILE; this is the
178178
// case for musl
179179
FILE *f=malloc(sizeof(int));
180-
#endif
180+
#endif
181181

182182
return f;
183183
}
@@ -205,10 +205,10 @@ inline FILE *_fdopen(int handle, const char *mode)
205205
__CPROVER_HIDE:;
206206
(void)handle;
207207
(void)*mode;
208-
#ifdef __CPROVER_STRING_ABSTRACTION
208+
#ifdef __CPROVER_STRING_ABSTRACTION
209209
__CPROVER_assert(__CPROVER_is_zero_string(mode),
210210
"fdopen zero-termination of 2nd argument");
211-
#endif
211+
#endif
212212

213213
FILE *f=malloc(sizeof(FILE));
214214

@@ -241,12 +241,12 @@ char *fgets(char *str, int size, FILE *stream)
241241
#endif
242242
}
243243

244-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
244+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
245245
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
246246
"fgets file must be open");
247-
#endif
247+
#endif
248248

249-
#ifdef __CPROVER_STRING_ABSTRACTION
249+
#ifdef __CPROVER_STRING_ABSTRACTION
250250
int resulting_size;
251251
__CPROVER_assert(__CPROVER_buffer_size(str)>=size, "buffer-overflow in fgets");
252252
if(size>0)
@@ -255,7 +255,7 @@ char *fgets(char *str, int size, FILE *stream)
255255
__CPROVER_is_zero_string(str)=!error;
256256
__CPROVER_zero_string_length(str)=resulting_size;
257257
}
258-
#else
258+
#else
259259
if(size>0)
260260
{
261261
int str_length=__VERIFIER_nondet_int();
@@ -268,7 +268,7 @@ char *fgets(char *str, int size, FILE *stream)
268268
if(!error)
269269
str[str_length]='\0';
270270
}
271-
#endif
271+
#endif
272272

273273
return error?0:str;
274274
}
@@ -302,10 +302,10 @@ inline size_t fread(
302302
#endif
303303
}
304304

305-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
305+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
306306
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
307307
"fread file must be open");
308-
#endif
308+
#endif
309309

310310
for(size_t i=0; i<bytes; i++)
311311
{
@@ -340,10 +340,10 @@ inline int feof(FILE *stream)
340340
#endif
341341
}
342342

343-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
343+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
344344
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
345345
"feof file must be open");
346-
#endif
346+
#endif
347347

348348
return return_value;
349349
}
@@ -372,10 +372,10 @@ inline int ferror(FILE *stream)
372372
#endif
373373
}
374374

375-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
375+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
376376
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
377377
"feof file must be open");
378-
#endif
378+
#endif
379379

380380
return return_value;
381381
}
@@ -402,16 +402,16 @@ __CPROVER_HIDE:;
402402

403403
int return_value=__VERIFIER_nondet_int();
404404

405-
#if !defined(__linux__) || defined(__GLIBC__)
405+
#if !defined(__linux__) || defined(__GLIBC__)
406406
(void)*stream;
407-
#else
407+
#else
408408
(void)*(char*)stream;
409-
#endif
409+
#endif
410410

411-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
411+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
412412
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
413413
"fileno file must be open");
414-
#endif
414+
#endif
415415

416416
return return_value;
417417
}
@@ -430,9 +430,9 @@ inline int fputs(const char *s, FILE *stream)
430430
// just return nondet
431431
__CPROVER_HIDE:;
432432
int return_value=__VERIFIER_nondet_int();
433-
#ifdef __CPROVER_STRING_ABSTRACTION
433+
#ifdef __CPROVER_STRING_ABSTRACTION
434434
__CPROVER_assert(__CPROVER_is_zero_string(s), "fputs zero-termination of 1st argument");
435-
#endif
435+
#endif
436436
(void)*s;
437437

438438
if(stream != stdout && stream != stderr)
@@ -444,10 +444,10 @@ inline int fputs(const char *s, FILE *stream)
444444
#endif
445445
}
446446

447-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
447+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
448448
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
449449
"fputs file must be open");
450-
#endif
450+
#endif
451451

452452
return return_value;
453453
}
@@ -468,11 +468,11 @@ inline int fflush(FILE *stream)
468468
int return_value=__VERIFIER_nondet_int();
469469
(void)stream;
470470

471-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
471+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
472472
if(stream)
473473
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
474474
"fflush file must be open");
475-
#endif
475+
#endif
476476

477477
return return_value;
478478
}
@@ -501,10 +501,10 @@ inline int fpurge(FILE *stream)
501501
#endif
502502
}
503503

504-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
504+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
505505
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
506506
"fpurge file must be open");
507-
#endif
507+
#endif
508508

509509
return return_value;
510510
}
@@ -537,10 +537,10 @@ inline int fgetc(FILE *stream)
537537

538538
__CPROVER_input("fgetc", return_value);
539539

540-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
540+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
541541
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
542542
"fgetc file must be open");
543-
#endif
543+
#endif
544544

545545
return return_value;
546546
}
@@ -568,10 +568,10 @@ inline int getc(FILE *stream)
568568
#endif
569569
}
570570

571-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
571+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
572572
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
573573
"getc file must be open");
574-
#endif
574+
#endif
575575

576576
// It's a byte or EOF, which we fix to -1.
577577
__CPROVER_assume(return_value>=-1 && return_value<=255);
@@ -623,10 +623,10 @@ inline int getw(FILE *stream)
623623
#endif
624624
}
625625

626-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
626+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
627627
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
628628
"getw file must be open");
629-
#endif
629+
#endif
630630

631631
__CPROVER_input("getw", return_value);
632632

@@ -648,18 +648,18 @@ inline int fseek(FILE *stream, long offset, int whence)
648648
__CPROVER_HIDE:;
649649
int return_value=__VERIFIER_nondet_int();
650650

651-
#if !defined(__linux__) || defined(__GLIBC__)
651+
#if !defined(__linux__) || defined(__GLIBC__)
652652
(void)*stream;
653-
#else
653+
#else
654654
(void)*(char*)stream;
655-
#endif
655+
#endif
656656
(void)offset;
657657
(void)whence;
658658

659-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
659+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
660660
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
661661
"fseek file must be open");
662-
#endif
662+
#endif
663663

664664
return return_value;
665665
}
@@ -678,16 +678,16 @@ inline long ftell(FILE *stream)
678678
__CPROVER_HIDE:;
679679
long return_value=__VERIFIER_nondet_long();
680680

681-
#if !defined(__linux__) || defined(__GLIBC__)
681+
#if !defined(__linux__) || defined(__GLIBC__)
682682
(void)*stream;
683-
#else
683+
#else
684684
(void)*(char*)stream;
685-
#endif
685+
#endif
686686

687-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
687+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
688688
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
689689
"ftell file must be open");
690-
#endif
690+
#endif
691691

692692
return return_value;
693693
}
@@ -701,18 +701,18 @@ inline long ftell(FILE *stream)
701701

702702
void rewind(FILE *stream)
703703
{
704-
__CPROVER_HIDE:
704+
__CPROVER_HIDE:
705705

706-
#if !defined(__linux__) || defined(__GLIBC__)
706+
#if !defined(__linux__) || defined(__GLIBC__)
707707
(void)*stream;
708-
#else
708+
#else
709709
(void)*(char*)stream;
710-
#endif
710+
#endif
711711

712-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
712+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
713713
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
714714
"rewind file must be open");
715-
#endif
715+
#endif
716716
}
717717

718718
/* FUNCTION: fwrite */
@@ -743,10 +743,10 @@ size_t fwrite(
743743
#endif
744744
}
745745

746-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
746+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
747747
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
748748
"fwrite file must be open");
749-
#endif
749+
#endif
750750

751751
size_t nwrite=__VERIFIER_nondet_size_t();
752752
__CPROVER_assume(nwrite<=nitems);
@@ -873,10 +873,10 @@ inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list a
873873
(void)*format;
874874
(void)arg;
875875

876-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
876+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
877877
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
878878
"vfscanf file must be open");
879-
#endif
879+
#endif
880880

881881
return result;
882882
}
@@ -977,10 +977,10 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg)
977977
(void)*format;
978978
(void)arg;
979979

980-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
980+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
981981
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
982982
"vfprintf file must be open");
983-
#endif
983+
#endif
984984

985985
return result;
986986
}

0 commit comments

Comments
 (0)