Skip to content

Commit

Permalink
C library: add FreeBSD's __srget, __swbuf
Browse files Browse the repository at this point in the history
Implemented as over-approximations of the implementations found at
https://cgit.freebsd.org/src/tree/lib/libc/stdio/.
  • Loading branch information
tautschnig committed Nov 20, 2023
1 parent fc75fe4 commit ffadcd4
Show file tree
Hide file tree
Showing 2 changed files with 50 additions and 0 deletions.
48 changes: 48 additions & 0 deletions src/ansi-c/library/stdio.c
Original file line number Diff line number Diff line change
Expand Up @@ -1749,3 +1749,51 @@ int __stdio_common_vfprintf(
}

#endif

/* FUNCTION: __srget */

#ifdef __FreeBSD__

# ifndef __CPROVER_STDIO_H_INCLUDED
# include <stdio.h>
# define __CPROVER_STDIO_H_INCLUDED
# endif

int __VERIFIER_nondet_int(void);

int __srget(FILE *stream)
{
(void)*stream;

// FreeBSD's implementation returns a character or EOF; __VERIFIER_nondet_int
// will capture all these options
return __VERIFIER_nondet_int();
}

#endif

/* FUNCTION: __swbuf */

#ifdef __FreeBSD__

# ifndef __CPROVER_STDIO_H_INCLUDED
# include <stdio.h>
# define __CPROVER_STDIO_H_INCLUDED
# endif

__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);

int __swbuf(int c, FILE *stream)
{
(void)c;
(void)*stream;

// FreeBSD's implementation returns `c` or or EOF in case writing failed; we
// just non-deterministically choose between these
if(__VERIFIER_nondet___CPROVER_bool())
return EOF;
else
return c;
}

#endif
2 changes: 2 additions & 0 deletions src/ansi-c/library_check.sh
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,8 @@ perl -p -i -e 's/^__isoc99_v?sscanf\n//' __functions # sscanf, Linux
perl -p -i -e 's/^__sigsetjmp\n//' __functions # sigsetjmp, Linux
perl -p -i -e 's/^__stdio_common_vfscanf\n//' __functions # fscanf, Windows
perl -p -i -e 's/^__stdio_common_vsscanf\n//' __functions # sscanf, Windows
perl -p -i -e 's/^__srget\n//' __functions # gets, FreeBSD
perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD

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

0 comments on commit ffadcd4

Please sign in to comment.