Skip to content

Commit 08f211c

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 9ecf930 commit 08f211c

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
@@ -1644,3 +1644,51 @@ int __stdio_common_vfprintf(
16441644
}
16451645

16461646
#endif
1647+
1648+
/* FUNCTION: __srget */
1649+
1650+
#ifdef __FreeBSD__
1651+
1652+
# ifndef __CPROVER_STDIO_H_INCLUDED
1653+
# include <stdio.h>
1654+
# define __CPROVER_STDIO_H_INCLUDED
1655+
# endif
1656+
1657+
int __VERIFIER_nondet_int(void);
1658+
1659+
int __srget(FILE *stream)
1660+
{
1661+
(void)*stream;
1662+
1663+
// FreeBSD's implementation returns a character or EOF; __VERIFIER_nondet_int
1664+
// will capture all these options
1665+
return __VERIFIER_nondet_int();
1666+
}
1667+
1668+
#endif
1669+
1670+
/* FUNCTION: __swbuf */
1671+
1672+
#ifdef __FreeBSD__
1673+
1674+
# ifndef __CPROVER_STDIO_H_INCLUDED
1675+
# include <stdio.h>
1676+
# define __CPROVER_STDIO_H_INCLUDED
1677+
# endif
1678+
1679+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
1680+
1681+
int __swbuf(int c, FILE *stream)
1682+
{
1683+
(void)c;
1684+
(void)*stream;
1685+
1686+
// FreeBSD's implementation returns `c` or or EOF in case writing failed; we
1687+
// just non-deterministically choose between these
1688+
if(__VERIFIER_nondet___CPROVER_bool())
1689+
return EOF;
1690+
else
1691+
return c;
1692+
}
1693+
1694+
#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)