Commit 4788bc52 authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'bugfix/basile/eacsl-103-reactivate-tests' into 'master'

[eacsl:tests] Reactivate and fix dev tests

See merge request frama-c/frama-c!2633
parents 0ad5c75a 304c5013
......@@ -179,7 +179,7 @@ static abbrev_t size2abbri(int size, int sign) {
return sign ? ILong : IULong;
else if (size == sizeof(long long int))
return sign ? ILongLong : IULongLong;
vabort(INT_ERROR "integral type corresponding to size %d unknown", size);
vabort(INT_ERROR "integral type corresponding to size %d unknown\n", size);
return '\0';
}
......@@ -192,7 +192,7 @@ static abbrev_t size2abbrf(int size) {
else if (size == sizeof(long double))
return FLongDouble;
vabort
(INT_ERROR "floating point type corresponding to size %d unknown", size);
(INT_ERROR "floating point type corresponding to size %d unknown\n", size);
return '\0';
}
......@@ -370,7 +370,7 @@ static char *fetch_format_flags(char *fmt, format_directive *dir) {
if (!dir->flags._f) \
{ dir->flags._f = 1; } \
else \
{ vabort(FMT_ERROR "flag %s has already been set", #_f); }
{ vabort(FMT_ERROR "flag %s has already been set\n", #_f); }
while (is_flag_char(*fmt)) {
dir->flags.specified = 1;
......@@ -590,7 +590,7 @@ static void release_directives(const char *fmt, format_directive ** dirs) {
/* Format string validation (well-formedness) {{{ */
static inline void validate_application(format_directive *dir, char *allowed,
char* kind, char *desc) {
vassert(strchr(allowed, dir->specifier) != '\0', FMT_ERROR
vassert(strchr(allowed, dir->specifier) != NULL, FMT_ERROR
"wrong application of %s [%s] to format specifier [%c]\n",
desc, kind, dir->specifier);
}
......@@ -605,7 +605,7 @@ static void validate_applications(format_directive *dir) {
i, d, u, f, F, g, or G conversion specifiers. For other specifiers
its behaviour is undefined. */
if (dir->flags.apostroph)
validate_application(dir, "idufFgG", "\\", desc);
validate_application(dir, "idufFgG", "'", desc);
/* # flag converts a value to an alternative form. It is applicable only to
x, X, a, A, e, E, f, F, g, and G conversion specifiers. */
......@@ -619,7 +619,7 @@ static void validate_applications(format_directive *dir) {
/* No flags should be used if 'n' specifier is given */
if (dir->flags.specified && dir->specifier == 'n')
vabort(FMT_ERROR "one of more flags with [n] specifier", NULL);
vabort(FMT_ERROR "one of more flags with [n] specifier\n", NULL);
/* ==== Precision ==== */
desc = "precision";
......@@ -637,7 +637,7 @@ static void validate_applications(format_directive *dir) {
desc = "field width";
if (dir->specifier == 'n' && dir->field_width != INT_MIN)
vabort(FMT_ERROR "field width used with [n] specifier", NULL);
vabort(FMT_ERROR "field width used with [n] specifier\n", NULL);
/* ==== Length modifiers ==== */
desc = "length modifier";
......@@ -1006,7 +1006,7 @@ int builtin_snprintf(const char *fmtdesc, char *buffer, size_t size,
characters to write, it does not matter */
if (size > 0 && !writeable((uintptr_t)buffer, size, (uintptr_t)buffer))
vabort("sprintf: output buffer is unallocated or has insufficient length "
"to store %d characters and \0 terminator or not writeable\n", size);
"to store %d characters and \\0 terminator or not writeable\n", size);
va_start(ap, fmt);
return vsnprintf(buffer, size, fmt, ap);
}
......
/*
run.config_dev
/* run.config_ci,run.config_dev
COMMENT: Check behaviours of format functions
DONTRUN:
*/
#include <stdlib.h>
......@@ -21,7 +19,7 @@ int main(int argc, const char **argv) {
OK(fprintf(fh, "foobar %s\n", "foobar"));
fclose(fh);
ABRT(fprintf(fh, "foobar %s\n", "foobar"));
ABRT(fprintf(&argc, "foobar %s\n", "foobar"));
ABRT(fprintf((FILE*)&argc, "foobar %s\n", "foobar"));
}
/* *** dprintf *** */
......
[kernel:typing:implicit-function-declaration] tests/format/fprintf.c:17: Warning:
Calling undeclared function fork. Old style K&R code?
[kernel:typing:incompatible-types-call] tests/format/fprintf.c:24: Warning:
expected 'FILE *' but got argument of type 'int *': & argc
[e-acsl] beginning translation.
[e-acsl] Warning: annotating undefined function `exit':
the generated program may miss memory instrumentation
......@@ -15,6 +11,12 @@
[e-acsl] Warning: annotating undefined function `waitpid':
the generated program may miss memory instrumentation
if there are memory-related annotations.
[e-acsl] Warning: annotating undefined function `fork':
the generated program may miss memory instrumentation
if there are memory-related annotations.
[e-acsl] tests/format/fprintf.c:10: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
......@@ -39,71 +41,71 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/format/fprintf.c:17: Warning:
Neither code nor specification for function fork, generating default assigns from the prototype
[kernel:annot:missing-spec] tests/format/fprintf.c:17: Warning:
[eva:alarm] FRAMAC_SHARE/libc/unistd.h:857: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/unistd.h:857: Warning:
function __gen_e_acsl_fork: postcondition 'result_ok_child_or_error' got status unknown.
[kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning:
Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown.
[eva:alarm] tests/format/fprintf.c:17: Warning:
[eva:alarm] tests/format/fprintf.c:15: Warning:
accessing uninitialized left-value. assert \initialized(&process_status);
[kernel:annot:missing-spec] tests/format/signalled.h:15: Warning:
Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
[eva:invalid-assigns] tests/format/fprintf.c:18:
[eva:invalid-assigns] tests/format/fprintf.c:16:
Completely invalid destination for assigns clause *stream. Ignoring.
[eva:alarm] tests/format/fprintf.c:18: Warning:
[eva:alarm] tests/format/fprintf.c:16: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_0);
[eva:alarm] tests/format/fprintf.c:21: Warning:
[eva:alarm] tests/format/fprintf.c:19: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_1);
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/format/fprintf.c:23: Warning:
[eva:alarm] tests/format/fprintf.c:21: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_2);
[eva:invalid-assigns] tests/format/fprintf.c:24:
[eva:invalid-assigns] tests/format/fprintf.c:22:
Completely invalid destination for assigns clause *stream. Ignoring.
[eva:alarm] tests/format/fprintf.c:24: Warning:
[eva:alarm] tests/format/fprintf.c:22: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_3);
[kernel:annot:missing-spec] tests/format/fprintf.c:29: Warning:
[kernel:annot:missing-spec] tests/format/fprintf.c:27: Warning:
Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:29: Warning:
[eva:alarm] tests/format/fprintf.c:27: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_4);
[eva:alarm] tests/format/fprintf.c:30: Warning:
[eva:alarm] tests/format/fprintf.c:28: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_5);
[kernel:annot:missing-spec] tests/format/fprintf.c:36: Warning:
[kernel:annot:missing-spec] tests/format/fprintf.c:34: Warning:
Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:36: Warning:
[eva:alarm] tests/format/fprintf.c:34: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_6);
[eva:alarm] tests/format/fprintf.c:37: Warning:
[eva:alarm] tests/format/fprintf.c:35: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_7);
[eva:alarm] tests/format/fprintf.c:38: Warning:
[eva:alarm] tests/format/fprintf.c:36: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_8);
[eva:invalid-assigns] tests/format/fprintf.c:39:
[eva:invalid-assigns] tests/format/fprintf.c:37:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:39: Warning:
[eva:alarm] tests/format/fprintf.c:37: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_9);
[eva:invalid-assigns] tests/format/fprintf.c:40:
[eva:invalid-assigns] tests/format/fprintf.c:38:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:40: Warning:
[eva:alarm] tests/format/fprintf.c:38: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_10);
[kernel:annot:missing-spec] tests/format/fprintf.c:43: Warning:
[kernel:annot:missing-spec] tests/format/fprintf.c:41: Warning:
Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:43: Warning:
[eva:alarm] tests/format/fprintf.c:41: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_11);
[eva:alarm] tests/format/fprintf.c:44: Warning:
[eva:alarm] tests/format/fprintf.c:42: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_12);
[eva:invalid-assigns] tests/format/fprintf.c:45:
[eva:invalid-assigns] tests/format/fprintf.c:43:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:45: Warning:
[eva:alarm] tests/format/fprintf.c:43: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_13);
[eva:alarm] tests/format/fprintf.c:46: Warning:
[eva:alarm] tests/format/fprintf.c:44: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_14);
[eva:invalid-assigns] tests/format/fprintf.c:47:
[eva:invalid-assigns] tests/format/fprintf.c:45:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:47: Warning:
[eva:alarm] tests/format/fprintf.c:45: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_15);
[eva:invalid-assigns] tests/format/fprintf.c:48:
[eva:invalid-assigns] tests/format/fprintf.c:46:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:48: Warning:
[eva:alarm] tests/format/fprintf.c:46: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_16);
......@@ -4,7 +4,9 @@
#include "stdlib.h"
#include "sys/select.h"
#include "sys/time.h"
#include "sys/types.h"
#include "sys/wait.h"
#include "unistd.h"
char *__gen_e_acsl_literal_string_31;
char *__gen_e_acsl_literal_string_30;
char *__gen_e_acsl_literal_string_29;
......@@ -80,9 +82,37 @@ int __gen_e_acsl_fclose(FILE *stream);
*/
pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options);
/*@ assigns \result;
assigns \result \from \nothing; */
extern int ( /* missing proto */ fork)(void);
/*@ ensures
result_ok_child_or_error:
\result ≡ 0 ∨ \result > 0 ∨ \result ≡ -1;
assigns \result;
assigns \result \from \nothing;
*/
pid_t __gen_e_acsl_fork(void);
/*@ ensures
result_ok_child_or_error:
\result ≡ 0 ∨ \result > 0 ∨ \result ≡ -1;
assigns \result;
assigns \result \from \nothing;
*/
pid_t __gen_e_acsl_fork(void)
{
pid_t __retres;
__retres = fork();
{
int __gen_e_acsl_or;
int __gen_e_acsl_or_2;
if (__retres == 0) __gen_e_acsl_or = 1;
else __gen_e_acsl_or = __retres > 0;
if (__gen_e_acsl_or) __gen_e_acsl_or_2 = 1;
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,"Postcondition","fork",
"\\result == 0 || \\result > 0 || \\result == -1",
"FRAMAC_SHARE/libc/unistd.h",857);
return __retres;
}
}
/*@ ensures result_ok_or_error: \result ≡ -1 ∨ \result ≥ 0;
ensures
......@@ -213,94 +243,94 @@ void __e_acsl_globals_init(void)
static char __e_acsl_already_run = 0;
if (! __e_acsl_already_run) {
__e_acsl_already_run = 1;
__gen_e_acsl_literal_string_31 = "tests/format/fprintf.c:48";
__gen_e_acsl_literal_string_31 = "tests/format/fprintf.c:46";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_31,
sizeof("tests/format/fprintf.c:48"));
sizeof("tests/format/fprintf.c:46"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_31);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_31);
__gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:47";
__gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:45";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_30,
sizeof("tests/format/fprintf.c:47"));
sizeof("tests/format/fprintf.c:45"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_30);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_30);
__gen_e_acsl_literal_string_29 = "tests/format/fprintf.c:46";
__gen_e_acsl_literal_string_29 = "tests/format/fprintf.c:44";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
sizeof("tests/format/fprintf.c:46"));
sizeof("tests/format/fprintf.c:44"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
__gen_e_acsl_literal_string_28 = "tests/format/fprintf.c:45";
__gen_e_acsl_literal_string_28 = "tests/format/fprintf.c:43";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
sizeof("tests/format/fprintf.c:45"));
sizeof("tests/format/fprintf.c:43"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_28);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_28);
__gen_e_acsl_literal_string_27 = "tests/format/fprintf.c:44";
__gen_e_acsl_literal_string_27 = "tests/format/fprintf.c:42";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
sizeof("tests/format/fprintf.c:44"));
sizeof("tests/format/fprintf.c:42"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_27);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_27);
__gen_e_acsl_literal_string_26 = "tests/format/fprintf.c:43";
__gen_e_acsl_literal_string_26 = "tests/format/fprintf.c:41";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
sizeof("tests/format/fprintf.c:43"));
sizeof("tests/format/fprintf.c:41"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_26);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_26);
__gen_e_acsl_literal_string_25 = "tests/format/fprintf.c:40";
__gen_e_acsl_literal_string_25 = "tests/format/fprintf.c:38";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
sizeof("tests/format/fprintf.c:40"));
sizeof("tests/format/fprintf.c:38"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_25);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_25);
__gen_e_acsl_literal_string_24 = "tests/format/fprintf.c:39";
__gen_e_acsl_literal_string_24 = "tests/format/fprintf.c:37";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
sizeof("tests/format/fprintf.c:39"));
sizeof("tests/format/fprintf.c:37"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
__gen_e_acsl_literal_string_23 = "tests/format/fprintf.c:38";
__gen_e_acsl_literal_string_23 = "tests/format/fprintf.c:36";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
sizeof("tests/format/fprintf.c:38"));
sizeof("tests/format/fprintf.c:36"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
__gen_e_acsl_literal_string_21 = "tests/format/fprintf.c:37";
__gen_e_acsl_literal_string_21 = "tests/format/fprintf.c:35";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
sizeof("tests/format/fprintf.c:37"));
sizeof("tests/format/fprintf.c:35"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
__gen_e_acsl_literal_string_19 = "tests/format/fprintf.c:36";
__gen_e_acsl_literal_string_19 = "tests/format/fprintf.c:34";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
sizeof("tests/format/fprintf.c:36"));
sizeof("tests/format/fprintf.c:34"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
__gen_e_acsl_literal_string_16 = "tests/format/fprintf.c:30";
__gen_e_acsl_literal_string_16 = "tests/format/fprintf.c:28";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
sizeof("tests/format/fprintf.c:30"));
sizeof("tests/format/fprintf.c:28"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
__gen_e_acsl_literal_string_15 = "tests/format/fprintf.c:29";
__gen_e_acsl_literal_string_15 = "tests/format/fprintf.c:27";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
sizeof("tests/format/fprintf.c:29"));
sizeof("tests/format/fprintf.c:27"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
__gen_e_acsl_literal_string_14 = "tests/format/fprintf.c:24";
__gen_e_acsl_literal_string_14 = "tests/format/fprintf.c:22";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
sizeof("tests/format/fprintf.c:24"));
sizeof("tests/format/fprintf.c:22"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
__gen_e_acsl_literal_string_13 = "tests/format/fprintf.c:23";
__gen_e_acsl_literal_string_13 = "tests/format/fprintf.c:21";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
sizeof("tests/format/fprintf.c:23"));
sizeof("tests/format/fprintf.c:21"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
__gen_e_acsl_literal_string_12 = "tests/format/fprintf.c:21";
__gen_e_acsl_literal_string_12 = "tests/format/fprintf.c:19";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
sizeof("tests/format/fprintf.c:21"));
sizeof("tests/format/fprintf.c:19"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
__gen_e_acsl_literal_string_9 = "tests/format/fprintf.c:18";
__gen_e_acsl_literal_string_9 = "tests/format/fprintf.c:16";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
sizeof("tests/format/fprintf.c:18"));
sizeof("tests/format/fprintf.c:16"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
__gen_e_acsl_literal_string_8 = "tests/format/fprintf.c:17";
__gen_e_acsl_literal_string_8 = "tests/format/fprintf.c:15";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
sizeof("tests/format/fprintf.c:17"));
sizeof("tests/format/fprintf.c:15"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
__gen_e_acsl_literal_string_11 = "foobar %s\n";
......@@ -379,7 +409,7 @@ int main(int argc, char const **argv)
__e_acsl_globals_init();
char *pstr = (char *)__gen_e_acsl_literal_string_6;
{
pid_t pid = fork();
pid_t pid = __gen_e_acsl_fork();
if (! pid) {
__e_acsl_builtin_fprintf("",stdout,__gen_e_acsl_literal_string_7);
__gen_e_acsl_exit(0);
......@@ -394,7 +424,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_0 = fork();
pid_t pid_0 = __gen_e_acsl_fork();
if (! pid_0) {
__e_acsl_builtin_fprintf("",(FILE *)0,__gen_e_acsl_literal_string_7);
__gen_e_acsl_exit(0);
......@@ -413,7 +443,7 @@ int main(int argc, char const **argv)
__e_acsl_full_init((void *)(& fh));
if (fh) {
{
pid_t pid_1 = fork();
pid_t pid_1 = __gen_e_acsl_fork();
if (! pid_1) {
__e_acsl_builtin_fprintf("s",fh,__gen_e_acsl_literal_string_11,
__gen_e_acsl_literal_string_10);
......@@ -430,7 +460,7 @@ int main(int argc, char const **argv)
}
__gen_e_acsl_fclose(fh);
{
pid_t pid_2 = fork();
pid_t pid_2 = __gen_e_acsl_fork();
if (! pid_2) {
__e_acsl_builtin_fprintf("s",fh,__gen_e_acsl_literal_string_11,
__gen_e_acsl_literal_string_10);
......@@ -446,7 +476,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_3 = fork();
pid_t pid_3 = __gen_e_acsl_fork();
if (! pid_3) {
__e_acsl_builtin_fprintf("s",(FILE *)(& argc),
__gen_e_acsl_literal_string_11,
......@@ -464,7 +494,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_4 = fork();
pid_t pid_4 = __gen_e_acsl_fork();
if (! pid_4) {
__e_acsl_builtin_dprintf("",1,__gen_e_acsl_literal_string_7);
__gen_e_acsl_exit(0);
......@@ -479,7 +509,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_5 = fork();
pid_t pid_5 = __gen_e_acsl_fork();
if (! pid_5) {
__e_acsl_builtin_dprintf("",3,__gen_e_acsl_literal_string_7);
__gen_e_acsl_exit(0);
......@@ -494,7 +524,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_6 = fork();
pid_t pid_6 = __gen_e_acsl_fork();
if (! pid_6) {
__e_acsl_builtin_sprintf("s",buf,__gen_e_acsl_literal_string_18,
__gen_e_acsl_literal_string_17);
......@@ -510,7 +540,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_7 = fork();
pid_t pid_7 = __gen_e_acsl_fork();
if (! pid_7) {
__e_acsl_builtin_sprintf("s",buf,__gen_e_acsl_literal_string_18,
__gen_e_acsl_literal_string_20);
......@@ -526,7 +556,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_8 = fork();
pid_t pid_8 = __gen_e_acsl_fork();
if (! pid_8) {
__e_acsl_builtin_sprintf("s",buf,__gen_e_acsl_literal_string_18,
__gen_e_acsl_literal_string_22);
......@@ -542,7 +572,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_9 = fork();
pid_t pid_9 = __gen_e_acsl_fork();
if (! pid_9) {
__e_acsl_builtin_sprintf("s",(char *)0,__gen_e_acsl_literal_string_18,
__gen_e_acsl_literal_string_22);
......@@ -558,7 +588,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_10 = fork();
pid_t pid_10 = __gen_e_acsl_fork();
if (! pid_10) {
__e_acsl_builtin_sprintf("s",pstr,__gen_e_acsl_literal_string_18,
__gen_e_acsl_literal_string_22);
......@@ -574,7 +604,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_11 = fork();
pid_t pid_11 = __gen_e_acsl_fork();
if (! pid_11) {
__e_acsl_builtin_snprintf("s",buf,(unsigned long)4,
__gen_e_acsl_literal_string_18,
......@@ -591,7 +621,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_12 = fork();
pid_t pid_12 = __gen_e_acsl_fork();
if (! pid_12) {
__e_acsl_builtin_snprintf("s",buf,(unsigned long)5,
__gen_e_acsl_literal_string_18,
......@@ -608,7 +638,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_13 = fork();
pid_t pid_13 = __gen_e_acsl_fork();
if (! pid_13) {
__e_acsl_builtin_snprintf("s",pstr,(unsigned long)6,
__gen_e_acsl_literal_string_18,
......@@ -625,7 +655,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_14 = fork();
pid_t pid_14 = __gen_e_acsl_fork();
if (! pid_14) {
__e_acsl_builtin_snprintf("s",buf,(unsigned long)6,
__gen_e_acsl_literal_string_18,
......@@ -642,7 +672,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_15 = fork();
pid_t pid_15 = __gen_e_acsl_fork();
if (! pid_15) {
__e_acsl_builtin_snprintf("s",(char *)0,(unsigned long)6,
__gen_e_acsl_literal_string_18,
......@@ -659,7 +689,7 @@ int main(int argc, char const **argv)
}
}
{
pid_t pid_16 = fork();
pid_t pid_16 = __gen_e_acsl_fork();
if (! pid_16) {
__e_acsl_builtin_snprintf("s",(char *)0,(unsigned long)0,
__gen_e_acsl_literal_string_18,
......
TEST 1: OK: Expected execution at tests/format/fprintf.c:15
fprintf: attempt to write to an invalid stream
TEST 2: OK: Expected signal at tests/format/fprintf.c:16
TEST 3: OK: Expected execution at tests/format/fprintf.c:19
fprintf: attempt to write to an invalid stream
TEST 4: OK: Expected signal at tests/format/fprintf.c:21
fprintf: attempt to write to an invalid stream
TEST 5: OK: Expected signal at tests/format/fprintf.c:22
TEST 6: OK: Expected execution at tests/format/fprintf.c:27
dprintf: attempt to write to a closed file descriptor 3
TEST 7: OK: Expected signal at tests/format/fprintf.c:28
TEST 8: OK: Expected execution at tests/format/fprintf.c:34
TEST 9: OK: Expected execution at tests/format/fprintf.c:35
sprintf: output buffer is unallocated or has insufficient length to store 6 characters or not writeable
TEST 10: OK: Expected signal at tests/format/fprintf.c:36
sprintf: output buffer is unallocated or has insufficient length to store 6 characters or not writeable
TEST 11: OK: Expected signal at tests/format/fprintf.c:37
sprintf: output buffer is unallocated or has insufficient length to store 6 characters or not writeable
TEST 12: OK: Expected signal at tests/format/fprintf.c:38
TEST 13: OK: Expected execution at tests/format/fprintf.c:41
TEST 14: OK: Expected execution at tests/format/fprintf.c:42
sprintf: output buffer is unallocated or has insufficient length to store 6 characters and \0 terminator or not writeable
TEST 15: OK: Expected signal at tests/format/fprintf.c:43
sprintf: output buffer is unallocated or has insufficient length to store 6 characters and \0 terminator or not writeable
TEST 16: OK: Expected signal at tests/format/fprintf.c:44
sprintf: output buffer is unallocated or has insufficient length to store 6 characters and \0 terminator or not writeable
TEST 17: OK: Expected signal at tests/format/fprintf.c:45
TEST 18: OK: Expected execution at tests/format/fprintf.c:46
[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
[kernel] Parsing tests/format/fprintf.c (with preprocessing)
gcc: error: ./tests/print.cmxs.startup.o: No such file or directory
gcc: error: ./tests/print.o: No such file or directory
gcc: fatal error: no input files
compilation terminated.
File "caml_startup", line 1:
Error: Error during linking
[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
De