[value] using specification for function __e_acsl_memory_init
[value] using specification for function __e_acsl_store_block
[value] using specification for function __e_acsl_full_init
[value] using specification for function __e_acsl_mark_readonly
[value] using specification for function strcpy
[value] using specification for function mktemp
[value] using specification for function fork
tests/format/fprintf.c:17:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
tests/format/fprintf.c:15:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_fprintf
tests/format/signalled.h:12:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_printf
[value] using specification for function __e_acsl_delete_block
tests/format/fprintf.c:18:[value] warning: Completely invalid destination for assigns clause *stream. Ignoring.
tests/format/fprintf.c:27:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_dprintf
tests/format/fprintf.c:34:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_sprintf
tests/format/fprintf.c:41:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_snprintf