From 80771a8971de464e1736395028ca3639746116b9 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 6 Jan 2020 17:37:44 +0100
Subject: [PATCH] [tests] fix E-ACSL oracles
---
src/plugins/e-acsl/tests/format/fprintf.c | 7 +-
.../tests/format/oracle_ci/fprintf.res.oracle | 66 ++++++++---------
.../tests/format/oracle_ci/gen_fprintf.c | 72 +++++++++----------
src/plugins/e-acsl/tests/format/signalled.h | 7 +-
4 files changed, 81 insertions(+), 71 deletions(-)
diff --git a/src/plugins/e-acsl/tests/format/fprintf.c b/src/plugins/e-acsl/tests/format/fprintf.c
index 11678d9695f..8bbf8600c66 100644
--- a/src/plugins/e-acsl/tests/format/fprintf.c
+++ b/src/plugins/e-acsl/tests/format/fprintf.c
@@ -1,7 +1,12 @@
-/* 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>
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
index 6e1034eb6e2..b1591588c9c 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
@@ -1,6 +1,6 @@
-[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);
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
index a30a9b7fb39..ec5c8f048c1 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
@@ -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";
diff --git a/src/plugins/e-acsl/tests/format/signalled.h b/src/plugins/e-acsl/tests/format/signalled.h
index fd980c5ca64..4021210a5db 100644
--- a/src/plugins/e-acsl/tests/format/signalled.h
+++ b/src/plugins/e-acsl/tests/format/signalled.h
@@ -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;
--
GitLab