Skip to content

Commit 0de2cb1

Browse files
committed
C library: add FreeBSD's __srget, __swbuf
Implemented as over-approximations of the implementations found at https://cgit.freebsd.org/src/tree/lib/libc/stdio/.
1 parent c939d00 commit 0de2cb1

File tree

2 files changed

+50
-0
lines changed

2 files changed

+50
-0
lines changed

Diff for: src/ansi-c/library/stdio.c

+48
Original file line numberDiff line numberDiff line change
@@ -1749,3 +1749,51 @@ int __stdio_common_vfprintf(
17491749
}
17501750

17511751
#endif
1752+
1753+
/* FUNCTION: __srget */
1754+
1755+
#ifdef __FreeBSD__
1756+
1757+
# ifndef __CPROVER_STDIO_H_INCLUDED
1758+
# include <stdio.h>
1759+
# define __CPROVER_STDIO_H_INCLUDED
1760+
# endif
1761+
1762+
int __VERIFIER_nondet_int(void);
1763+
1764+
int __srget(FILE *stream)
1765+
{
1766+
(void)*stream;
1767+
1768+
// FreeBSD's implementation returns a character or EOF; __VERIFIER_nondet_int
1769+
// will capture all these options
1770+
return __VERIFIER_nondet_int();
1771+
}
1772+
1773+
#endif
1774+
1775+
/* FUNCTION: __swbuf */
1776+
1777+
#ifdef __FreeBSD__
1778+
1779+
# ifndef __CPROVER_STDIO_H_INCLUDED
1780+
# include <stdio.h>
1781+
# define __CPROVER_STDIO_H_INCLUDED
1782+
# endif
1783+
1784+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
1785+
1786+
int __swbuf(int c, FILE *stream)
1787+
{
1788+
(void)c;
1789+
(void)*stream;
1790+
1791+
// FreeBSD's implementation returns `c` or or EOF in case writing failed; we
1792+
// just non-deterministically choose between these
1793+
if(__VERIFIER_nondet___CPROVER_bool())
1794+
return EOF;
1795+
else
1796+
return c;
1797+
}
1798+
1799+
#endif

Diff for: src/ansi-c/library_check.sh

+2
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,8 @@ perl -p -i -e 's/^__isoc99_v?sscanf\n//' __functions # sscanf, Linux
4545
perl -p -i -e 's/^__sigsetjmp\n//' __functions # sigsetjmp, Linux
4646
perl -p -i -e 's/^__stdio_common_vfscanf\n//' __functions # fscanf, Windows
4747
perl -p -i -e 's/^__stdio_common_vsscanf\n//' __functions # sscanf, Windows
48+
perl -p -i -e 's/^__srget\n//' __functions # gets, FreeBSD
49+
perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD
4850

4951
# Some functions are covered by existing tests:
5052
perl -p -i -e 's/^__CPROVER_deallocate\n//' __functions # free-01

0 commit comments

Comments
 (0)