Commit 80771a89 authored by Virgile Prevosto's avatar Virgile Prevosto

[tests] fix E-ACSL oracles

parent ff91918b
/* run.config_dev
/*
run.config_dev
COMMENT: Check behaviours of format functions
DONTRUN:
*/
/*
run.config_ci
STDOPT: #"@PTEST_FILE@ -cpp-extra-args='-D__FC_ASSERT_FILE__=@PTEST_FILE@'"
*/
#include <stdlib.h>
#include <stdio.h>
......
[kernel:typing:implicit-function-declaration] tests/format/fprintf.c:16: Warning:
[kernel:typing:implicit-function-declaration] tests/format/fprintf.c:21: Warning:
Calling undeclared function fork. Old style K&R code?
[kernel:typing:incompatible-types-call] tests/format/fprintf.c:23: Warning:
[kernel:typing:incompatible-types-call] tests/format/fprintf.c:28: Warning:
expected 'FILE *' but got argument of type 'int *': & argc
[e-acsl] beginning translation.
[e-acsl] Warning: annotating undefined function `exit':
......@@ -39,71 +39,71 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/format/fprintf.c:16: Warning:
[kernel:annot:missing-spec] tests/format/fprintf.c:21: Warning:
Neither code nor specification for function fork, generating default assigns from the prototype
[kernel:annot:missing-spec] tests/format/fprintf.c:16: Warning:
[kernel:annot:missing-spec] tests/format/fprintf.c:21: 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:16: Warning:
[eva:alarm] tests/format/fprintf.c:21: Warning:
accessing uninitialized left-value. assert \initialized(&process_status);
[kernel:annot:missing-spec] tests/format/signalled.h:12: Warning:
[kernel:annot:missing-spec] tests/format/signalled.h:17: Warning:
Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
[eva:invalid-assigns] tests/format/fprintf.c:17:
[eva:invalid-assigns] tests/format/fprintf.c:22:
Completely invalid destination for assigns clause *stream. Ignoring.
[eva:alarm] tests/format/fprintf.c:17: Warning:
[eva:alarm] tests/format/fprintf.c:22: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_0);
[eva:alarm] tests/format/fprintf.c:20: Warning:
[eva:alarm] tests/format/fprintf.c:25: 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:22: Warning:
[eva:alarm] tests/format/fprintf.c:27: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_2);
[eva:invalid-assigns] tests/format/fprintf.c:23:
[eva:invalid-assigns] tests/format/fprintf.c:28:
Completely invalid destination for assigns clause *stream. Ignoring.
[eva:alarm] tests/format/fprintf.c:23: Warning:
[eva:alarm] tests/format/fprintf.c:28: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_3);
[kernel:annot:missing-spec] tests/format/fprintf.c:28: Warning:
[kernel:annot:missing-spec] tests/format/fprintf.c:33: Warning:
Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:28: Warning:
[eva:alarm] tests/format/fprintf.c:33: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_4);
[eva:alarm] tests/format/fprintf.c:29: Warning:
[eva:alarm] tests/format/fprintf.c:34: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_5);
[kernel:annot:missing-spec] tests/format/fprintf.c:35: Warning:
[kernel:annot:missing-spec] tests/format/fprintf.c:40: Warning:
Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:35: Warning:
[eva:alarm] tests/format/fprintf.c:40: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_6);
[eva:alarm] tests/format/fprintf.c:36: Warning:
[eva:alarm] tests/format/fprintf.c:41: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_7);
[eva:alarm] tests/format/fprintf.c:37: Warning:
[eva:alarm] tests/format/fprintf.c:42: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_8);
[eva:invalid-assigns] tests/format/fprintf.c:38:
[eva:invalid-assigns] tests/format/fprintf.c:43:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:38: Warning:
[eva:alarm] tests/format/fprintf.c:43: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_9);
[eva:invalid-assigns] tests/format/fprintf.c:39:
[eva:invalid-assigns] tests/format/fprintf.c:44:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:39: Warning:
[eva:alarm] tests/format/fprintf.c:44: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_10);
[kernel:annot:missing-spec] tests/format/fprintf.c:42: Warning:
[kernel:annot:missing-spec] tests/format/fprintf.c:47: Warning:
Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:42: Warning:
[eva:alarm] tests/format/fprintf.c:47: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_11);
[eva:alarm] tests/format/fprintf.c:43: Warning:
[eva:alarm] tests/format/fprintf.c:48: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_12);
[eva:invalid-assigns] tests/format/fprintf.c:44:
[eva:invalid-assigns] tests/format/fprintf.c:49:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:44: Warning:
[eva:alarm] tests/format/fprintf.c:49: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_13);
[eva:alarm] tests/format/fprintf.c:45: Warning:
[eva:alarm] tests/format/fprintf.c:50: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_14);
[eva:invalid-assigns] tests/format/fprintf.c:46:
[eva:invalid-assigns] tests/format/fprintf.c:51:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:46: Warning:
[eva:alarm] tests/format/fprintf.c:51: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_15);
[eva:invalid-assigns] tests/format/fprintf.c:47:
[eva:invalid-assigns] tests/format/fprintf.c:52:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:47: Warning:
[eva:alarm] tests/format/fprintf.c:52: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_16);
......@@ -47,94 +47,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:47";
__gen_e_acsl_literal_string_31 = "tests/format/fprintf.c:52";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_31,
sizeof("tests/format/fprintf.c:47"));
sizeof("tests/format/fprintf.c:52"));
__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:46";
__gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:51";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_30,
sizeof("tests/format/fprintf.c:46"));
sizeof("tests/format/fprintf.c:51"));
__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:45";
__gen_e_acsl_literal_string_29 = "tests/format/fprintf.c:50";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
sizeof("tests/format/fprintf.c:45"));
sizeof("tests/format/fprintf.c:50"));
__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:44";
__gen_e_acsl_literal_string_28 = "tests/format/fprintf.c:49";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
sizeof("tests/format/fprintf.c:44"));
sizeof("tests/format/fprintf.c:49"));
__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:43";
__gen_e_acsl_literal_string_27 = "tests/format/fprintf.c:48";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
sizeof("tests/format/fprintf.c:43"));
sizeof("tests/format/fprintf.c:48"));
__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:42";
__gen_e_acsl_literal_string_26 = "tests/format/fprintf.c:47";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
sizeof("tests/format/fprintf.c:42"));
sizeof("tests/format/fprintf.c:47"));
__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:39";
__gen_e_acsl_literal_string_25 = "tests/format/fprintf.c:44";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
sizeof("tests/format/fprintf.c:39"));
sizeof("tests/format/fprintf.c:44"));
__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:38";
__gen_e_acsl_literal_string_24 = "tests/format/fprintf.c:43";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
sizeof("tests/format/fprintf.c:38"));
sizeof("tests/format/fprintf.c:43"));
__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:37";
__gen_e_acsl_literal_string_23 = "tests/format/fprintf.c:42";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
sizeof("tests/format/fprintf.c:37"));
sizeof("tests/format/fprintf.c:42"));
__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:36";
__gen_e_acsl_literal_string_21 = "tests/format/fprintf.c:41";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
sizeof("tests/format/fprintf.c:36"));
sizeof("tests/format/fprintf.c:41"));
__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:35";
__gen_e_acsl_literal_string_19 = "tests/format/fprintf.c:40";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
sizeof("tests/format/fprintf.c:35"));
sizeof("tests/format/fprintf.c:40"));
__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:29";
__gen_e_acsl_literal_string_16 = "tests/format/fprintf.c:34";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
sizeof("tests/format/fprintf.c:29"));
sizeof("tests/format/fprintf.c:34"));
__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:28";
__gen_e_acsl_literal_string_15 = "tests/format/fprintf.c:33";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
sizeof("tests/format/fprintf.c:28"));
sizeof("tests/format/fprintf.c:33"));
__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:23";
__gen_e_acsl_literal_string_14 = "tests/format/fprintf.c:28";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
sizeof("tests/format/fprintf.c:23"));
sizeof("tests/format/fprintf.c:28"));
__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:22";
__gen_e_acsl_literal_string_13 = "tests/format/fprintf.c:27";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
sizeof("tests/format/fprintf.c:22"));
sizeof("tests/format/fprintf.c:27"));
__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:20";
__gen_e_acsl_literal_string_12 = "tests/format/fprintf.c:25";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
sizeof("tests/format/fprintf.c:20"));
sizeof("tests/format/fprintf.c:25"));
__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:17";
__gen_e_acsl_literal_string_9 = "tests/format/fprintf.c:22";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
sizeof("tests/format/fprintf.c:17"));
sizeof("tests/format/fprintf.c:22"));
__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:16";
__gen_e_acsl_literal_string_8 = "tests/format/fprintf.c:21";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
sizeof("tests/format/fprintf.c:16"));
sizeof("tests/format/fprintf.c:21"));
__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";
......
......@@ -4,7 +4,12 @@
#define STRINGIFY(x) #x
#define TOSTRING(x) STRINGIFY(x)
#define AT __FILE__ ":" TOSTRING(__LINE__)
#ifdef __FC_ASSERT_FILE__
#define __EACSL_FILENAME__ TOSTRING(__FC_ASSERT_FILE__)
#else
#define __EACSL_FILENAME__ __FILE__
#endif
#define AT __EACSL_FILENAME__ ":" TOSTRING(__LINE__)
int testno = 0;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment