Commit 304c5013 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl:tests] Reactivate `format` tests

parent 50e5a397
/*
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
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: compilation of './tests/print.ml' failed
[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/printf.c (with preprocessing)
[kernel:parser:decimal-float] tests/format/printf.c:89: Warning:
Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[variadic] tests/format/printf.c:29: Warning:
Call to function printf with non-static format argument:
no specification will be generated.
[variadic] tests/format/printf.c:31: Warning:
Call to function printf with non-static format argument:
no specification will be generated.
[variadic] tests/format/printf.c:33: Warning:
Call to function printf with non-static format argument:
no specification will be generated.
[variadic] tests/format/printf.c:35: Warning:
Call to function printf with non-static format argument:
no specification will be generated.
[variadic] tests/format/printf.c:37: Warning:
Call to function printf with non-static format argument:
no specification will be generated.
[variadic] tests/format/printf.c:39: Warning:
Call to function printf with non-static format argument:
no specification will be generated.
[variadic] tests/format/printf.c:186: Warning:
Not enough arguments: expected 5, given 4.
[variadic] tests/format/printf.c:189: Warning:
Too many arguments: expected 5, given 6. Superfluous arguments will be removed.
[variadic] tests/format/printf.c:194: Warning:
Call to function printf with non-static format argument:
no specification will be generated.
[variadic] tests/format/printf.c:197: Warning: Unknown conversion specifier $.
[variadic] tests/format/printf.c:199: Warning: Unknown conversion specifier $.
[variadic] tests/format/printf.c:201: Warning: Unknown conversion specifier $.
[variadic] tests/format/printf.c:204: Warning: Unknown conversion specifier $.
[variadic] tests/format/printf.c:206: Warning: Unknown conversion specifier $.
[variadic] tests/format/printf.c:226: Warning: Unknown conversion specifier l.
[variadic] tests/format/printf.c:257: Warning:
Incorrect type for argument 2. The argument will be cast from wint_t to intmax_t.
[variadic] tests/format/printf.c:279: Warning:
Incorrect type for argument 2. The argument will be cast from int to size_t.
[variadic] tests/format/printf.c:279: Warning:
Incorrect type for argument 2. The argument will be cast from int to size_t.
[variadic] tests/format/printf.c:292: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
[variadic] tests/format/printf.c:292: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
[variadic] tests/format/printf.c:293: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
[variadic] tests/format/printf.c:293: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
[variadic] tests/format/printf.c:307: Warning: Unknown conversion specifier C.
[variadic] tests/format/printf.c:308: Warning: Unknown conversion specifier S.
[variadic] tests/format/printf.c:309: Warning: Unknown conversion specifier m.
[variadic] tests/format/printf.c:315: Warning:
Incorrect type for argument 2. The argument will be cast from long to int.
[variadic] tests/format/printf.c:315: Warning:
Incorrect type for argument 2. The argument will be cast from long to int.
[variadic] tests/format/printf.c:316: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned int to int.
[variadic] tests/format/printf.c:316: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned int to int.
[variadic] tests/format/printf.c:317: Warning:
Incorrect type for argument 2. The argument will be cast from void * to int.
[variadic] tests/format/printf.c:317: Warning:
Incorrect type for argument 2. The argument will be cast from void * to int.
[variadic] tests/format/printf.c:318: Warning:
Incorrect type for argument 2. The argument will be cast from double to int.
[variadic] tests/format/printf.c:318: Warning: