Skip to content

Commit c08e473

Browse files
kroeningkroening
authored
Merge pull request #8239 from tautschnig/features/snprintf
C library: implement {v,}snprintf
2 parents 25f5d3a + cd7459e commit c08e473

File tree

6 files changed

+240
-0
lines changed

6 files changed

+240
-0
lines changed

‎regression/cbmc-library/snprintf-01/main.c

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <assert.h>
2+
#include <stdio.h>
3+
4+
int main()
5+
{
6+
char result[10];
7+
int bytes = snprintf(result, 10, "%d\n", 42);
8+
assert(bytes <= 10);
9+
return 0;
10+
}

‎regression/cbmc-library/snprintf-01/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check --unwind 10 --no-unwinding-assertions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc-library/vsnprintf-01/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <assert.h>
2+
#include <stdarg.h>
3+
#include <stdio.h>
4+
5+
int xsnprintf(char *ptr, size_t size, const char *format, ...)
6+
{
7+
va_list list;
8+
va_start(list, format);
9+
int result = vsnprintf(ptr, size, format, list);
10+
va_end(list);
11+
return result;
12+
}
13+
14+
int main()
15+
{
16+
char result[10];
17+
int bytes = xsnprintf(result, 10, "%d\n", 42);
18+
assert(bytes <= 10);
19+
return 0;
20+
}

‎regression/cbmc-library/vsnprintf-01/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check --unwind 10 --no-unwinding-assertions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

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

+191
Original file line numberDiff line numberDiff line change
@@ -1606,6 +1606,154 @@ int vasprintf(char **ptr, const char *fmt, va_list ap)
16061606
return i;
16071607
}
16081608

1609+
/* FUNCTION: snprintf */
1610+
1611+
#ifndef __CPROVER_STDIO_H_INCLUDED
1612+
# include <stdio.h>
1613+
# define __CPROVER_STDIO_H_INCLUDED
1614+
#endif
1615+
1616+
#ifndef __CPROVER_STDARG_H_INCLUDED
1617+
# include <stdarg.h>
1618+
# define __CPROVER_STDARG_H_INCLUDED
1619+
#endif
1620+
1621+
#undef snprintf
1622+
1623+
int snprintf(char *str, size_t size, const char *fmt, ...)
1624+
{
1625+
va_list list;
1626+
va_start(list, fmt);
1627+
int result = vsnprintf(str, size, fmt, list);
1628+
va_end(list);
1629+
return result;
1630+
}
1631+
1632+
/* FUNCTION: __builtin___snprintf_chk */
1633+
1634+
#ifndef __CPROVER_STDIO_H_INCLUDED
1635+
# include <stdio.h>
1636+
# define __CPROVER_STDIO_H_INCLUDED
1637+
#endif
1638+
1639+
#ifndef __CPROVER_STDARG_H_INCLUDED
1640+
# include <stdarg.h>
1641+
# define __CPROVER_STDARG_H_INCLUDED
1642+
#endif
1643+
1644+
int __builtin___vsnprintf_chk(
1645+
char *str,
1646+
size_t size,
1647+
int flag,
1648+
size_t bufsize,
1649+
const char *fmt,
1650+
va_list ap);
1651+
1652+
int __builtin___snprintf_chk(
1653+
char *str,
1654+
size_t size,
1655+
int flag,
1656+
size_t bufsize,
1657+
const char *fmt,
1658+
...)
1659+
{
1660+
va_list list;
1661+
va_start(list, fmt);
1662+
int result = __builtin___vsnprintf_chk(str, size, flag, bufsize, fmt, list);
1663+
va_end(list);
1664+
return result;
1665+
}
1666+
1667+
/* FUNCTION: vsnprintf */
1668+
1669+
#ifndef __CPROVER_STDIO_H_INCLUDED
1670+
# include <stdio.h>
1671+
# define __CPROVER_STDIO_H_INCLUDED
1672+
#endif
1673+
1674+
#ifndef __CPROVER_STDARG_H_INCLUDED
1675+
# include <stdarg.h>
1676+
# define __CPROVER_STDARG_H_INCLUDED
1677+
#endif
1678+
1679+
#undef vsnprintf
1680+
1681+
char __VERIFIER_nondet_char(void);
1682+
1683+
int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
1684+
{
1685+
(void)*fmt;
1686+
1687+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
1688+
__CPROVER_OBJECT_SIZE(ap))
1689+
1690+
{
1691+
(void)va_arg(ap, int);
1692+
__CPROVER_precondition(
1693+
__CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
1694+
"vsnprintf object overlap");
1695+
}
1696+
1697+
size_t i = 0;
1698+
for(; i < size; ++i)
1699+
{
1700+
char c = __VERIFIER_nondet_char();
1701+
str[i] = c;
1702+
if(c == '\0')
1703+
break;
1704+
}
1705+
1706+
return i;
1707+
}
1708+
1709+
/* FUNCTION: __builtin___vsnprintf_chk */
1710+
1711+
#ifndef __CPROVER_STDIO_H_INCLUDED
1712+
# include <stdio.h>
1713+
# define __CPROVER_STDIO_H_INCLUDED
1714+
#endif
1715+
1716+
#ifndef __CPROVER_STDARG_H_INCLUDED
1717+
# include <stdarg.h>
1718+
# define __CPROVER_STDARG_H_INCLUDED
1719+
#endif
1720+
1721+
char __VERIFIER_nondet_char(void);
1722+
1723+
int __builtin___vsnprintf_chk(
1724+
char *str,
1725+
size_t size,
1726+
int flag,
1727+
size_t bufsize,
1728+
const char *fmt,
1729+
va_list ap)
1730+
{
1731+
(void)flag;
1732+
(void)bufsize;
1733+
(void)*fmt;
1734+
1735+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
1736+
__CPROVER_OBJECT_SIZE(ap))
1737+
1738+
{
1739+
(void)va_arg(ap, int);
1740+
__CPROVER_precondition(
1741+
__CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
1742+
"vsnprintf object overlap");
1743+
}
1744+
1745+
size_t i = 0;
1746+
for(; i < size; ++i)
1747+
{
1748+
char c = __VERIFIER_nondet_char();
1749+
str[i] = c;
1750+
if(c == '\0')
1751+
break;
1752+
}
1753+
1754+
return i;
1755+
}
1756+
16091757
/* FUNCTION: __acrt_iob_func */
16101758

16111759
#ifdef _WIN32
@@ -1667,6 +1815,49 @@ int __stdio_common_vfprintf(
16671815

16681816
#endif
16691817

1818+
/* FUNCTION: __stdio_common_vsprintf */
1819+
1820+
#ifdef _WIN32
1821+
1822+
# ifndef __CPROVER_STDIO_H_INCLUDED
1823+
# include <stdio.h>
1824+
# define __CPROVER_STDIO_H_INCLUDED
1825+
# endif
1826+
1827+
# ifndef __CPROVER_STDARG_H_INCLUDED
1828+
# include <stdarg.h>
1829+
# define __CPROVER_STDARG_H_INCLUDED
1830+
# endif
1831+
1832+
char __VERIFIER_nondet_char(void);
1833+
1834+
int __stdio_common_vsprintf(
1835+
unsigned __int64 options,
1836+
char *str,
1837+
size_t size,
1838+
char const *fmt,
1839+
_locale_t locale,
1840+
va_list args)
1841+
{
1842+
(void)options;
1843+
(void)*fmt;
1844+
(void)locale;
1845+
(void)args;
1846+
1847+
size_t i = 0;
1848+
for(; i < size; ++i)
1849+
{
1850+
char c = __VERIFIER_nondet_char();
1851+
str[i] = c;
1852+
if(c == '\0')
1853+
break;
1854+
}
1855+
1856+
return i;
1857+
}
1858+
1859+
#endif
1860+
16701861
/* FUNCTION: __srget */
16711862

16721863
#ifdef __FreeBSD__

‎src/ansi-c/library_check.sh

+3
Original file line numberDiff line numberDiff line change
@@ -38,12 +38,15 @@ perl -p -i -e 's/^_munmap\n//' __functions # mumap, macOS
3838
perl -p -i -e 's/^_pipe\n//' __functions # pipe, macOS
3939
perl -p -i -e 's/^_setjmp\n//' __functions # pipe, macOS
4040
perl -p -i -e 's/^_time(32|64)\n//' __functions # time, Windows
41+
perl -p -i -e 's/^__builtin___snprintf_chk\n//' __functions # snprintf, macOS
42+
perl -p -i -e 's/^__builtin___vsnprintf_chk\n//' __functions # vsnprintf, macOS
4143
perl -p -i -e 's/^__inet_(addr|aton|ntoa|network)\n//' __functions # inet_*, FreeBSD
4244
perl -p -i -e 's/^__isoc99_v?fscanf\n//' __functions # fscanf, Linux
4345
perl -p -i -e 's/^__isoc99_v?scanf\n//' __functions # scanf, Linux
4446
perl -p -i -e 's/^__isoc99_v?sscanf\n//' __functions # sscanf, Linux
4547
perl -p -i -e 's/^__sigsetjmp\n//' __functions # sigsetjmp, Linux
4648
perl -p -i -e 's/^__stdio_common_vfscanf\n//' __functions # fscanf, Windows
49+
perl -p -i -e 's/^__stdio_common_vsprintf\n//' __functions # snprintf, Windows
4750
perl -p -i -e 's/^__stdio_common_vsscanf\n//' __functions # sscanf, Windows
4851
perl -p -i -e 's/^__srget\n//' __functions # gets, FreeBSD
4952
perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD

0 commit comments

Comments
 (0)