From aa5f18539cc1a3daa03c9a3758caad4d1b9c1afd Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 2 Aug 2021 18:21:32 +0200
Subject: [PATCH] [eacsl] Update tests
---
src/plugins/e-acsl/Makefile.in | 3 +-
.../tests/bts/oracle/bts2252.res.oracle | 3 -
.../e-acsl/tests/bts/oracle/gen_bts2252.c | 1 +
.../e-acsl/tests/builtin/oracle/gen_strcat.c | 413 ++++++--
.../e-acsl/tests/builtin/oracle/gen_strcpy.c | 272 ++++-
.../builtin/oracle_dev/strcat.e-acsl.err.log | 44 +-
.../builtin/oracle_dev/strcpy.e-acsl.err.log | 34 +-
src/plugins/e-acsl/tests/builtin/strcat.c | 40 +
src/plugins/e-acsl/tests/builtin/strcpy.c | 35 +
.../e-acsl/tests/format/oracle/gen_printf.c | 29 +
.../e-acsl/tests/format/oracle/gen_sprintf.c | 173 ++++
.../tests/format/oracle/printf.res.oracle | 3 -
.../tests/format/oracle/sprintf.res.oracle | 20 +
.../format/oracle_dev/printf.e-acsl.err.log | 170 ++--
.../format/oracle_dev/sprintf.e-acsl.err.log | 0
src/plugins/e-acsl/tests/format/sprintf.c | 34 +
src/plugins/e-acsl/tests/libc/file.c | 40 +
src/plugins/e-acsl/tests/libc/mem.c | 30 +
.../e-acsl/tests/libc/oracle/file.res.oracle | 52 +
.../e-acsl/tests/libc/oracle/gen_file.c | 434 ++++++++
.../e-acsl/tests/libc/oracle/gen_mem.c | 351 +++++++
.../e-acsl/tests/libc/oracle/gen_sprintf.c | 186 ++++
.../e-acsl/tests/libc/oracle/gen_str.c | 959 ++++++++++++++++++
.../e-acsl/tests/libc/oracle/mem.res.oracle | 45 +
.../tests/libc/oracle/sprintf.res.oracle | 15 +
.../e-acsl/tests/libc/oracle/str.res.oracle | 118 +++
.../tests/libc/oracle_dev/file.e-acsl.err.log | 0
.../tests/libc/oracle_dev/mem.e-acsl.err.log | 0
.../libc/oracle_dev/sprintf.e-acsl.err.log | 0
.../tests/libc/oracle_dev/str.e-acsl.err.log | 0
src/plugins/e-acsl/tests/libc/sprintf.c | 33 +
src/plugins/e-acsl/tests/libc/str.c | 76 ++
.../tests/temporal/oracle/gen_t_memcpy.c | 2 +
.../tests/temporal/oracle/t_memcpy.res.oracle | 6 -
34 files changed, 3370 insertions(+), 251 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/format/oracle/gen_sprintf.c
create mode 100644 src/plugins/e-acsl/tests/format/oracle/sprintf.res.oracle
create mode 100644 src/plugins/e-acsl/tests/format/oracle_dev/sprintf.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/format/sprintf.c
create mode 100644 src/plugins/e-acsl/tests/libc/file.c
create mode 100644 src/plugins/e-acsl/tests/libc/mem.c
create mode 100644 src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
create mode 100644 src/plugins/e-acsl/tests/libc/oracle/gen_file.c
create mode 100644 src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
create mode 100644 src/plugins/e-acsl/tests/libc/oracle/gen_sprintf.c
create mode 100644 src/plugins/e-acsl/tests/libc/oracle/gen_str.c
create mode 100644 src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
create mode 100644 src/plugins/e-acsl/tests/libc/oracle/sprintf.res.oracle
create mode 100644 src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
create mode 100644 src/plugins/e-acsl/tests/libc/oracle_dev/file.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/libc/oracle_dev/mem.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/libc/oracle_dev/sprintf.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/libc/oracle_dev/str.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/libc/sprintf.c
create mode 100644 src/plugins/e-acsl/tests/libc/str.c
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index aa7c8e23b76..a8a90519d28 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -179,7 +179,8 @@ PLUGIN_TESTS_DIRS := \
format \
temporal \
special \
- builtin
+ builtin \
+ libc
PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
index d2df68cc06e..72adb373089 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
@@ -1,7 +1,4 @@
[e-acsl] beginning translation.
-[e-acsl] Warning: annotating undefined function `strncpy':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:388: Warning:
E-ACSL construct `logic functions performing read accesses'
is not yet supported.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
index 274ddffd5a5..d5ae3f9c191 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -163,6 +163,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gen_e_acsl_at_2 = dest;
__gen_e_acsl_at = dest;
__retres = strncpy(dest,src,n);
+ __e_acsl_initialize((void *)dest,n);
{
unsigned long __gen_e_acsl_size_6;
__e_acsl_mpz_t __gen_e_acsl__8;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index 8fcaa4939fa..b26e3c1f7a7 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -30,14 +30,15 @@ char *__gen_e_acsl_literal_string_12;
char *__gen_e_acsl_literal_string_11;
char *__gen_e_acsl_literal_string_10;
char *__gen_e_acsl_literal_string_9;
-char *__gen_e_acsl_literal_string_8;
+char *__gen_e_acsl_literal_string_30;
+char *__gen_e_acsl_literal_string_7;
char *__gen_e_acsl_literal_string_6;
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
char *__gen_e_acsl_literal_string_3;
char *__gen_e_acsl_literal_string_5;
char *__gen_e_acsl_literal_string_4;
-char *__gen_e_acsl_literal_string_7;
+char *__gen_e_acsl_literal_string_8;
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
/*@ exits status: \exit_status ≡ \old(status);
@@ -75,6 +76,253 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options);
*/
pid_t __gen_e_acsl_fork(void);
+void test_memory_tracking(void)
+{
+ {
+ char dest[4];
+ __e_acsl_store_block((void *)(dest),(size_t)4);
+ __e_acsl_builtin_strcpy(dest,__gen_e_acsl_literal_string_6);
+ char src[2] = {(char)'b', (char)'\000'};
+ __e_acsl_store_block((void *)(src),(size_t)2);
+ __e_acsl_full_init((void *)(& src));
+ {
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_size = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(dest + 1 * 0),
+ (size_t)__gen_e_acsl_if);
+ __e_acsl_assert(__gen_e_acsl_initialized,1,"Assertion",
+ "test_memory_tracking","\\initialized(&dest[0 .. 1])",
+ "tests/builtin/strcat.c",14);
+ }
+ /*@ assert \initialized(&dest[0 .. 1]); */ ;
+ {
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
+ int __gen_e_acsl_initialized_2;
+ __gen_e_acsl_size_2 = 1 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(dest + 1 * 2),
+ (size_t)__gen_e_acsl_if_2);
+ __e_acsl_assert(! __gen_e_acsl_initialized_2,1,"Assertion",
+ "test_memory_tracking","!\\initialized(&dest[2 .. 3])",
+ "tests/builtin/strcat.c",15);
+ }
+ /*@ assert ¬\initialized(&dest[2 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_3;
+ int __gen_e_acsl_if_3;
+ int __gen_e_acsl_initialized_3;
+ __gen_e_acsl_size_3 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_3 <= 0) __gen_e_acsl_if_3 = 0;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(src + 1 * 0),
+ (size_t)__gen_e_acsl_if_3);
+ __e_acsl_assert(__gen_e_acsl_initialized_3,1,"Assertion",
+ "test_memory_tracking","\\initialized(&src[0 .. 1])",
+ "tests/builtin/strcat.c",16);
+ }
+ /*@ assert \initialized(&src[0 .. 1]); */ ;
+ __e_acsl_builtin_strcat(dest,(char const *)(src));
+ {
+ int __gen_e_acsl_size_4;
+ int __gen_e_acsl_if_4;
+ int __gen_e_acsl_initialized_4;
+ __gen_e_acsl_size_4 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_4 <= 0) __gen_e_acsl_if_4 = 0;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(dest + 1 * 0),
+ (size_t)__gen_e_acsl_if_4);
+ __e_acsl_assert(__gen_e_acsl_initialized_4,1,"Assertion",
+ "test_memory_tracking","\\initialized(&dest[0 .. 2])",
+ "tests/builtin/strcat.c",19);
+ }
+ /*@ assert \initialized(&dest[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& dest[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_5,1,"Assertion",
+ "test_memory_tracking","!\\initialized(&dest[3])",
+ "tests/builtin/strcat.c",20);
+ }
+ /*@ assert ¬\initialized(&dest[3]); */ ;
+ __e_acsl_delete_block((void *)(src));
+ __e_acsl_delete_block((void *)(dest));
+ }
+ {
+ char dest_0[4];
+ __e_acsl_store_block((void *)(dest_0),(size_t)4);
+ __e_acsl_builtin_strcpy(dest_0,__gen_e_acsl_literal_string_6);
+ char src_0[3] = {(char)'b', (char)'c', (char)'\000'};
+ __e_acsl_store_block((void *)(src_0),(size_t)3);
+ __e_acsl_full_init((void *)(& src_0));
+ {
+ int __gen_e_acsl_size_5;
+ int __gen_e_acsl_if_5;
+ int __gen_e_acsl_initialized_6;
+ __gen_e_acsl_size_5 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_5 <= 0) __gen_e_acsl_if_5 = 0;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(dest_0 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_5);
+ __e_acsl_assert(__gen_e_acsl_initialized_6,1,"Assertion",
+ "test_memory_tracking",
+ "\\initialized(&dest_0[0 .. 1])",
+ "tests/builtin/strcat.c",26);
+ }
+ /*@ assert \initialized(&dest_0[0 .. 1]); */ ;
+ {
+ int __gen_e_acsl_size_6;
+ int __gen_e_acsl_if_6;
+ int __gen_e_acsl_initialized_7;
+ __gen_e_acsl_size_6 = 1 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size_6 <= 0) __gen_e_acsl_if_6 = 0;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
+ __gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(dest_0 +
+ 1 * 2),
+ (size_t)__gen_e_acsl_if_6);
+ __e_acsl_assert(! __gen_e_acsl_initialized_7,1,"Assertion",
+ "test_memory_tracking",
+ "!\\initialized(&dest_0[2 .. 3])",
+ "tests/builtin/strcat.c",27);
+ }
+ /*@ assert ¬\initialized(&dest_0[2 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_7;
+ int __gen_e_acsl_if_7;
+ int __gen_e_acsl_initialized_8;
+ __gen_e_acsl_size_7 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_7 <= 0) __gen_e_acsl_if_7 = 0;
+ else __gen_e_acsl_if_7 = __gen_e_acsl_size_7;
+ __gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(src_0 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_7);
+ __e_acsl_assert(__gen_e_acsl_initialized_8,1,"Assertion",
+ "test_memory_tracking","\\initialized(&src_0[0 .. 2])",
+ "tests/builtin/strcat.c",28);
+ }
+ /*@ assert \initialized(&src_0[0 .. 2]); */ ;
+ __e_acsl_builtin_strncat(dest_0,(char const *)(src_0),(unsigned long)1);
+ {
+ int __gen_e_acsl_size_8;
+ int __gen_e_acsl_if_8;
+ int __gen_e_acsl_initialized_9;
+ __gen_e_acsl_size_8 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_8 <= 0) __gen_e_acsl_if_8 = 0;
+ else __gen_e_acsl_if_8 = __gen_e_acsl_size_8;
+ __gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)(dest_0 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_8);
+ __e_acsl_assert(__gen_e_acsl_initialized_9,1,"Assertion",
+ "test_memory_tracking",
+ "\\initialized(&dest_0[0 .. 2])",
+ "tests/builtin/strcat.c",31);
+ }
+ /*@ assert \initialized(&dest_0[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_10;
+ __gen_e_acsl_initialized_10 = __e_acsl_initialized((void *)(& dest_0[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_10,1,"Assertion",
+ "test_memory_tracking","!\\initialized(&dest_0[3])",
+ "tests/builtin/strcat.c",32);
+ }
+ /*@ assert ¬\initialized(&dest_0[3]); */ ;
+ __e_acsl_delete_block((void *)(src_0));
+ __e_acsl_delete_block((void *)(dest_0));
+ }
+ {
+ char dest_1[4];
+ __e_acsl_store_block((void *)(dest_1),(size_t)4);
+ __e_acsl_builtin_strcpy(dest_1,__gen_e_acsl_literal_string_6);
+ char src_1[2] = {(char)'b', (char)'\000'};
+ __e_acsl_store_block((void *)(src_1),(size_t)2);
+ __e_acsl_full_init((void *)(& src_1));
+ {
+ int __gen_e_acsl_size_9;
+ int __gen_e_acsl_if_9;
+ int __gen_e_acsl_initialized_11;
+ __gen_e_acsl_size_9 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_9 <= 0) __gen_e_acsl_if_9 = 0;
+ else __gen_e_acsl_if_9 = __gen_e_acsl_size_9;
+ __gen_e_acsl_initialized_11 = __e_acsl_initialized((void *)(dest_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_9);
+ __e_acsl_assert(__gen_e_acsl_initialized_11,1,"Assertion",
+ "test_memory_tracking",
+ "\\initialized(&dest_1[0 .. 1])",
+ "tests/builtin/strcat.c",38);
+ }
+ /*@ assert \initialized(&dest_1[0 .. 1]); */ ;
+ {
+ int __gen_e_acsl_size_10;
+ int __gen_e_acsl_if_10;
+ int __gen_e_acsl_initialized_12;
+ __gen_e_acsl_size_10 = 1 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size_10 <= 0) __gen_e_acsl_if_10 = 0;
+ else __gen_e_acsl_if_10 = __gen_e_acsl_size_10;
+ __gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(dest_1 +
+ 1 * 2),
+ (size_t)__gen_e_acsl_if_10);
+ __e_acsl_assert(! __gen_e_acsl_initialized_12,1,"Assertion",
+ "test_memory_tracking",
+ "!\\initialized(&dest_1[2 .. 3])",
+ "tests/builtin/strcat.c",39);
+ }
+ /*@ assert ¬\initialized(&dest_1[2 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_11;
+ int __gen_e_acsl_if_11;
+ int __gen_e_acsl_initialized_13;
+ __gen_e_acsl_size_11 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_11 <= 0) __gen_e_acsl_if_11 = 0;
+ else __gen_e_acsl_if_11 = __gen_e_acsl_size_11;
+ __gen_e_acsl_initialized_13 = __e_acsl_initialized((void *)(src_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_11);
+ __e_acsl_assert(__gen_e_acsl_initialized_13,1,"Assertion",
+ "test_memory_tracking","\\initialized(&src_1[0 .. 1])",
+ "tests/builtin/strcat.c",40);
+ }
+ /*@ assert \initialized(&src_1[0 .. 1]); */ ;
+ __e_acsl_builtin_strncat(dest_1,(char const *)(src_1),(unsigned long)2);
+ {
+ int __gen_e_acsl_size_12;
+ int __gen_e_acsl_if_12;
+ int __gen_e_acsl_initialized_14;
+ __gen_e_acsl_size_12 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_12 <= 0) __gen_e_acsl_if_12 = 0;
+ else __gen_e_acsl_if_12 = __gen_e_acsl_size_12;
+ __gen_e_acsl_initialized_14 = __e_acsl_initialized((void *)(dest_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_12);
+ __e_acsl_assert(__gen_e_acsl_initialized_14,1,"Assertion",
+ "test_memory_tracking",
+ "\\initialized(&dest_1[0 .. 2])",
+ "tests/builtin/strcat.c",43);
+ }
+ /*@ assert \initialized(&dest_1[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_15;
+ __gen_e_acsl_initialized_15 = __e_acsl_initialized((void *)(& dest_1[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_15,1,"Assertion",
+ "test_memory_tracking","!\\initialized(&dest_1[3])",
+ "tests/builtin/strcat.c",44);
+ }
+ /*@ assert ¬\initialized(&dest_1[3]); */ ;
+ __e_acsl_delete_block((void *)(src_1));
+ __e_acsl_delete_block((void *)(dest_1));
+ }
+ return;
+}
+
/*@ ensures
result_ok_child_or_error:
\result ≡ 0 ∨ \result > 0 ∨ \result ≡ -1;
@@ -191,119 +439,123 @@ 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_29 = "tests/builtin/strcat.c:61";
+ __gen_e_acsl_literal_string_29 = "tests/builtin/strcat.c:99";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
- sizeof("tests/builtin/strcat.c:61"));
+ sizeof("tests/builtin/strcat.c:99"));
__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/builtin/strcat.c:60";
+ __gen_e_acsl_literal_string_28 = "tests/builtin/strcat.c:98";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
- sizeof("tests/builtin/strcat.c:60"));
+ sizeof("tests/builtin/strcat.c:98"));
__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/builtin/strcat.c:59";
+ __gen_e_acsl_literal_string_27 = "tests/builtin/strcat.c:96";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
- sizeof("tests/builtin/strcat.c:59"));
+ sizeof("tests/builtin/strcat.c:96"));
__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/builtin/strcat.c:57";
+ __gen_e_acsl_literal_string_26 = "tests/builtin/strcat.c:95";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
- sizeof("tests/builtin/strcat.c:57"));
+ sizeof("tests/builtin/strcat.c:95"));
__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/builtin/strcat.c:56";
+ __gen_e_acsl_literal_string_25 = "tests/builtin/strcat.c:94";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
- sizeof("tests/builtin/strcat.c:56"));
+ sizeof("tests/builtin/strcat.c:94"));
__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/builtin/strcat.c:55";
+ __gen_e_acsl_literal_string_24 = "tests/builtin/strcat.c:93";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
- sizeof("tests/builtin/strcat.c:55"));
+ sizeof("tests/builtin/strcat.c:93"));
__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/builtin/strcat.c:54";
+ __gen_e_acsl_literal_string_23 = "tests/builtin/strcat.c:92";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
- sizeof("tests/builtin/strcat.c:54"));
+ sizeof("tests/builtin/strcat.c:92"));
__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_22 = "tests/builtin/strcat.c:53";
+ __gen_e_acsl_literal_string_22 = "tests/builtin/strcat.c:91";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
- sizeof("tests/builtin/strcat.c:53"));
+ sizeof("tests/builtin/strcat.c:91"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
- __gen_e_acsl_literal_string_21 = "tests/builtin/strcat.c:52";
+ __gen_e_acsl_literal_string_21 = "tests/builtin/strcat.c:90";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
- sizeof("tests/builtin/strcat.c:52"));
+ sizeof("tests/builtin/strcat.c:90"));
__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_20 = "tests/builtin/strcat.c:51";
+ __gen_e_acsl_literal_string_20 = "tests/builtin/strcat.c:77";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,
- sizeof("tests/builtin/strcat.c:51"));
+ sizeof("tests/builtin/strcat.c:77"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
- __gen_e_acsl_literal_string_19 = "tests/builtin/strcat.c:38";
+ __gen_e_acsl_literal_string_19 = "tests/builtin/strcat.c:76";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
- sizeof("tests/builtin/strcat.c:38"));
+ sizeof("tests/builtin/strcat.c:76"));
__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_18 = "tests/builtin/strcat.c:37";
+ __gen_e_acsl_literal_string_18 = "tests/builtin/strcat.c:75";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
- sizeof("tests/builtin/strcat.c:37"));
+ sizeof("tests/builtin/strcat.c:75"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
- __gen_e_acsl_literal_string_17 = "tests/builtin/strcat.c:36";
+ __gen_e_acsl_literal_string_17 = "tests/builtin/strcat.c:74";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,
- sizeof("tests/builtin/strcat.c:36"));
+ sizeof("tests/builtin/strcat.c:74"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
- __gen_e_acsl_literal_string_16 = "tests/builtin/strcat.c:35";
+ __gen_e_acsl_literal_string_16 = "tests/builtin/strcat.c:73";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
- sizeof("tests/builtin/strcat.c:35"));
+ sizeof("tests/builtin/strcat.c:73"));
__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/builtin/strcat.c:34";
+ __gen_e_acsl_literal_string_15 = "tests/builtin/strcat.c:72";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
- sizeof("tests/builtin/strcat.c:34"));
+ sizeof("tests/builtin/strcat.c:72"));
__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/builtin/strcat.c:33";
+ __gen_e_acsl_literal_string_14 = "tests/builtin/strcat.c:71";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
- sizeof("tests/builtin/strcat.c:33"));
+ sizeof("tests/builtin/strcat.c:71"));
__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/builtin/strcat.c:32";
+ __gen_e_acsl_literal_string_13 = "tests/builtin/strcat.c:70";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
- sizeof("tests/builtin/strcat.c:32"));
+ sizeof("tests/builtin/strcat.c:70"));
__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/builtin/strcat.c:31";
+ __gen_e_acsl_literal_string_12 = "tests/builtin/strcat.c:69";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
- sizeof("tests/builtin/strcat.c:31"));
+ sizeof("tests/builtin/strcat.c:69"));
__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_11 = "tests/builtin/strcat.c:30";
+ __gen_e_acsl_literal_string_11 = "tests/builtin/strcat.c:68";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
- sizeof("tests/builtin/strcat.c:30"));
+ sizeof("tests/builtin/strcat.c:68"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
- __gen_e_acsl_literal_string_10 = "tests/builtin/strcat.c:29";
+ __gen_e_acsl_literal_string_10 = "tests/builtin/strcat.c:67";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
- sizeof("tests/builtin/strcat.c:29"));
+ sizeof("tests/builtin/strcat.c:67"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
- __gen_e_acsl_literal_string_9 = "tests/builtin/strcat.c:28";
+ __gen_e_acsl_literal_string_9 = "tests/builtin/strcat.c:66";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
- sizeof("tests/builtin/strcat.c:28"));
+ sizeof("tests/builtin/strcat.c:66"));
__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/builtin/strcat.c:27";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
- sizeof("tests/builtin/strcat.c:27"));
- __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_6 = "abcd";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,
+ __gen_e_acsl_literal_string_30 = "tests/builtin/strcat.c:100";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_30,
+ sizeof("tests/builtin/strcat.c:100"));
+ __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_7 = "abcd";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,
sizeof("abcd"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
+ __gen_e_acsl_literal_string_6 = "a";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,sizeof("a"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
__gen_e_acsl_literal_string = "TEST %d: ";
@@ -331,10 +583,10 @@ void __e_acsl_globals_init(void)
sizeof("FAIL: Unexpected execution at %s\n"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
- __gen_e_acsl_literal_string_7 = "";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,sizeof(""));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
+ __gen_e_acsl_literal_string_8 = "";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,sizeof(""));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
}
return;
}
@@ -344,10 +596,10 @@ int main(int argc, char const **argv)
int __retres;
__e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
__e_acsl_globals_init();
- char *const_str = (char *)__gen_e_acsl_literal_string_6;
+ char *const_str = (char *)__gen_e_acsl_literal_string_7;
char *unalloc_str = malloc((unsigned long)5);
char *_barrier = malloc((unsigned long)1);
- char *empty_str = (char *)__gen_e_acsl_literal_string_7;
+ char *empty_str = (char *)__gen_e_acsl_literal_string_8;
free((void *)unalloc_str);
{
char dest1[9] =
@@ -388,7 +640,7 @@ int main(int argc, char const **argv)
int process_status;
__e_acsl_store_block((void *)(& process_status),(size_t)4);
__gen_e_acsl_waitpid(pid,& process_status,0);
- signal_eval(process_status,0,__gen_e_acsl_literal_string_8);
+ signal_eval(process_status,0,__gen_e_acsl_literal_string_9);
__e_acsl_delete_block((void *)(& process_status));
}
}
@@ -402,7 +654,7 @@ int main(int argc, char const **argv)
int process_status_0;
__e_acsl_store_block((void *)(& process_status_0),(size_t)4);
__gen_e_acsl_waitpid(pid_0,& process_status_0,0);
- signal_eval(process_status_0,0,__gen_e_acsl_literal_string_9);
+ signal_eval(process_status_0,0,__gen_e_acsl_literal_string_10);
__e_acsl_delete_block((void *)(& process_status_0));
}
}
@@ -416,7 +668,7 @@ int main(int argc, char const **argv)
int process_status_1;
__e_acsl_store_block((void *)(& process_status_1),(size_t)4);
__gen_e_acsl_waitpid(pid_1,& process_status_1,0);
- signal_eval(process_status_1,1,__gen_e_acsl_literal_string_10);
+ signal_eval(process_status_1,1,__gen_e_acsl_literal_string_11);
__e_acsl_delete_block((void *)(& process_status_1));
}
}
@@ -430,7 +682,7 @@ int main(int argc, char const **argv)
int process_status_2;
__e_acsl_store_block((void *)(& process_status_2),(size_t)4);
__gen_e_acsl_waitpid(pid_2,& process_status_2,0);
- signal_eval(process_status_2,1,__gen_e_acsl_literal_string_11);
+ signal_eval(process_status_2,1,__gen_e_acsl_literal_string_12);
__e_acsl_delete_block((void *)(& process_status_2));
}
}
@@ -444,21 +696,21 @@ int main(int argc, char const **argv)
int process_status_3;
__e_acsl_store_block((void *)(& process_status_3),(size_t)4);
__gen_e_acsl_waitpid(pid_3,& process_status_3,0);
- signal_eval(process_status_3,1,__gen_e_acsl_literal_string_12);
+ signal_eval(process_status_3,1,__gen_e_acsl_literal_string_13);
__e_acsl_delete_block((void *)(& process_status_3));
}
}
{
pid_t pid_4 = __gen_e_acsl_fork();
if (! pid_4) {
- __e_acsl_builtin_strcat((char *)0,__gen_e_acsl_literal_string_7);
+ __e_acsl_builtin_strcat((char *)0,__gen_e_acsl_literal_string_8);
__gen_e_acsl_exit(0);
}
else {
int process_status_4;
__e_acsl_store_block((void *)(& process_status_4),(size_t)4);
__gen_e_acsl_waitpid(pid_4,& process_status_4,0);
- signal_eval(process_status_4,1,__gen_e_acsl_literal_string_13);
+ signal_eval(process_status_4,1,__gen_e_acsl_literal_string_14);
__e_acsl_delete_block((void *)(& process_status_4));
}
}
@@ -472,7 +724,7 @@ int main(int argc, char const **argv)
int process_status_5;
__e_acsl_store_block((void *)(& process_status_5),(size_t)4);
__gen_e_acsl_waitpid(pid_5,& process_status_5,0);
- signal_eval(process_status_5,1,__gen_e_acsl_literal_string_14);
+ signal_eval(process_status_5,1,__gen_e_acsl_literal_string_15);
__e_acsl_delete_block((void *)(& process_status_5));
}
}
@@ -486,7 +738,7 @@ int main(int argc, char const **argv)
int process_status_6;
__e_acsl_store_block((void *)(& process_status_6),(size_t)4);
__gen_e_acsl_waitpid(pid_6,& process_status_6,0);
- signal_eval(process_status_6,1,__gen_e_acsl_literal_string_15);
+ signal_eval(process_status_6,1,__gen_e_acsl_literal_string_16);
__e_acsl_delete_block((void *)(& process_status_6));
}
}
@@ -500,7 +752,7 @@ int main(int argc, char const **argv)
int process_status_7;
__e_acsl_store_block((void *)(& process_status_7),(size_t)4);
__gen_e_acsl_waitpid(pid_7,& process_status_7,0);
- signal_eval(process_status_7,1,__gen_e_acsl_literal_string_16);
+ signal_eval(process_status_7,1,__gen_e_acsl_literal_string_17);
__e_acsl_delete_block((void *)(& process_status_7));
}
}
@@ -514,7 +766,7 @@ int main(int argc, char const **argv)
int process_status_8;
__e_acsl_store_block((void *)(& process_status_8),(size_t)4);
__gen_e_acsl_waitpid(pid_8,& process_status_8,0);
- signal_eval(process_status_8,1,__gen_e_acsl_literal_string_17);
+ signal_eval(process_status_8,1,__gen_e_acsl_literal_string_18);
__e_acsl_delete_block((void *)(& process_status_8));
}
}
@@ -528,7 +780,7 @@ int main(int argc, char const **argv)
int process_status_9;
__e_acsl_store_block((void *)(& process_status_9),(size_t)4);
__gen_e_acsl_waitpid(pid_9,& process_status_9,0);
- signal_eval(process_status_9,1,__gen_e_acsl_literal_string_18);
+ signal_eval(process_status_9,1,__gen_e_acsl_literal_string_19);
__e_acsl_delete_block((void *)(& process_status_9));
}
}
@@ -544,7 +796,7 @@ int main(int argc, char const **argv)
int process_status_10;
__e_acsl_store_block((void *)(& process_status_10),(size_t)4);
__gen_e_acsl_waitpid(pid_10,& process_status_10,0);
- signal_eval(process_status_10,0,__gen_e_acsl_literal_string_19);
+ signal_eval(process_status_10,0,__gen_e_acsl_literal_string_20);
__e_acsl_delete_block((void *)(& process_status_10));
}
__e_acsl_delete_block((void *)(& pd4));
@@ -597,7 +849,7 @@ int main(int argc, char const **argv)
int process_status_11;
__e_acsl_store_block((void *)(& process_status_11),(size_t)4);
__gen_e_acsl_waitpid(pid_11,& process_status_11,0);
- signal_eval(process_status_11,0,__gen_e_acsl_literal_string_20);
+ signal_eval(process_status_11,0,__gen_e_acsl_literal_string_21);
__e_acsl_delete_block((void *)(& process_status_11));
}
}
@@ -612,7 +864,7 @@ int main(int argc, char const **argv)
int process_status_12;
__e_acsl_store_block((void *)(& process_status_12),(size_t)4);
__gen_e_acsl_waitpid(pid_12,& process_status_12,0);
- signal_eval(process_status_12,1,__gen_e_acsl_literal_string_21);
+ signal_eval(process_status_12,1,__gen_e_acsl_literal_string_22);
__e_acsl_delete_block((void *)(& process_status_12));
}
}
@@ -627,7 +879,7 @@ int main(int argc, char const **argv)
int process_status_13;
__e_acsl_store_block((void *)(& process_status_13),(size_t)4);
__gen_e_acsl_waitpid(pid_13,& process_status_13,0);
- signal_eval(process_status_13,1,__gen_e_acsl_literal_string_22);
+ signal_eval(process_status_13,1,__gen_e_acsl_literal_string_23);
__e_acsl_delete_block((void *)(& process_status_13));
}
}
@@ -642,7 +894,7 @@ int main(int argc, char const **argv)
int process_status_14;
__e_acsl_store_block((void *)(& process_status_14),(size_t)4);
__gen_e_acsl_waitpid(pid_14,& process_status_14,0);
- signal_eval(process_status_14,1,__gen_e_acsl_literal_string_23);
+ signal_eval(process_status_14,1,__gen_e_acsl_literal_string_24);
__e_acsl_delete_block((void *)(& process_status_14));
}
}
@@ -657,7 +909,7 @@ int main(int argc, char const **argv)
int process_status_15;
__e_acsl_store_block((void *)(& process_status_15),(size_t)4);
__gen_e_acsl_waitpid(pid_15,& process_status_15,0);
- signal_eval(process_status_15,1,__gen_e_acsl_literal_string_24);
+ signal_eval(process_status_15,1,__gen_e_acsl_literal_string_25);
__e_acsl_delete_block((void *)(& process_status_15));
}
}
@@ -671,7 +923,7 @@ int main(int argc, char const **argv)
int process_status_16;
__e_acsl_store_block((void *)(& process_status_16),(size_t)4);
__gen_e_acsl_waitpid(pid_16,& process_status_16,0);
- signal_eval(process_status_16,1,__gen_e_acsl_literal_string_25);
+ signal_eval(process_status_16,1,__gen_e_acsl_literal_string_26);
__e_acsl_delete_block((void *)(& process_status_16));
}
}
@@ -686,7 +938,7 @@ int main(int argc, char const **argv)
int process_status_17;
__e_acsl_store_block((void *)(& process_status_17),(size_t)4);
__gen_e_acsl_waitpid(pid_17,& process_status_17,0);
- signal_eval(process_status_17,1,__gen_e_acsl_literal_string_26);
+ signal_eval(process_status_17,1,__gen_e_acsl_literal_string_27);
__e_acsl_delete_block((void *)(& process_status_17));
}
}
@@ -700,7 +952,7 @@ int main(int argc, char const **argv)
int process_status_18;
__e_acsl_store_block((void *)(& process_status_18),(size_t)4);
__gen_e_acsl_waitpid(pid_18,& process_status_18,0);
- signal_eval(process_status_18,1,__gen_e_acsl_literal_string_27);
+ signal_eval(process_status_18,1,__gen_e_acsl_literal_string_28);
__e_acsl_delete_block((void *)(& process_status_18));
}
}
@@ -715,7 +967,7 @@ int main(int argc, char const **argv)
int process_status_19;
__e_acsl_store_block((void *)(& process_status_19),(size_t)4);
__gen_e_acsl_waitpid(pid_19,& process_status_19,0);
- signal_eval(process_status_19,1,__gen_e_acsl_literal_string_28);
+ signal_eval(process_status_19,1,__gen_e_acsl_literal_string_29);
__e_acsl_delete_block((void *)(& process_status_19));
}
}
@@ -730,7 +982,7 @@ int main(int argc, char const **argv)
int process_status_20;
__e_acsl_store_block((void *)(& process_status_20),(size_t)4);
__gen_e_acsl_waitpid(pid_20,& process_status_20,0);
- signal_eval(process_status_20,1,__gen_e_acsl_literal_string_29);
+ signal_eval(process_status_20,1,__gen_e_acsl_literal_string_30);
__e_acsl_delete_block((void *)(& process_status_20));
}
__e_acsl_delete_block((void *)(& pd4_0));
@@ -743,6 +995,7 @@ int main(int argc, char const **argv)
__e_acsl_delete_block((void *)(dest1_0));
}
}
+ test_memory_tracking();
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 09d7c8aff99..a43aa68428e 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -98,6 +98,209 @@ pid_t __gen_e_acsl_fork(void);
*/
char *__gen_e_acsl_strdup(char const *s);
+void test_memory_tracking(void)
+{
+ {
+ char dest[4];
+ __e_acsl_store_block((void *)(dest),(size_t)4);
+ char src[2] = {(char)'b', (char)'\000'};
+ __e_acsl_store_block((void *)(src),(size_t)2);
+ __e_acsl_full_init((void *)(& src));
+ {
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_size = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(dest + 1 * 0),
+ (size_t)__gen_e_acsl_if);
+ __e_acsl_assert(! __gen_e_acsl_initialized,1,"Assertion",
+ "test_memory_tracking","!\\initialized(&dest[0 .. 3])",
+ "tests/builtin/strcpy.c",13);
+ }
+ /*@ assert ¬\initialized(&dest[0 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
+ int __gen_e_acsl_initialized_2;
+ __gen_e_acsl_size_2 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(src + 1 * 0),
+ (size_t)__gen_e_acsl_if_2);
+ __e_acsl_assert(__gen_e_acsl_initialized_2,1,"Assertion",
+ "test_memory_tracking","\\initialized(&src[0 .. 1])",
+ "tests/builtin/strcpy.c",14);
+ }
+ /*@ assert \initialized(&src[0 .. 1]); */ ;
+ __e_acsl_builtin_strcpy(dest,(char const *)(src));
+ {
+ int __gen_e_acsl_size_3;
+ int __gen_e_acsl_if_3;
+ int __gen_e_acsl_initialized_3;
+ __gen_e_acsl_size_3 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_3 <= 0) __gen_e_acsl_if_3 = 0;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(dest + 1 * 0),
+ (size_t)__gen_e_acsl_if_3);
+ __e_acsl_assert(__gen_e_acsl_initialized_3,1,"Assertion",
+ "test_memory_tracking","\\initialized(&dest[0 .. 1])",
+ "tests/builtin/strcpy.c",17);
+ }
+ /*@ assert \initialized(&dest[0 .. 1]); */ ;
+ {
+ int __gen_e_acsl_size_4;
+ int __gen_e_acsl_if_4;
+ int __gen_e_acsl_initialized_4;
+ __gen_e_acsl_size_4 = 1 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size_4 <= 0) __gen_e_acsl_if_4 = 0;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(dest + 1 * 2),
+ (size_t)__gen_e_acsl_if_4);
+ __e_acsl_assert(! __gen_e_acsl_initialized_4,1,"Assertion",
+ "test_memory_tracking","!\\initialized(&dest[2 .. 3])",
+ "tests/builtin/strcpy.c",18);
+ }
+ /*@ assert ¬\initialized(&dest[2 .. 3]); */ ;
+ __e_acsl_delete_block((void *)(src));
+ __e_acsl_delete_block((void *)(dest));
+ }
+ {
+ char dest_0[4];
+ __e_acsl_store_block((void *)(dest_0),(size_t)4);
+ char src_0[4] = {(char)'a', (char)'b', (char)'\000'};
+ __e_acsl_store_block((void *)(src_0),(size_t)4);
+ __e_acsl_full_init((void *)(& src_0));
+ {
+ int __gen_e_acsl_size_5;
+ int __gen_e_acsl_if_5;
+ int __gen_e_acsl_initialized_5;
+ __gen_e_acsl_size_5 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_5 <= 0) __gen_e_acsl_if_5 = 0;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(dest_0 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_5);
+ __e_acsl_assert(! __gen_e_acsl_initialized_5,1,"Assertion",
+ "test_memory_tracking",
+ "!\\initialized(&dest_0[0 .. 3])",
+ "tests/builtin/strcpy.c",23);
+ }
+ /*@ assert ¬\initialized(&dest_0[0 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_6;
+ int __gen_e_acsl_if_6;
+ int __gen_e_acsl_initialized_6;
+ __gen_e_acsl_size_6 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_6 <= 0) __gen_e_acsl_if_6 = 0;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(src_0 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_6);
+ __e_acsl_assert(__gen_e_acsl_initialized_6,1,"Assertion",
+ "test_memory_tracking","\\initialized(&src_0[0 .. 3])",
+ "tests/builtin/strcpy.c",24);
+ }
+ /*@ assert \initialized(&src_0[0 .. 3]); */ ;
+ __e_acsl_builtin_strncpy(dest_0,(char const *)(src_0),(unsigned long)1);
+ {
+ int __gen_e_acsl_initialized_7;
+ __gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(dest_0),
+ sizeof(char));
+ __e_acsl_assert(__gen_e_acsl_initialized_7,1,"Assertion",
+ "test_memory_tracking","\\initialized((char *)dest_0)",
+ "tests/builtin/strcpy.c",27);
+ }
+ /*@ assert \initialized((char *)dest_0); */ ;
+ {
+ int __gen_e_acsl_size_7;
+ int __gen_e_acsl_if_7;
+ int __gen_e_acsl_initialized_8;
+ __gen_e_acsl_size_7 = 1 * ((3 - 1) + 1);
+ if (__gen_e_acsl_size_7 <= 0) __gen_e_acsl_if_7 = 0;
+ else __gen_e_acsl_if_7 = __gen_e_acsl_size_7;
+ __gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(dest_0 +
+ 1 * 1),
+ (size_t)__gen_e_acsl_if_7);
+ __e_acsl_assert(! __gen_e_acsl_initialized_8,1,"Assertion",
+ "test_memory_tracking",
+ "!\\initialized(&dest_0[1 .. 3])",
+ "tests/builtin/strcpy.c",28);
+ }
+ /*@ assert ¬\initialized(&dest_0[1 .. 3]); */ ;
+ __e_acsl_delete_block((void *)(src_0));
+ __e_acsl_delete_block((void *)(dest_0));
+ }
+ {
+ char dest_1[4];
+ __e_acsl_store_block((void *)(dest_1),(size_t)4);
+ char src_1[4] = {(char)'b', (char)'\000'};
+ __e_acsl_store_block((void *)(src_1),(size_t)4);
+ __e_acsl_full_init((void *)(& src_1));
+ {
+ int __gen_e_acsl_size_8;
+ int __gen_e_acsl_if_8;
+ int __gen_e_acsl_initialized_9;
+ __gen_e_acsl_size_8 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_8 <= 0) __gen_e_acsl_if_8 = 0;
+ else __gen_e_acsl_if_8 = __gen_e_acsl_size_8;
+ __gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)(dest_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_8);
+ __e_acsl_assert(! __gen_e_acsl_initialized_9,1,"Assertion",
+ "test_memory_tracking",
+ "!\\initialized(&dest_1[0 .. 3])",
+ "tests/builtin/strcpy.c",33);
+ }
+ /*@ assert ¬\initialized(&dest_1[0 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_9;
+ int __gen_e_acsl_if_9;
+ int __gen_e_acsl_initialized_10;
+ __gen_e_acsl_size_9 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_9 <= 0) __gen_e_acsl_if_9 = 0;
+ else __gen_e_acsl_if_9 = __gen_e_acsl_size_9;
+ __gen_e_acsl_initialized_10 = __e_acsl_initialized((void *)(src_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_9);
+ __e_acsl_assert(__gen_e_acsl_initialized_10,1,"Assertion",
+ "test_memory_tracking","\\initialized(&src_1[0 .. 3])",
+ "tests/builtin/strcpy.c",34);
+ }
+ /*@ assert \initialized(&src_1[0 .. 3]); */ ;
+ __e_acsl_builtin_strncpy(dest_1,(char const *)(src_1),(unsigned long)3);
+ {
+ int __gen_e_acsl_size_10;
+ int __gen_e_acsl_if_10;
+ int __gen_e_acsl_initialized_11;
+ __gen_e_acsl_size_10 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_10 <= 0) __gen_e_acsl_if_10 = 0;
+ else __gen_e_acsl_if_10 = __gen_e_acsl_size_10;
+ __gen_e_acsl_initialized_11 = __e_acsl_initialized((void *)(dest_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_10);
+ __e_acsl_assert(__gen_e_acsl_initialized_11,1,"Assertion",
+ "test_memory_tracking",
+ "\\initialized(&dest_1[0 .. 2])",
+ "tests/builtin/strcpy.c",37);
+ }
+ /*@ assert \initialized(&dest_1[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_12;
+ __gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& dest_1[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_12,1,"Assertion",
+ "test_memory_tracking","!\\initialized(&dest_1[3])",
+ "tests/builtin/strcpy.c",38);
+ }
+ /*@ assert ¬\initialized(&dest_1[3]); */ ;
+ __e_acsl_delete_block((void *)(src_1));
+ __e_acsl_delete_block((void *)(dest_1));
+ }
+ return;
+}
+
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result
@@ -260,89 +463,89 @@ 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_24 = "tests/builtin/strcpy.c:39";
+ __gen_e_acsl_literal_string_24 = "tests/builtin/strcpy.c:72";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
- sizeof("tests/builtin/strcpy.c:39"));
+ sizeof("tests/builtin/strcpy.c:72"));
__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/builtin/strcpy.c:38";
+ __gen_e_acsl_literal_string_23 = "tests/builtin/strcpy.c:71";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
- sizeof("tests/builtin/strcpy.c:38"));
+ sizeof("tests/builtin/strcpy.c:71"));
__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_22 = "tests/builtin/strcpy.c:37";
+ __gen_e_acsl_literal_string_22 = "tests/builtin/strcpy.c:70";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
- sizeof("tests/builtin/strcpy.c:37"));
+ sizeof("tests/builtin/strcpy.c:70"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
- __gen_e_acsl_literal_string_21 = "tests/builtin/strcpy.c:36";
+ __gen_e_acsl_literal_string_21 = "tests/builtin/strcpy.c:69";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
- sizeof("tests/builtin/strcpy.c:36"));
+ sizeof("tests/builtin/strcpy.c:69"));
__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_20 = "tests/builtin/strcpy.c:35";
+ __gen_e_acsl_literal_string_20 = "tests/builtin/strcpy.c:68";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,
- sizeof("tests/builtin/strcpy.c:35"));
+ sizeof("tests/builtin/strcpy.c:68"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
- __gen_e_acsl_literal_string_19 = "tests/builtin/strcpy.c:34";
+ __gen_e_acsl_literal_string_19 = "tests/builtin/strcpy.c:67";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
- sizeof("tests/builtin/strcpy.c:34"));
+ sizeof("tests/builtin/strcpy.c:67"));
__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_18 = "tests/builtin/strcpy.c:33";
+ __gen_e_acsl_literal_string_18 = "tests/builtin/strcpy.c:66";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
- sizeof("tests/builtin/strcpy.c:33"));
+ sizeof("tests/builtin/strcpy.c:66"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
- __gen_e_acsl_literal_string_17 = "tests/builtin/strcpy.c:32";
+ __gen_e_acsl_literal_string_17 = "tests/builtin/strcpy.c:65";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,
- sizeof("tests/builtin/strcpy.c:32"));
+ sizeof("tests/builtin/strcpy.c:65"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
- __gen_e_acsl_literal_string_16 = "tests/builtin/strcpy.c:29";
+ __gen_e_acsl_literal_string_16 = "tests/builtin/strcpy.c:62";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
- sizeof("tests/builtin/strcpy.c:29"));
+ sizeof("tests/builtin/strcpy.c:62"));
__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/builtin/strcpy.c:28";
+ __gen_e_acsl_literal_string_15 = "tests/builtin/strcpy.c:61";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
- sizeof("tests/builtin/strcpy.c:28"));
+ sizeof("tests/builtin/strcpy.c:61"));
__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/builtin/strcpy.c:27";
+ __gen_e_acsl_literal_string_14 = "tests/builtin/strcpy.c:60";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
- sizeof("tests/builtin/strcpy.c:27"));
+ sizeof("tests/builtin/strcpy.c:60"));
__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/builtin/strcpy.c:26";
+ __gen_e_acsl_literal_string_13 = "tests/builtin/strcpy.c:59";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
- sizeof("tests/builtin/strcpy.c:26"));
+ sizeof("tests/builtin/strcpy.c:59"));
__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/builtin/strcpy.c:25";
+ __gen_e_acsl_literal_string_12 = "tests/builtin/strcpy.c:58";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
- sizeof("tests/builtin/strcpy.c:25"));
+ sizeof("tests/builtin/strcpy.c:58"));
__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_11 = "tests/builtin/strcpy.c:24";
+ __gen_e_acsl_literal_string_11 = "tests/builtin/strcpy.c:57";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
- sizeof("tests/builtin/strcpy.c:24"));
+ sizeof("tests/builtin/strcpy.c:57"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
- __gen_e_acsl_literal_string_10 = "tests/builtin/strcpy.c:23";
+ __gen_e_acsl_literal_string_10 = "tests/builtin/strcpy.c:56";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
- sizeof("tests/builtin/strcpy.c:23"));
+ sizeof("tests/builtin/strcpy.c:56"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
- __gen_e_acsl_literal_string_9 = "tests/builtin/strcpy.c:22";
+ __gen_e_acsl_literal_string_9 = "tests/builtin/strcpy.c:55";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
- sizeof("tests/builtin/strcpy.c:22"));
+ sizeof("tests/builtin/strcpy.c:55"));
__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_7 = "tests/builtin/strcpy.c:21";
+ __gen_e_acsl_literal_string_7 = "tests/builtin/strcpy.c:54";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,
- sizeof("tests/builtin/strcpy.c:21"));
+ sizeof("tests/builtin/strcpy.c:54"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
__gen_e_acsl_literal_string_6 = "abcd";
@@ -643,6 +846,7 @@ int main(int argc, char const **argv)
free((void *)src);
free((void *)dest1);
free((void *)dest2);
+ test_memory_tracking();
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
index ab8fc09f167..3e0326a3b60 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
@@ -1,40 +1,40 @@
-TEST 1: OK: Expected execution at tests/builtin/strcat.c:27
-TEST 2: OK: Expected execution at tests/builtin/strcat.c:28
+TEST 1: OK: Expected execution at tests/builtin/strcat.c:66
+TEST 2: OK: Expected execution at tests/builtin/strcat.c:67
strcat: insufficient space in destination string, available: 8 bytes, requires at least 9 bytes
-TEST 3: OK: Expected signal at tests/builtin/strcat.c:29
+TEST 3: OK: Expected signal at tests/builtin/strcat.c:68
strcat: destination string string unallocated
-TEST 4: OK: Expected signal at tests/builtin/strcat.c:30
+TEST 4: OK: Expected signal at tests/builtin/strcat.c:69
strcat: source string string unallocated
-TEST 5: OK: Expected signal at tests/builtin/strcat.c:31
+TEST 5: OK: Expected signal at tests/builtin/strcat.c:70
strcat: destination string string unallocated
-TEST 6: OK: Expected signal at tests/builtin/strcat.c:32
+TEST 6: OK: Expected signal at tests/builtin/strcat.c:71
strcat: source string string unallocated
-TEST 7: OK: Expected signal at tests/builtin/strcat.c:33
+TEST 7: OK: Expected signal at tests/builtin/strcat.c:72
strcat: destination string string is not writable
-TEST 8: OK: Expected signal at tests/builtin/strcat.c:34
+TEST 8: OK: Expected signal at tests/builtin/strcat.c:73
strcat: overlapping memory areas
-TEST 9: OK: Expected signal at tests/builtin/strcat.c:35
+TEST 9: OK: Expected signal at tests/builtin/strcat.c:74
strcat: overlapping memory areas
-TEST 10: OK: Expected signal at tests/builtin/strcat.c:36
+TEST 10: OK: Expected signal at tests/builtin/strcat.c:75
strcat: overlapping memory areas
-TEST 11: OK: Expected signal at tests/builtin/strcat.c:37
-TEST 12: OK: Expected execution at tests/builtin/strcat.c:38
-TEST 13: OK: Expected execution at tests/builtin/strcat.c:51
+TEST 11: OK: Expected signal at tests/builtin/strcat.c:76
+TEST 12: OK: Expected execution at tests/builtin/strcat.c:77
+TEST 13: OK: Expected execution at tests/builtin/strcat.c:90
strncat: insufficient space in destination string, available: 8 bytes, requires at least 9 bytes
-TEST 14: OK: Expected signal at tests/builtin/strcat.c:52
+TEST 14: OK: Expected signal at tests/builtin/strcat.c:91
strcat: destination string string unallocated
-TEST 15: OK: Expected signal at tests/builtin/strcat.c:53
+TEST 15: OK: Expected signal at tests/builtin/strcat.c:92
strncat: source string string unallocated
-TEST 16: OK: Expected signal at tests/builtin/strcat.c:54
+TEST 16: OK: Expected signal at tests/builtin/strcat.c:93
strcat: destination string string unallocated
-TEST 17: OK: Expected signal at tests/builtin/strcat.c:55
+TEST 17: OK: Expected signal at tests/builtin/strcat.c:94
strncat: source string string unallocated
-TEST 18: OK: Expected signal at tests/builtin/strcat.c:56
+TEST 18: OK: Expected signal at tests/builtin/strcat.c:95
strcat: destination string string is not writable
-TEST 19: OK: Expected signal at tests/builtin/strcat.c:57
+TEST 19: OK: Expected signal at tests/builtin/strcat.c:96
strcat: overlapping memory areas
-TEST 20: OK: Expected signal at tests/builtin/strcat.c:59
+TEST 20: OK: Expected signal at tests/builtin/strcat.c:98
strncat: insufficient space in destination string, available: 6 bytes, requires at least 7 bytes
-TEST 21: OK: Expected signal at tests/builtin/strcat.c:60
+TEST 21: OK: Expected signal at tests/builtin/strcat.c:99
strcat: overlapping memory areas
-TEST 22: OK: Expected signal at tests/builtin/strcat.c:61
+TEST 22: OK: Expected signal at tests/builtin/strcat.c:100
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcpy.e-acsl.err.log b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcpy.e-acsl.err.log
index eba27da3669..478465e4ea3 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcpy.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcpy.e-acsl.err.log
@@ -1,27 +1,27 @@
-TEST 1: OK: Expected execution at tests/builtin/strcpy.c:21
-TEST 2: OK: Expected execution at tests/builtin/strcpy.c:22
+TEST 1: OK: Expected execution at tests/builtin/strcpy.c:54
+TEST 2: OK: Expected execution at tests/builtin/strcpy.c:55
strlen: insufficient space in destination string, at least 5 bytes required
-TEST 3: OK: Expected signal at tests/builtin/strcpy.c:23
+TEST 3: OK: Expected signal at tests/builtin/strcpy.c:56
strlen: destination string space unallocated or cannot be written
-TEST 4: OK: Expected signal at tests/builtin/strcpy.c:24
+TEST 4: OK: Expected signal at tests/builtin/strcpy.c:57
strlen: destination string space unallocated or cannot be written
-TEST 5: OK: Expected signal at tests/builtin/strcpy.c:25
-TEST 6: OK: Expected execution at tests/builtin/strcpy.c:26
+TEST 5: OK: Expected signal at tests/builtin/strcpy.c:58
+TEST 6: OK: Expected execution at tests/builtin/strcpy.c:59
strcpy: overlapping memory areas
-TEST 7: OK: Expected signal at tests/builtin/strcpy.c:27
-TEST 8: OK: Expected execution at tests/builtin/strcpy.c:28
+TEST 7: OK: Expected signal at tests/builtin/strcpy.c:60
+TEST 8: OK: Expected execution at tests/builtin/strcpy.c:61
strcpy: overlapping memory areas
-TEST 9: OK: Expected signal at tests/builtin/strcpy.c:29
-TEST 10: OK: Expected execution at tests/builtin/strcpy.c:32
+TEST 9: OK: Expected signal at tests/builtin/strcpy.c:62
+TEST 10: OK: Expected execution at tests/builtin/strcpy.c:65
strncpy: insufficient space in destination string , at least 6 bytes required
-TEST 11: OK: Expected signal at tests/builtin/strcpy.c:33
+TEST 11: OK: Expected signal at tests/builtin/strcpy.c:66
strncpy: destination string space unallocated or cannot be written
-TEST 12: OK: Expected signal at tests/builtin/strcpy.c:34
+TEST 12: OK: Expected signal at tests/builtin/strcpy.c:67
strncpy: destination string space unallocated or cannot be written
-TEST 13: OK: Expected signal at tests/builtin/strcpy.c:35
-TEST 14: OK: Expected execution at tests/builtin/strcpy.c:36
+TEST 13: OK: Expected signal at tests/builtin/strcpy.c:68
+TEST 14: OK: Expected execution at tests/builtin/strcpy.c:69
strncpy: overlapping memory areas
-TEST 15: OK: Expected signal at tests/builtin/strcpy.c:37
-TEST 16: OK: Expected execution at tests/builtin/strcpy.c:38
+TEST 15: OK: Expected signal at tests/builtin/strcpy.c:70
+TEST 16: OK: Expected execution at tests/builtin/strcpy.c:71
strncpy: overlapping memory areas
-TEST 17: OK: Expected signal at tests/builtin/strcpy.c:39
+TEST 17: OK: Expected signal at tests/builtin/strcpy.c:72
diff --git a/src/plugins/e-acsl/tests/builtin/strcat.c b/src/plugins/e-acsl/tests/builtin/strcat.c
index 913f1208a13..395d13a3a00 100644
--- a/src/plugins/e-acsl/tests/builtin/strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/strcat.c
@@ -6,6 +6,45 @@
#include <string.h>
#include <stdlib.h>
+void test_memory_tracking() {
+ {
+ char dest[4];
+ strcpy(dest, "a");
+ char src[] = "b";
+ //@ assert \initialized(&dest[0..1]);
+ //@ assert !\initialized(&dest[2..3]);
+ //@ assert \initialized(&src[0..1]);
+
+ strcat(dest, src);
+ //@ assert \initialized(&dest[0..2]);
+ //@ assert !\initialized(&dest[3]);
+ }
+ { // strncat with n < strlen(src)
+ char dest[4];
+ strcpy(dest, "a");
+ char src[] = "bc";
+ //@ assert \initialized(&dest[0..1]);
+ //@ assert !\initialized(&dest[2..3]);
+ //@ assert \initialized(&src[0..2]);
+
+ strncat(dest, src, 1);
+ //@ assert \initialized(&dest[0..2]);
+ //@ assert !\initialized(&dest[3]);
+ }
+ { // strncat with n >= strlen(src)
+ char dest[4];
+ strcpy(dest, "a");
+ char src[] = "b";
+ //@ assert \initialized(&dest[0..1]);
+ //@ assert !\initialized(&dest[2..3]);
+ //@ assert \initialized(&src[0..1]);
+
+ strncat(dest, src, 2);
+ //@ assert \initialized(&dest[0..2]);
+ //@ assert !\initialized(&dest[3]);
+ }
+}
+
int main(int argc, const char **argv) {
char *const_str = "abcd";
char *unalloc_str = malloc(5);
@@ -60,6 +99,7 @@ int main(int argc, const char **argv) {
ABRT(strncat(pd1 + 3, pd1, 5)); // overlapping spaces [abort]
ABRT(strncat(pd4 + 4, pd4, 5)); // overlapping spaces [abort]
}
+ test_memory_tracking();
return 0;
}
diff --git a/src/plugins/e-acsl/tests/builtin/strcpy.c b/src/plugins/e-acsl/tests/builtin/strcpy.c
index ad599900304..4aaa1722b18 100644
--- a/src/plugins/e-acsl/tests/builtin/strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/strcpy.c
@@ -6,6 +6,39 @@
#include <string.h>
#include <stdlib.h>
+void test_memory_tracking() {
+ {
+ char dest[4];
+ char src[] = "b";
+ //@ assert !\initialized(&dest[0..3]);
+ //@ assert \initialized(&src[0..1]);
+
+ strcpy(dest, src);
+ //@ assert \initialized(&dest[0..1]);
+ //@ assert !\initialized(&dest[2..3]);
+ }
+ { // strncpy with n < strlen(src)
+ char dest[4];
+ char src[4] = "ab";
+ //@ assert !\initialized(&dest[0..3]);
+ //@ assert \initialized(&src[0..3]);
+
+ strncpy(dest, src, 1);
+ //@ assert \initialized(&dest[0]);
+ //@ assert !\initialized(&dest[1..3]);
+ }
+ { // strncpy with n >= strlen(src)
+ char dest[4];
+ char src[4] = "b";
+ //@ assert !\initialized(&dest[0..3]);
+ //@ assert \initialized(&src[0..3]);
+
+ strncpy(dest, src, 3);
+ //@ assert \initialized(&dest[0..2]);
+ //@ assert !\initialized(&dest[3]);
+ }
+}
+
int main(int argc, const char **argv) {
char empty_str[1] = "";
char *const_str = "abcd";
@@ -41,5 +74,7 @@ int main(int argc, const char **argv) {
free(src);
free(dest1);
free(dest2);
+
+ test_memory_tracking();
return 0;
}
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index 1e708d06d7d..b5d7a91b2f1 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -703,11 +703,40 @@ pid_t __gen_e_acsl_fork(void)
char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
{
char *__gen_e_acsl_at;
+ unsigned long __gen_e_acsl_strcpy_src_size;
char *__retres;
__e_acsl_store_block((void *)(& src),(size_t)8);
__e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
__gen_e_acsl_at = dest;
__retres = strcpy(dest,src);
+ {
+ __e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_strcpy_src_size;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_le;
+ unsigned long __gen_e_acsl_size;
+ __gmpz_init_set_ui(__gen_e_acsl___gen_e_acsl_strcpy_src_size,
+ __gen_e_acsl_strcpy_src_size);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl___gen_e_acsl_strcpy_src_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_ui(__gen_e_acsl__2,18446744073709551615UL);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __e_acsl_assert(__gen_e_acsl_le <= 0,1,"RTE","strcpy",
+ "size_lesser_or_eq_than_SIZE_MAX:\n __gen_e_acsl_strcpy_src_size + 1 <= 18446744073709551615",
+ "FRAMAC_SHARE/libc/string.h",367);
+ __gen_e_acsl_size = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __e_acsl_initialize((void *)dest,__gen_e_acsl_size);
+ __gmpz_clear(__gen_e_acsl___gen_e_acsl_strcpy_src_size);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl__2);
+ }
__e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","strcpy",
"result_ptr: \\result == \\old(dest)",
"FRAMAC_SHARE/libc/string.h",374);
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_sprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_sprintf.c
new file mode 100644
index 00000000000..503129bceba
--- /dev/null
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_sprintf.c
@@ -0,0 +1,173 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+char *__gen_e_acsl_literal_string;
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+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 = "%d";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("%d"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+ }
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
+ {
+ char buf[4];
+ __e_acsl_store_block((void *)(buf),(size_t)4);
+ {
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_size = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(buf + 1 * 0),
+ (size_t)__gen_e_acsl_if);
+ __e_acsl_assert(! __gen_e_acsl_initialized,1,"Assertion","main",
+ "!\\initialized(&buf[0 .. 3])",
+ "tests/format/sprintf.c",10);
+ }
+ /*@ assert ¬\initialized(&buf[0 .. 3]); */ ;
+ __e_acsl_builtin_sprintf("d",buf,__gen_e_acsl_literal_string,10);
+ {
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
+ int __gen_e_acsl_initialized_2;
+ __gen_e_acsl_size_2 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(buf + 1 * 0),
+ (size_t)__gen_e_acsl_if_2);
+ __e_acsl_assert(__gen_e_acsl_initialized_2,1,"Assertion","main",
+ "\\initialized(&buf[0 .. 2])","tests/format/sprintf.c",
+ 13);
+ }
+ /*@ assert \initialized(&buf[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& buf[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_3,1,"Assertion","main",
+ "!\\initialized(&buf[3])","tests/format/sprintf.c",14);
+ }
+ /*@ assert ¬\initialized(&buf[3]); */ ;
+ __e_acsl_delete_block((void *)(buf));
+ }
+ {
+ char buf_0[4];
+ __e_acsl_store_block((void *)(buf_0),(size_t)4);
+ {
+ int __gen_e_acsl_size_3;
+ int __gen_e_acsl_if_3;
+ int __gen_e_acsl_initialized_4;
+ __gen_e_acsl_size_3 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_3 <= 0) __gen_e_acsl_if_3 = 0;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(buf_0 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_3);
+ __e_acsl_assert(! __gen_e_acsl_initialized_4,1,"Assertion","main",
+ "!\\initialized(&buf_0[0 .. 3])",
+ "tests/format/sprintf.c",18);
+ }
+ /*@ assert ¬\initialized(&buf_0[0 .. 3]); */ ;
+ __e_acsl_builtin_snprintf("d",buf_0,(unsigned long)2,
+ __gen_e_acsl_literal_string,10);
+ {
+ int __gen_e_acsl_size_4;
+ int __gen_e_acsl_if_4;
+ int __gen_e_acsl_initialized_5;
+ __gen_e_acsl_size_4 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_4 <= 0) __gen_e_acsl_if_4 = 0;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(buf_0 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_4);
+ __e_acsl_assert(__gen_e_acsl_initialized_5,1,"Assertion","main",
+ "\\initialized(&buf_0[0 .. 1])",
+ "tests/format/sprintf.c",21);
+ }
+ /*@ assert \initialized(&buf_0[0 .. 1]); */ ;
+ {
+ int __gen_e_acsl_initialized_6;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& buf_0[2]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_6,1,"Assertion","main",
+ "!\\initialized(&buf_0[2])","tests/format/sprintf.c",
+ 22);
+ }
+ /*@ assert ¬\initialized(&buf_0[2]); */ ;
+ {
+ int __gen_e_acsl_initialized_7;
+ __gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(& buf_0[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_7,1,"Assertion","main",
+ "!\\initialized(&buf_0[3])","tests/format/sprintf.c",
+ 23);
+ }
+ /*@ assert ¬\initialized(&buf_0[3]); */ ;
+ __e_acsl_delete_block((void *)(buf_0));
+ }
+ {
+ char buf_1[4];
+ __e_acsl_store_block((void *)(buf_1),(size_t)4);
+ {
+ int __gen_e_acsl_size_5;
+ int __gen_e_acsl_if_5;
+ int __gen_e_acsl_initialized_8;
+ __gen_e_acsl_size_5 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_5 <= 0) __gen_e_acsl_if_5 = 0;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(buf_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_5);
+ __e_acsl_assert(! __gen_e_acsl_initialized_8,1,"Assertion","main",
+ "!\\initialized(&buf_1[0 .. 3])",
+ "tests/format/sprintf.c",27);
+ }
+ /*@ assert ¬\initialized(&buf_1[0 .. 3]); */ ;
+ __e_acsl_builtin_snprintf("d",buf_1,(unsigned long)4,
+ __gen_e_acsl_literal_string,10);
+ {
+ int __gen_e_acsl_size_6;
+ int __gen_e_acsl_if_6;
+ int __gen_e_acsl_initialized_9;
+ __gen_e_acsl_size_6 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_6 <= 0) __gen_e_acsl_if_6 = 0;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
+ __gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)(buf_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_6);
+ __e_acsl_assert(__gen_e_acsl_initialized_9,1,"Assertion","main",
+ "\\initialized(&buf_1[0 .. 2])",
+ "tests/format/sprintf.c",30);
+ }
+ /*@ assert \initialized(&buf_1[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_10;
+ __gen_e_acsl_initialized_10 = __e_acsl_initialized((void *)(& buf_1[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_10,1,"Assertion","main",
+ "!\\initialized(&buf_1[3])","tests/format/sprintf.c",
+ 31);
+ }
+ /*@ assert ¬\initialized(&buf_1[3]); */ ;
+ __e_acsl_delete_block((void *)(buf_1));
+ }
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 8ad5e311180..8ac28fcd5d6 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -14,9 +14,6 @@
[e-acsl] Warning: annotating undefined function `strchr':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `strcpy':
- 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.
diff --git a/src/plugins/e-acsl/tests/format/oracle/sprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/sprintf.res.oracle
new file mode 100644
index 00000000000..fe875c9a1ac
--- /dev/null
+++ b/src/plugins/e-acsl/tests/format/oracle/sprintf.res.oracle
@@ -0,0 +1,20 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[kernel:annot:missing-spec] tests/format/sprintf.c:12: Warning:
+ Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
+[eva:alarm] tests/format/sprintf.c:13: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/format/sprintf.c:14: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[kernel:annot:missing-spec] tests/format/sprintf.c:20: Warning:
+ Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
+[eva:alarm] tests/format/sprintf.c:21: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/format/sprintf.c:22: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/format/sprintf.c:23: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/format/sprintf.c:30: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/format/sprintf.c:31: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log b/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
index 02725ad71ef..2fa4a16bc9b 100644
--- a/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
@@ -29,19 +29,19 @@ TEST 20: OK: Expected execution at tests/format/printf.c:209
TEST 21: OK: Expected execution at tests/format/printf.c:209
TEST 22: OK: Expected execution at tests/format/printf.c:209
TEST 23: OK: Expected execution at tests/format/printf.c:209
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [c]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [c]
TEST 24: OK: Expected signal at tests/format/printf.c:209
TEST 25: OK: Expected execution at tests/format/printf.c:209
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [p]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [p]
TEST 26: OK: Expected signal at tests/format/printf.c:209
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [n]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [n]
TEST 27: OK: Expected signal at tests/format/printf.c:209
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [d]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [d]
TEST 28: OK: Expected signal at tests/format/printf.c:215
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [i]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [i]
TEST 29: OK: Expected signal at tests/format/printf.c:215
TEST 30: OK: Expected execution at tests/format/printf.c:215
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [u]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [u]
TEST 31: OK: Expected signal at tests/format/printf.c:215
TEST 32: OK: Expected execution at tests/format/printf.c:215
TEST 33: OK: Expected execution at tests/format/printf.c:215
@@ -52,13 +52,13 @@ TEST 37: OK: Expected execution at tests/format/printf.c:215
TEST 38: OK: Expected execution at tests/format/printf.c:215
TEST 39: OK: Expected execution at tests/format/printf.c:215
TEST 40: OK: Expected execution at tests/format/printf.c:215
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [c]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [c]
TEST 41: OK: Expected signal at tests/format/printf.c:215
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [s]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [s]
TEST 42: OK: Expected signal at tests/format/printf.c:215
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [p]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [p]
TEST 43: OK: Expected signal at tests/format/printf.c:215
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [n]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [n]
TEST 44: OK: Expected signal at tests/format/printf.c:215
TEST 45: OK: Expected execution at tests/format/printf.c:218
TEST 46: OK: Expected execution at tests/format/printf.c:218
@@ -73,39 +73,39 @@ TEST 54: OK: Expected execution at tests/format/printf.c:218
TEST 55: OK: Expected execution at tests/format/printf.c:218
TEST 56: OK: Expected execution at tests/format/printf.c:218
TEST 57: OK: Expected execution at tests/format/printf.c:218
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [0] to format specifier [c]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [0] to format specifier [c]
TEST 58: OK: Expected signal at tests/format/printf.c:218
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [0] to format specifier [s]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [0] to format specifier [s]
TEST 59: OK: Expected signal at tests/format/printf.c:218
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [0] to format specifier [p]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [0] to format specifier [p]
TEST 60: OK: Expected signal at tests/format/printf.c:218
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [0] to format specifier [n]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [0] to format specifier [n]
TEST 61: OK: Expected signal at tests/format/printf.c:218
TEST 62: OK: Expected execution at tests/format/printf.c:224
TEST 63: OK: Expected execution at tests/format/printf.c:225
Format error: illegal format specifier 'l'
TEST 64: OK: Expected signal at tests/format/printf.c:226
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [f]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [f]
TEST 65: OK: Expected signal at tests/format/printf.c:232
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [F]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [F]
TEST 66: OK: Expected signal at tests/format/printf.c:232
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [e]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [e]
TEST 67: OK: Expected signal at tests/format/printf.c:232
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [E]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [E]
TEST 68: OK: Expected signal at tests/format/printf.c:232
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [g]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [g]
TEST 69: OK: Expected signal at tests/format/printf.c:232
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [G]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [G]
TEST 70: OK: Expected signal at tests/format/printf.c:232
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [a]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [a]
TEST 71: OK: Expected signal at tests/format/printf.c:232
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [A]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [A]
TEST 72: OK: Expected signal at tests/format/printf.c:232
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [c]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [c]
TEST 73: OK: Expected signal at tests/format/printf.c:232
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [s]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [s]
TEST 74: OK: Expected signal at tests/format/printf.c:232
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [p]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [p]
TEST 75: OK: Expected signal at tests/format/printf.c:232
TEST 76: OK: Expected execution at tests/format/printf.c:233
TEST 77: OK: Expected execution at tests/format/printf.c:233
@@ -114,27 +114,27 @@ TEST 79: OK: Expected execution at tests/format/printf.c:234
TEST 80: OK: Expected execution at tests/format/printf.c:235
TEST 81: OK: Expected execution at tests/format/printf.c:235
TEST 82: OK: Expected execution at tests/format/printf.c:235
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [f]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [f]
TEST 83: OK: Expected signal at tests/format/printf.c:238
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [F]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [F]
TEST 84: OK: Expected signal at tests/format/printf.c:238
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [e]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [e]
TEST 85: OK: Expected signal at tests/format/printf.c:238
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [E]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [E]
TEST 86: OK: Expected signal at tests/format/printf.c:238
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [g]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [g]
TEST 87: OK: Expected signal at tests/format/printf.c:238
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [G]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [G]
TEST 88: OK: Expected signal at tests/format/printf.c:238
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [a]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [a]
TEST 89: OK: Expected signal at tests/format/printf.c:238
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [A]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [A]
TEST 90: OK: Expected signal at tests/format/printf.c:238
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [c]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [c]
TEST 91: OK: Expected signal at tests/format/printf.c:238
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [s]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [s]
TEST 92: OK: Expected signal at tests/format/printf.c:238
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [p]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [p]
TEST 93: OK: Expected signal at tests/format/printf.c:238
TEST 94: OK: Expected execution at tests/format/printf.c:239
TEST 95: OK: Expected execution at tests/format/printf.c:239
@@ -143,7 +143,7 @@ TEST 97: OK: Expected execution at tests/format/printf.c:240
TEST 98: OK: Expected execution at tests/format/printf.c:241
TEST 99: OK: Expected execution at tests/format/printf.c:241
TEST 100: OK: Expected execution at tests/format/printf.c:241
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [l] to format specifier [p]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [l] to format specifier [p]
TEST 101: OK: Expected signal at tests/format/printf.c:244
TEST 102: OK: Expected execution at tests/format/printf.c:245
TEST 103: OK: Expected execution at tests/format/printf.c:245
@@ -168,27 +168,27 @@ TEST 121: OK: Expected execution at tests/format/printf.c:262
TEST 122: OK: Expected execution at tests/format/printf.c:263
TEST 123: OK: Expected execution at tests/format/printf.c:263
TEST 124: OK: Expected execution at tests/format/printf.c:263
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [f]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [f]
TEST 125: OK: Expected signal at tests/format/printf.c:266
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [F]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [F]
TEST 126: OK: Expected signal at tests/format/printf.c:266
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [e]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [e]
TEST 127: OK: Expected signal at tests/format/printf.c:266
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [E]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [E]
TEST 128: OK: Expected signal at tests/format/printf.c:266
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [g]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [g]
TEST 129: OK: Expected signal at tests/format/printf.c:266
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [G]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [G]
TEST 130: OK: Expected signal at tests/format/printf.c:266
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [a]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [a]
TEST 131: OK: Expected signal at tests/format/printf.c:266
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [A]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [A]
TEST 132: OK: Expected signal at tests/format/printf.c:266
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [c]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [c]
TEST 133: OK: Expected signal at tests/format/printf.c:266
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [s]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [s]
TEST 134: OK: Expected signal at tests/format/printf.c:266
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [p]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [p]
TEST 135: OK: Expected signal at tests/format/printf.c:266
TEST 136: OK: Expected execution at tests/format/printf.c:267
TEST 137: OK: Expected execution at tests/format/printf.c:267
@@ -197,27 +197,27 @@ TEST 139: OK: Expected execution at tests/format/printf.c:268
TEST 140: OK: Expected execution at tests/format/printf.c:269
TEST 141: OK: Expected execution at tests/format/printf.c:269
TEST 142: OK: Expected execution at tests/format/printf.c:269
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [f]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [f]
TEST 143: OK: Expected signal at tests/format/printf.c:272
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [F]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [F]
TEST 144: OK: Expected signal at tests/format/printf.c:272
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [e]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [e]
TEST 145: OK: Expected signal at tests/format/printf.c:272
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [E]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [E]
TEST 146: OK: Expected signal at tests/format/printf.c:272
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [g]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [g]
TEST 147: OK: Expected signal at tests/format/printf.c:272
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [G]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [G]
TEST 148: OK: Expected signal at tests/format/printf.c:272
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [a]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [a]
TEST 149: OK: Expected signal at tests/format/printf.c:272
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [A]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [A]
TEST 150: OK: Expected signal at tests/format/printf.c:272
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [c]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [c]
TEST 151: OK: Expected signal at tests/format/printf.c:272
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [s]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [s]
TEST 152: OK: Expected signal at tests/format/printf.c:272
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [p]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [p]
TEST 153: OK: Expected signal at tests/format/printf.c:272
TEST 154: OK: Expected execution at tests/format/printf.c:277
TEST 155: OK: Expected execution at tests/format/printf.c:277
@@ -226,27 +226,27 @@ TEST 157: OK: Expected execution at tests/format/printf.c:281
TEST 158: OK: Expected execution at tests/format/printf.c:282
TEST 159: OK: Expected execution at tests/format/printf.c:282
TEST 160: OK: Expected execution at tests/format/printf.c:282
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [f]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [f]
TEST 161: OK: Expected signal at tests/format/printf.c:287
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [F]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [F]
TEST 162: OK: Expected signal at tests/format/printf.c:287
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [e]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [e]
TEST 163: OK: Expected signal at tests/format/printf.c:287
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [E]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [E]
TEST 164: OK: Expected signal at tests/format/printf.c:287
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [g]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [g]
TEST 165: OK: Expected signal at tests/format/printf.c:287
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [G]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [G]
TEST 166: OK: Expected signal at tests/format/printf.c:287
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [a]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [a]
TEST 167: OK: Expected signal at tests/format/printf.c:287
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [A]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [A]
TEST 168: OK: Expected signal at tests/format/printf.c:287
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [c]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [c]
TEST 169: OK: Expected signal at tests/format/printf.c:287
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [s]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [s]
TEST 170: OK: Expected signal at tests/format/printf.c:287
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [p]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [p]
TEST 171: OK: Expected signal at tests/format/printf.c:287
TEST 172: OK: Expected execution at tests/format/printf.c:289
TEST 173: OK: Expected execution at tests/format/printf.c:289
@@ -255,23 +255,23 @@ TEST 175: OK: Expected execution at tests/format/printf.c:290
TEST 176: OK: Expected execution at tests/format/printf.c:295
TEST 177: OK: Expected execution at tests/format/printf.c:295
TEST 178: OK: Expected execution at tests/format/printf.c:296
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [d]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [d]
TEST 179: OK: Expected signal at tests/format/printf.c:299
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [i]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [i]
TEST 180: OK: Expected signal at tests/format/printf.c:299
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [o]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [o]
TEST 181: OK: Expected signal at tests/format/printf.c:299
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [u]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [u]
TEST 182: OK: Expected signal at tests/format/printf.c:299
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [x]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [x]
TEST 183: OK: Expected signal at tests/format/printf.c:299
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [c]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [c]
TEST 184: OK: Expected signal at tests/format/printf.c:299
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [s]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [s]
TEST 185: OK: Expected signal at tests/format/printf.c:299
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [p]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [p]
TEST 186: OK: Expected signal at tests/format/printf.c:299
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [n]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [n]
TEST 187: OK: Expected signal at tests/format/printf.c:299
TEST 188: OK: Expected execution at tests/format/printf.c:300
TEST 189: OK: Expected execution at tests/format/printf.c:300
@@ -550,11 +550,11 @@ printf: directive 1 ('%n') expects argument of type 'int*' but the corresponding
TEST 368: OK: Expected signal at tests/format/printf.c:460
printf: argument 0 of directive %n not allocated or writeable
TEST 369: OK: Expected signal at tests/format/printf.c:461
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag ['] to format specifier [n]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag ['] to format specifier [n]
TEST 370: OK: Expected signal at tests/format/printf.c:464
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [0] to format specifier [n]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [0] to format specifier [n]
TEST 371: OK: Expected signal at tests/format/printf.c:465
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [n]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [n]
TEST 372: OK: Expected signal at tests/format/printf.c:466
Format error: one of more flags with [n] specifier
TEST 373: OK: Expected signal at tests/format/printf.c:467
@@ -562,11 +562,11 @@ Format error: one of more flags with [n] specifier
TEST 374: OK: Expected signal at tests/format/printf.c:468
Format error: one of more flags with [n] specifier
TEST 375: OK: Expected signal at tests/format/printf.c:469
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [n]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [n]
TEST 376: OK: Expected signal at tests/format/printf.c:470
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [n]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [n]
TEST 377: OK: Expected signal at tests/format/printf.c:471
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [n]
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [n]
TEST 378: OK: Expected signal at tests/format/printf.c:472
Format error: field width used with [n] specifier
TEST 379: OK: Expected signal at tests/format/printf.c:473
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/sprintf.e-acsl.err.log b/src/plugins/e-acsl/tests/format/oracle_dev/sprintf.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/format/sprintf.c b/src/plugins/e-acsl/tests/format/sprintf.c
new file mode 100644
index 00000000000..9e821831938
--- /dev/null
+++ b/src/plugins/e-acsl/tests/format/sprintf.c
@@ -0,0 +1,34 @@
+/* run.config_ci,run.config_dev
+ COMMENT: Check memory tracking of sprintf built-ins
+*/
+
+#include <stdio.h>
+
+int main() {
+ {
+ char buf[4];
+ //@ assert !\initialized(&buf[0..3]);
+
+ sprintf(buf, "%d", 10);
+ //@ assert \initialized(&buf[0..2]);
+ //@ assert !\initialized(&buf[3]);
+ }
+ { // snprintf with n < what would be printed
+ char buf[4];
+ //@ assert !\initialized(&buf[0..3]);
+
+ snprintf(buf, 2, "%d", 10);
+ //@ assert \initialized(&buf[0..1]);
+ //@ assert !\initialized(&buf[2]);
+ //@ assert !\initialized(&buf[3]);
+ }
+ { // snprintf with n >= what would be printed
+ char buf[4];
+ //@ assert !\initialized(&buf[0..3]);
+
+ snprintf(buf, 4, "%d", 10);
+ //@ assert \initialized(&buf[0..2]);
+ //@ assert !\initialized(&buf[3]);
+ }
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/libc/file.c b/src/plugins/e-acsl/tests/libc/file.c
new file mode 100644
index 00000000000..6a44a67ff09
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/file.c
@@ -0,0 +1,40 @@
+/* run.config
+ COMMENT: Test non built-in `fread` memory tracking
+*/
+
+#include <stdio.h>
+
+int main() {
+ int buf[6];
+ FILE *f = fopen("/dev/urandom", "r");
+ // we assume this fopen will always succeed,
+ // to ensure the code below is always tested
+ int res = fread(buf+1, sizeof(int), 4, f);
+ //@ assert !\initialized(&buf[0]);
+ if (res == 0) {
+ //@ assert !\initialized(&buf[1]);
+ }
+ if (res >= 1) {
+ //@ assert \initialized(&buf[1]);
+ }
+ if (res >= 2) {
+ //@ assert \initialized(&buf[2]);
+ }
+ if (res >= 3) {
+ //@ assert \initialized(&buf[3]);
+ }
+ if (res >= 4) {
+ //@ assert \initialized(&buf[4]);
+ }
+ //@ assert !\initialized(&buf[5]);
+
+ // intentionally do not read the return value;
+ // but we suppose in this test that it will always succeed
+ // and read 4 elements
+ int buf2[6];
+ fread(buf2+1, sizeof(int), 4, f);
+ //@ assert !\initialized(&buf2[0]);
+ //@ assert \initialized(&buf2[1..4]);
+ //@ assert !\initialized(&buf2[5]);
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/libc/mem.c b/src/plugins/e-acsl/tests/libc/mem.c
new file mode 100644
index 00000000000..a8b038156bb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/mem.c
@@ -0,0 +1,30 @@
+/* run.config
+ COMMENT: Test non built-in `memset`, `memcpy` and `memmove` memory tracking
+*/
+
+#include <string.h>
+
+int main() {
+ char a[2];
+ memset(a, 1, 1);
+ //@assert \initialized(&a[0]);
+ //@assert !\initialized(&a[1]);
+ memset(a+1, 1, 1);
+ //@assert \initialized(&a[1]);
+ int b[5];
+ memset(&b[2], 42, 2*sizeof(b[0]));
+ //@assert !\initialized(&b[0]);
+ //@assert !\initialized(&b[1]);
+ //@assert \initialized(&b[2..3]);
+ //@assert !\initialized(&b[4]);
+
+ char c[4];
+ memcpy(c+1, a, 2);
+ //@assert !\initialized(&c[0]);
+ //@assert \initialized(&c[1..2]);
+ //@assert !\initialized(&c[3]);
+
+ memmove(c, c+1, 2);
+ //@ assert \initialized(&c[0..2]);
+ //@ assert !\initialized(&c[3]);
+}
diff --git a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
new file mode 100644
index 00000000000..12656044ebd
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
@@ -0,0 +1,52 @@
+[e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `fopen':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:350: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:150: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:151: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:149: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:155: Warning:
+ E-ACSL construct `predicate with no definition nor reads clause'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/libc/file.c:12: Warning:
+ function __gen_e_acsl_fread: precondition 'valid_stream' got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:350: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+ function __gen_e_acsl_fread: postcondition 'initialization' got status unknown.
+[eva:alarm] tests/libc/file.c:15: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/libc/file.c:15: Warning: assertion got status unknown.
+[eva:alarm] tests/libc/file.c:18: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/libc/file.c:21: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/libc/file.c:24: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/libc/file.c:27: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/libc/file.c:35: Warning:
+ function __gen_e_acsl_fread: precondition 'valid_stream' got status unknown.
+[eva:alarm] tests/libc/file.c:37: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
new file mode 100644
index 00000000000..c6b6e713f91
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
@@ -0,0 +1,434 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+char *__gen_e_acsl_literal_string;
+char *__gen_e_acsl_literal_string_2;
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+/*@ requires valid_filename: valid_read_string(filename);
+ requires valid_mode: valid_read_string(mode);
+ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename)))),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))), __fc_p_fopen;
+ */
+FILE *__gen_e_acsl_fopen(char const * restrict filename,
+ char const * restrict mode);
+
+/*@ requires valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1));
+ requires valid_stream: \valid(stream);
+ ensures size_read: \result ≤ \old(nmemb);
+ ensures
+ initialization:
+ \initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1));
+ assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream, \result;
+ assigns *((char *)ptr + (0 .. nmemb * size - 1))
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns *stream
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns \result \from size, (indirect: *stream);
+ */
+size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
+ FILE * restrict stream);
+
+/*@ requires valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1));
+ requires valid_stream: \valid(stream);
+ ensures size_read: \result ≤ \old(nmemb);
+ ensures
+ initialization:
+ \initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1));
+ assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream, \result;
+ assigns *((char *)ptr + (0 .. nmemb * size - 1))
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns *stream
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns \result \from size, (indirect: *stream);
+ */
+size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
+ FILE * restrict stream)
+{
+ __e_acsl_mpz_t __gen_e_acsl_at_3;
+ void *__gen_e_acsl_at_2;
+ size_t __gen_e_acsl_at;
+ size_t __retres;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof;
+ __e_acsl_mpz_t __gen_e_acsl_nmemb;
+ __e_acsl_mpz_t __gen_e_acsl_size_2;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_mul_2;
+ int __gen_e_acsl_le;
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_le_2;
+ unsigned long __gen_e_acsl_size_3;
+ int __gen_e_acsl_valid;
+ int __gen_e_acsl_valid_2;
+ __e_acsl_store_block((void *)(& stream),(size_t)8);
+ __e_acsl_store_block((void *)(& ptr),(size_t)8);
+ __gmpz_init_set_si(__gen_e_acsl_sizeof,1L);
+ __gmpz_init_set_ui(__gen_e_acsl_nmemb,nmemb);
+ __gmpz_init_set_ui(__gen_e_acsl_size_2,size);
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_nmemb),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init(__gen_e_acsl_mul_2);
+ __gmpz_mul(__gen_e_acsl_mul_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_init_set(__gen_e_acsl_size,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2));
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ if (__gen_e_acsl_le <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __gmpz_init_set_si(__gen_e_acsl__3,0L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_clear(__gen_e_acsl__3);
+ }
+ else __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gmpz_init_set_ui(__gen_e_acsl__4,18446744073709551615UL);
+ __gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __e_acsl_assert(__gen_e_acsl_le_2 <= 0,1,"RTE","fread",
+ "offset_lesser_or_eq_than_SIZE_MAX:\n (\\let size = sizeof(char) * (((nmemb * size - 1) - 0) + 1);\n size <= 0? 0: size)\n <= 18446744073709551615",
+ "FRAMAC_SHARE/libc/stdio.h",351);
+ __gen_e_acsl_size_3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)((char *)ptr + 1 * 0),
+ __gen_e_acsl_size_3,ptr,
+ (void *)(& ptr));
+ __e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","fread",
+ "valid_ptr_block: \\valid((char *)ptr + (0 .. nmemb * size - 1))",
+ "FRAMAC_SHARE/libc/stdio.h",351);
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stream,sizeof(FILE),
+ (void *)stream,(void *)(& stream));
+ __e_acsl_assert(__gen_e_acsl_valid_2,1,"Precondition","fread",
+ "valid_stream: \\valid(stream)",
+ "FRAMAC_SHARE/libc/stdio.h",352);
+ __gmpz_clear(__gen_e_acsl_size);
+ __gmpz_clear(__gen_e_acsl_sizeof);
+ __gmpz_clear(__gen_e_acsl_nmemb);
+ __gmpz_clear(__gen_e_acsl_size_2);
+ __gmpz_clear(__gen_e_acsl_mul);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_mul_2);
+ __gmpz_clear(__gen_e_acsl_if);
+ __gmpz_clear(__gen_e_acsl__4);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_size_7;
+ __gmpz_init_set_ui(__gen_e_acsl_size_7,size);
+ __gmpz_init_set(__gen_e_acsl_at_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
+ __gmpz_clear(__gen_e_acsl_size_7);
+ }
+ __gen_e_acsl_at_2 = ptr;
+ __gen_e_acsl_at = nmemb;
+ __retres = fread(ptr,size,nmemb,stream);
+ {
+ __e_acsl_mpz_t __gen_e_acsl___retres;
+ __e_acsl_mpz_t __gen_e_acsl_size_4;
+ __e_acsl_mpz_t __gen_e_acsl_mul_3;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ int __gen_e_acsl_le_3;
+ unsigned long __gen_e_acsl_size_5;
+ __gmpz_init_set_ui(__gen_e_acsl___retres,__retres);
+ __gmpz_init_set_ui(__gen_e_acsl_size_4,size);
+ __gmpz_init(__gen_e_acsl_mul_3);
+ __gmpz_mul(__gen_e_acsl_mul_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl___retres),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4));
+ __gmpz_init_set_ui(__gen_e_acsl__5,18446744073709551615UL);
+ __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __e_acsl_assert(__gen_e_acsl_le_3 <= 0,1,"RTE","fread",
+ "size_lesser_or_eq_than_SIZE_MAX: __retres * size <= 18446744073709551615",
+ "FRAMAC_SHARE/libc/stdio.h",350);
+ __gen_e_acsl_size_5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3));
+ __e_acsl_initialize(ptr,__gen_e_acsl_size_5);
+ __gmpz_clear(__gen_e_acsl___retres);
+ __gmpz_clear(__gen_e_acsl_size_4);
+ __gmpz_clear(__gen_e_acsl_mul_3);
+ __gmpz_clear(__gen_e_acsl__5);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_size_6;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof_2;
+ __e_acsl_mpz_t __gen_e_acsl_result;
+ __e_acsl_mpz_t __gen_e_acsl_mul_4;
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl_sub_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl_mul_5;
+ int __gen_e_acsl_le_4;
+ __e_acsl_mpz_t __gen_e_acsl_if_2;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ int __gen_e_acsl_le_5;
+ unsigned long __gen_e_acsl_size_8;
+ int __gen_e_acsl_initialized;
+ __e_acsl_assert(__retres <= __gen_e_acsl_at,1,"Postcondition","fread",
+ "size_read: \\result <= \\old(nmemb)",
+ "FRAMAC_SHARE/libc/stdio.h",356);
+ __gmpz_init_set_si(__gen_e_acsl_sizeof_2,1L);
+ __gmpz_init_set_ui(__gen_e_acsl_result,__retres);
+ __gmpz_init(__gen_e_acsl_mul_4);
+ __gmpz_mul(__gen_e_acsl_mul_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_result),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3));
+ __gmpz_init_set_si(__gen_e_acsl__6,1L);
+ __gmpz_init(__gen_e_acsl_sub_3);
+ __gmpz_sub(__gen_e_acsl_sub_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init_set_si(__gen_e_acsl__7,0L);
+ __gmpz_init(__gen_e_acsl_sub_4);
+ __gmpz_sub(__gen_e_acsl_sub_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init(__gen_e_acsl_mul_5);
+ __gmpz_mul(__gen_e_acsl_mul_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gmpz_init_set(__gen_e_acsl_size_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_5));
+ __gen_e_acsl_le_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ if (__gen_e_acsl_le_4 <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ __gmpz_init_set_si(__gen_e_acsl__8,0L);
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gmpz_clear(__gen_e_acsl__8);
+ }
+ else __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6));
+ __gmpz_init_set_ui(__gen_e_acsl__9,18446744073709551615UL);
+ __gen_e_acsl_le_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __e_acsl_assert(__gen_e_acsl_le_5 <= 0,1,"RTE","fread",
+ "offset_lesser_or_eq_than_SIZE_MAX:\n (\\let size = sizeof(char) * (((\\result * \\old(size) - 1) - 0) + 1);\n size <= 0? 0: size)\n <= 18446744073709551615",
+ "FRAMAC_SHARE/libc/stdio.h",357);
+ __gen_e_acsl_size_8 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at_2 +
+ 1 * 0),
+ __gen_e_acsl_size_8);
+ __e_acsl_assert(__gen_e_acsl_initialized,1,"Postcondition","fread",
+ "initialization:\n \\initialized((char *)\\old(ptr) + (0 .. \\result * \\old(size) - 1))",
+ "FRAMAC_SHARE/libc/stdio.h",357);
+ __e_acsl_delete_block((void *)(& stream));
+ __e_acsl_delete_block((void *)(& ptr));
+ __gmpz_clear(__gen_e_acsl_size_6);
+ __gmpz_clear(__gen_e_acsl_sizeof_2);
+ __gmpz_clear(__gen_e_acsl_result);
+ __gmpz_clear(__gen_e_acsl_mul_4);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_sub_3);
+ __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl_mul_5);
+ __gmpz_clear(__gen_e_acsl_if_2);
+ __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl_at_3);
+ return __retres;
+ }
+}
+
+/*@ requires valid_filename: valid_read_string(filename);
+ requires valid_mode: valid_read_string(mode);
+ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename)))),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))), __fc_p_fopen;
+ */
+FILE *__gen_e_acsl_fopen(char const * restrict filename,
+ char const * restrict mode)
+{
+ FILE *__retres;
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
+ __retres = fopen(filename,mode);
+ __e_acsl_delete_block((void *)(& __retres));
+ return __retres;
+}
+
+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 = "r";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("r"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+ __gen_e_acsl_literal_string_2 = "/dev/urandom";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+ sizeof("/dev/urandom"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
+ }
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int buf[6];
+ size_t tmp_0;
+ int buf2[6];
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
+ __e_acsl_store_block((void *)(buf2),(size_t)24);
+ __e_acsl_store_block((void *)(buf),(size_t)24);
+ FILE *f =
+ __gen_e_acsl_fopen(__gen_e_acsl_literal_string_2,
+ __gen_e_acsl_literal_string);
+ __e_acsl_store_block((void *)(& f),(size_t)8);
+ __e_acsl_full_init((void *)(& f));
+ tmp_0 = __gen_e_acsl_fread((void *)(& buf[1]),sizeof(int),(unsigned long)4,
+ f);
+ int res = (int)tmp_0;
+ {
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(buf),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized,1,"Assertion","main",
+ "!\\initialized((int *)buf)","tests/libc/file.c",13);
+ }
+ /*@ assert ¬\initialized((int *)buf); */ ;
+ if (res == 0) {
+ {
+ int __gen_e_acsl_initialized_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& buf[1]),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_2,1,"Assertion","main",
+ "!\\initialized(&buf[1])","tests/libc/file.c",15);
+ }
+ /*@ assert ¬\initialized(&buf[1]); */ ;
+ }
+ if (res >= 1) {
+ {
+ int __gen_e_acsl_initialized_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& buf[1]),
+ sizeof(int));
+ __e_acsl_assert(__gen_e_acsl_initialized_3,1,"Assertion","main",
+ "\\initialized(&buf[1])","tests/libc/file.c",18);
+ }
+ /*@ assert \initialized(&buf[1]); */ ;
+ }
+ if (res >= 2) {
+ {
+ int __gen_e_acsl_initialized_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& buf[2]),
+ sizeof(int));
+ __e_acsl_assert(__gen_e_acsl_initialized_4,1,"Assertion","main",
+ "\\initialized(&buf[2])","tests/libc/file.c",21);
+ }
+ /*@ assert \initialized(&buf[2]); */ ;
+ }
+ if (res >= 3) {
+ {
+ int __gen_e_acsl_initialized_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& buf[3]),
+ sizeof(int));
+ __e_acsl_assert(__gen_e_acsl_initialized_5,1,"Assertion","main",
+ "\\initialized(&buf[3])","tests/libc/file.c",24);
+ }
+ /*@ assert \initialized(&buf[3]); */ ;
+ }
+ if (res >= 4) {
+ {
+ int __gen_e_acsl_initialized_6;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& buf[4]),
+ sizeof(int));
+ __e_acsl_assert(__gen_e_acsl_initialized_6,1,"Assertion","main",
+ "\\initialized(&buf[4])","tests/libc/file.c",27);
+ }
+ /*@ assert \initialized(&buf[4]); */ ;
+ }
+ {
+ int __gen_e_acsl_initialized_7;
+ __gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(& buf[5]),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_7,1,"Assertion","main",
+ "!\\initialized(&buf[5])","tests/libc/file.c",29);
+ }
+ /*@ assert ¬\initialized(&buf[5]); */ ;
+ __gen_e_acsl_fread((void *)(& buf2[1]),sizeof(int),(unsigned long)4,f);
+ {
+ int __gen_e_acsl_initialized_8;
+ __gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(buf2),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_8,1,"Assertion","main",
+ "!\\initialized((int *)buf2)","tests/libc/file.c",36);
+ }
+ /*@ assert ¬\initialized((int *)buf2); */ ;
+ {
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_initialized_9;
+ __gen_e_acsl_size = 4 * ((4 - 1) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)((char *)(buf2) +
+ 4 * 1),
+ (size_t)__gen_e_acsl_if);
+ __e_acsl_assert(__gen_e_acsl_initialized_9,1,"Assertion","main",
+ "\\initialized(&buf2[1 .. 4])","tests/libc/file.c",37);
+ }
+ /*@ assert \initialized(&buf2[1 .. 4]); */ ;
+ {
+ int __gen_e_acsl_initialized_10;
+ __gen_e_acsl_initialized_10 = __e_acsl_initialized((void *)(& buf2[5]),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_10,1,"Assertion","main",
+ "!\\initialized(&buf2[5])","tests/libc/file.c",38);
+ }
+ /*@ assert ¬\initialized(&buf2[5]); */ ;
+ __retres = 0;
+ __e_acsl_delete_block((void *)(buf2));
+ __e_acsl_delete_block((void *)(& f));
+ __e_acsl_delete_block((void *)(buf));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
new file mode 100644
index 00000000000..2416c3eb591
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
@@ -0,0 +1,351 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+#include "string.h"
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+/*@ requires valid_dest: valid_or_empty(dest, n);
+ requires valid_src: valid_read_or_empty(src, n);
+ requires
+ separation:
+ \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+ ensures
+ copied_contents:
+ memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *((char *)dest + (0 .. n - 1)), \result;
+ assigns *((char *)dest + (0 .. n - 1))
+ \from *((char *)src + (0 .. n - 1));
+ assigns \result \from dest;
+ */
+void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
+ size_t n);
+
+/*@ requires valid_dest: valid_or_empty(dest, n);
+ requires valid_src: valid_read_or_empty(src, n);
+ ensures
+ copied_contents:
+ memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *((char *)dest + (0 .. n - 1)), \result;
+ assigns *((char *)dest + (0 .. n - 1))
+ \from *((char *)src + (0 .. n - 1));
+ assigns \result \from dest;
+ */
+void *__gen_e_acsl_memmove(void *dest, void const *src, size_t n);
+
+/*@ requires valid_s: valid_or_empty(s, n);
+ ensures
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
+ ensures result_ptr: \result ≡ \old(s);
+ assigns *((char *)s + (0 .. n - 1)), \result;
+ assigns *((char *)s + (0 .. n - 1)) \from c;
+ assigns \result \from s;
+ */
+void *__gen_e_acsl_memset(void *s, int c, size_t n);
+
+int main(void)
+{
+ int __retres;
+ char a[2];
+ int b[5];
+ char c[4];
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(c),(size_t)4);
+ __e_acsl_store_block((void *)(b),(size_t)20);
+ __e_acsl_store_block((void *)(a),(size_t)2);
+ __gen_e_acsl_memset((void *)(a),1,(unsigned long)1);
+ {
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(a),sizeof(char));
+ __e_acsl_assert(__gen_e_acsl_initialized,1,"Assertion","main",
+ "\\initialized((char *)a)","tests/libc/mem.c",10);
+ }
+ /*@ assert \initialized((char *)a); */ ;
+ {
+ int __gen_e_acsl_initialized_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& a[1]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_2,1,"Assertion","main",
+ "!\\initialized(&a[1])","tests/libc/mem.c",11);
+ }
+ /*@ assert ¬\initialized(&a[1]); */ ;
+ __gen_e_acsl_memset((void *)(& a[1]),1,(unsigned long)1);
+ {
+ int __gen_e_acsl_initialized_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& a[1]),
+ sizeof(char));
+ __e_acsl_assert(__gen_e_acsl_initialized_3,1,"Assertion","main",
+ "\\initialized(&a[1])","tests/libc/mem.c",13);
+ }
+ /*@ assert \initialized(&a[1]); */ ;
+ __gen_e_acsl_memset((void *)(& b[2]),42,(unsigned long)2 * sizeof(b[0]));
+ {
+ int __gen_e_acsl_initialized_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(b),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_4,1,"Assertion","main",
+ "!\\initialized((int *)b)","tests/libc/mem.c",16);
+ }
+ /*@ assert ¬\initialized((int *)b); */ ;
+ {
+ int __gen_e_acsl_initialized_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& b[1]),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_5,1,"Assertion","main",
+ "!\\initialized(&b[1])","tests/libc/mem.c",17);
+ }
+ /*@ assert ¬\initialized(&b[1]); */ ;
+ {
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_initialized_6;
+ __gen_e_acsl_size = 4 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)((char *)(b) +
+ 4 * 2),
+ (size_t)__gen_e_acsl_if);
+ __e_acsl_assert(__gen_e_acsl_initialized_6,1,"Assertion","main",
+ "\\initialized(&b[2 .. 3])","tests/libc/mem.c",18);
+ }
+ /*@ assert \initialized(&b[2 .. 3]); */ ;
+ {
+ int __gen_e_acsl_initialized_7;
+ __gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(& b[4]),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_7,1,"Assertion","main",
+ "!\\initialized(&b[4])","tests/libc/mem.c",19);
+ }
+ /*@ assert ¬\initialized(&b[4]); */ ;
+ __gen_e_acsl_memcpy((void *)(& c[1]),(void const *)(a),(unsigned long)2);
+ {
+ int __gen_e_acsl_initialized_8;
+ __gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(c),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_8,1,"Assertion","main",
+ "!\\initialized((char *)c)","tests/libc/mem.c",23);
+ }
+ /*@ assert ¬\initialized((char *)c); */ ;
+ {
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
+ int __gen_e_acsl_initialized_9;
+ __gen_e_acsl_size_2 = 1 * ((2 - 1) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)(c + 1 * 1),
+ (size_t)__gen_e_acsl_if_2);
+ __e_acsl_assert(__gen_e_acsl_initialized_9,1,"Assertion","main",
+ "\\initialized(&c[1 .. 2])","tests/libc/mem.c",24);
+ }
+ /*@ assert \initialized(&c[1 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_10;
+ __gen_e_acsl_initialized_10 = __e_acsl_initialized((void *)(& c[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_10,1,"Assertion","main",
+ "!\\initialized(&c[3])","tests/libc/mem.c",25);
+ }
+ /*@ assert ¬\initialized(&c[3]); */ ;
+ __gen_e_acsl_memmove((void *)(c),(void const *)(& c[1]),(unsigned long)2);
+ {
+ int __gen_e_acsl_size_3;
+ int __gen_e_acsl_if_3;
+ int __gen_e_acsl_initialized_11;
+ __gen_e_acsl_size_3 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_3 <= 0) __gen_e_acsl_if_3 = 0;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl_initialized_11 = __e_acsl_initialized((void *)(c + 1 * 0),
+ (size_t)__gen_e_acsl_if_3);
+ __e_acsl_assert(__gen_e_acsl_initialized_11,1,"Assertion","main",
+ "\\initialized(&c[0 .. 2])","tests/libc/mem.c",28);
+ }
+ /*@ assert \initialized(&c[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_12;
+ __gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& c[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_12,1,"Assertion","main",
+ "!\\initialized(&c[3])","tests/libc/mem.c",29);
+ }
+ /*@ assert ¬\initialized(&c[3]); */ ;
+ __retres = 0;
+ __e_acsl_delete_block((void *)(c));
+ __e_acsl_delete_block((void *)(b));
+ __e_acsl_delete_block((void *)(a));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+/*@ requires valid_s: valid_or_empty(s, n);
+ ensures
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
+ ensures result_ptr: \result ≡ \old(s);
+ assigns *((char *)s + (0 .. n - 1)), \result;
+ assigns *((char *)s + (0 .. n - 1)) \from c;
+ assigns \result \from s;
+ */
+void *__gen_e_acsl_memset(void *s, int c, size_t n)
+{
+ void *__gen_e_acsl_at;
+ void *__retres;
+ __e_acsl_store_block((void *)(& s),(size_t)8);
+ __gen_e_acsl_at = s;
+ __retres = memset(s,c,n);
+ __e_acsl_initialize(s,n);
+ __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","memset",
+ "result_ptr: \\result == \\old(s)",
+ "FRAMAC_SHARE/libc/string.h",135);
+ __e_acsl_delete_block((void *)(& s));
+ return __retres;
+}
+
+/*@ requires valid_dest: valid_or_empty(dest, n);
+ requires valid_src: valid_read_or_empty(src, n);
+ ensures
+ copied_contents:
+ memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *((char *)dest + (0 .. n - 1)), \result;
+ assigns *((char *)dest + (0 .. n - 1))
+ \from *((char *)src + (0 .. n - 1));
+ assigns \result \from dest;
+ */
+void *__gen_e_acsl_memmove(void *dest, void const *src, size_t n)
+{
+ void *__gen_e_acsl_at;
+ void *__retres;
+ __e_acsl_store_block((void *)(& src),(size_t)8);
+ __e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gen_e_acsl_at = dest;
+ __retres = memmove(dest,src,n);
+ __e_acsl_initialize(dest,n);
+ __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","memmove",
+ "result_ptr: \\result == \\old(dest)",
+ "FRAMAC_SHARE/libc/string.h",125);
+ __e_acsl_delete_block((void *)(& src));
+ __e_acsl_delete_block((void *)(& dest));
+ return __retres;
+}
+
+/*@ requires valid_dest: valid_or_empty(dest, n);
+ requires valid_src: valid_read_or_empty(src, n);
+ requires
+ separation:
+ \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+ ensures
+ copied_contents:
+ memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *((char *)dest + (0 .. n - 1)), \result;
+ assigns *((char *)dest + (0 .. n - 1))
+ \from *((char *)src + (0 .. n - 1));
+ assigns \result \from dest;
+ */
+void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
+ size_t n)
+{
+ void *__gen_e_acsl_at;
+ void *__retres;
+ {
+ unsigned long __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ unsigned long __gen_e_acsl__3;
+ unsigned long __gen_e_acsl_if;
+ int __gen_e_acsl_valid_read;
+ unsigned long __gen_e_acsl_size_2;
+ unsigned long __gen_e_acsl__4;
+ unsigned long __gen_e_acsl_if_2;
+ int __gen_e_acsl_valid_read_2;
+ unsigned long __gen_e_acsl_size_3;
+ unsigned long __gen_e_acsl__5;
+ unsigned long __gen_e_acsl_if_3;
+ unsigned long __gen_e_acsl_size_4;
+ unsigned long __gen_e_acsl__6;
+ unsigned long __gen_e_acsl_if_4;
+ int __gen_e_acsl_separated;
+ __e_acsl_store_block((void *)(& src),(size_t)8);
+ __e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size = 1UL * __gen_e_acsl__3;
+ if (__gen_e_acsl_size <= 0UL) __gen_e_acsl_if = 0UL;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)dest +
+ 1 * 0),
+ __gen_e_acsl_if,dest,
+ (void *)(& dest));
+ __e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","memcpy",
+ "separated_guard: \\valid_read((char *)dest + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",98);
+ __gen_e_acsl__4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_2 = 1UL * __gen_e_acsl__4;
+ if (__gen_e_acsl_size_2 <= 0UL) __gen_e_acsl_if_2 = 0UL;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)((char *)src +
+ 1 * 0),
+ __gen_e_acsl_if_2,
+ (void *)src,
+ (void *)(& src));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","memcpy",
+ "separated_guard: \\valid_read((char *)src + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",98);
+ __gen_e_acsl__5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_3 = 1UL * __gen_e_acsl__5;
+ if (__gen_e_acsl_size_3 <= 0UL) __gen_e_acsl_if_3 = 0UL;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_4 = 1UL * __gen_e_acsl__6;
+ if (__gen_e_acsl_size_4 <= 0UL) __gen_e_acsl_if_4 = 0UL;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl_separated = __e_acsl_separated((size_t)2,
+ (char *)dest + 1 * 0,
+ __gen_e_acsl_if_3,
+ (char *)src + 1 * 0,
+ __gen_e_acsl_if_4);
+ __e_acsl_assert(__gen_e_acsl_separated,1,"Precondition","memcpy",
+ "separation:\n \\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",98);
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ __gen_e_acsl_at = dest;
+ __retres = memcpy(dest,src,n);
+ __e_acsl_initialize(dest,n);
+ __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","memcpy",
+ "result_ptr: \\result == \\old(dest)",
+ "FRAMAC_SHARE/libc/string.h",102);
+ __e_acsl_delete_block((void *)(& src));
+ __e_acsl_delete_block((void *)(& dest));
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_sprintf.c b/src/plugins/e-acsl/tests/libc/oracle/gen_sprintf.c
new file mode 100644
index 00000000000..4686cea0c6b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_sprintf.c
@@ -0,0 +1,186 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+char *__gen_e_acsl_literal_string;
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+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 = "%d";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("%d"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+ }
+ return;
+}
+
+int main(void)
+{
+ int __gen_e_acsl_snprintf_res_2;
+ int __gen_e_acsl_snprintf_res;
+ int __gen_e_acsl_sprintf_res;
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
+ {
+ char buf[4];
+ __e_acsl_store_block((void *)(buf),(size_t)4);
+ {
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_size = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(buf + 1 * 0),
+ (size_t)__gen_e_acsl_if);
+ __e_acsl_assert(! __gen_e_acsl_initialized,1,"Assertion","main",
+ "!\\initialized(&buf[0 .. 3])","tests/libc/sprintf.c",
+ 10);
+ }
+ /*@ assert ¬\initialized(&buf[0 .. 3]); */ ;
+ __gen_e_acsl_sprintf_res = sprintf(buf,__gen_e_acsl_literal_string,10); /* sprintf_va_1 */
+ if (__gen_e_acsl_sprintf_res >= 0) __e_acsl_initialize((void *)(buf),
+ (size_t)(__gen_e_acsl_sprintf_res + 1L));
+ {
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
+ int __gen_e_acsl_initialized_2;
+ __gen_e_acsl_size_2 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(buf + 1 * 0),
+ (size_t)__gen_e_acsl_if_2);
+ __e_acsl_assert(__gen_e_acsl_initialized_2,1,"Assertion","main",
+ "\\initialized(&buf[0 .. 2])","tests/libc/sprintf.c",
+ 13);
+ }
+ /*@ assert \initialized(&buf[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& buf[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_3,1,"Assertion","main",
+ "!\\initialized(&buf[3])","tests/libc/sprintf.c",14);
+ }
+ /*@ assert ¬\initialized(&buf[3]); */ ;
+ __e_acsl_delete_block((void *)(buf));
+ }
+ {
+ char buf_0[4];
+ __e_acsl_store_block((void *)(buf_0),(size_t)4);
+ {
+ int __gen_e_acsl_size_3;
+ int __gen_e_acsl_if_3;
+ int __gen_e_acsl_initialized_4;
+ __gen_e_acsl_size_3 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_3 <= 0) __gen_e_acsl_if_3 = 0;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(buf_0 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_3);
+ __e_acsl_assert(! __gen_e_acsl_initialized_4,1,"Assertion","main",
+ "!\\initialized(&buf_0[0 .. 3])",
+ "tests/libc/sprintf.c",18);
+ }
+ /*@ assert ¬\initialized(&buf_0[0 .. 3]); */ ;
+ __gen_e_acsl_snprintf_res = snprintf(buf_0,(unsigned long)2,
+ __gen_e_acsl_literal_string,10); /* snprintf_va_1 */
+ if (__gen_e_acsl_snprintf_res >= 0) {
+ unsigned long __gen_e_acsl_n;
+ if (2UL <= (unsigned long)__gen_e_acsl_snprintf_res) __gen_e_acsl_n = (unsigned long)2;
+ else __gen_e_acsl_n = __gen_e_acsl_snprintf_res + 1L;
+ __e_acsl_initialize((void *)(buf_0),__gen_e_acsl_n);
+ }
+ {
+ int __gen_e_acsl_size_4;
+ int __gen_e_acsl_if_4;
+ int __gen_e_acsl_initialized_5;
+ __gen_e_acsl_size_4 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_4 <= 0) __gen_e_acsl_if_4 = 0;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(buf_0 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_4);
+ __e_acsl_assert(__gen_e_acsl_initialized_5,1,"Assertion","main",
+ "\\initialized(&buf_0[0 .. 1])","tests/libc/sprintf.c",
+ 21);
+ }
+ /*@ assert \initialized(&buf_0[0 .. 1]); */ ;
+ {
+ int __gen_e_acsl_size_5;
+ int __gen_e_acsl_if_5;
+ int __gen_e_acsl_initialized_6;
+ __gen_e_acsl_size_5 = 1 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size_5 <= 0) __gen_e_acsl_if_5 = 0;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(buf_0 +
+ 1 * 2),
+ (size_t)__gen_e_acsl_if_5);
+ __e_acsl_assert(! __gen_e_acsl_initialized_6,1,"Assertion","main",
+ "!\\initialized(&buf_0[2 .. 3])",
+ "tests/libc/sprintf.c",22);
+ }
+ /*@ assert ¬\initialized(&buf_0[2 .. 3]); */ ;
+ __e_acsl_delete_block((void *)(buf_0));
+ }
+ {
+ char buf_1[4];
+ __e_acsl_store_block((void *)(buf_1),(size_t)4);
+ {
+ int __gen_e_acsl_size_6;
+ int __gen_e_acsl_if_6;
+ int __gen_e_acsl_initialized_7;
+ __gen_e_acsl_size_6 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_6 <= 0) __gen_e_acsl_if_6 = 0;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
+ __gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(buf_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_6);
+ __e_acsl_assert(! __gen_e_acsl_initialized_7,1,"Assertion","main",
+ "!\\initialized(&buf_1[0 .. 3])",
+ "tests/libc/sprintf.c",26);
+ }
+ /*@ assert ¬\initialized(&buf_1[0 .. 3]); */ ;
+ __gen_e_acsl_snprintf_res_2 = snprintf(buf_1,(unsigned long)4,
+ __gen_e_acsl_literal_string,10); /* snprintf_va_2 */
+ if (__gen_e_acsl_snprintf_res_2 >= 0) {
+ unsigned long __gen_e_acsl_n_2;
+ if (4UL <= (unsigned long)__gen_e_acsl_snprintf_res_2) __gen_e_acsl_n_2 = (unsigned long)4;
+ else __gen_e_acsl_n_2 = __gen_e_acsl_snprintf_res_2 + 1L;
+ __e_acsl_initialize((void *)(buf_1),__gen_e_acsl_n_2);
+ }
+ {
+ int __gen_e_acsl_size_7;
+ int __gen_e_acsl_if_7;
+ int __gen_e_acsl_initialized_8;
+ __gen_e_acsl_size_7 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_7 <= 0) __gen_e_acsl_if_7 = 0;
+ else __gen_e_acsl_if_7 = __gen_e_acsl_size_7;
+ __gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(buf_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_7);
+ __e_acsl_assert(__gen_e_acsl_initialized_8,1,"Assertion","main",
+ "\\initialized(&buf_1[0 .. 2])","tests/libc/sprintf.c",
+ 29);
+ }
+ /*@ assert \initialized(&buf_1[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_9;
+ __gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)(& buf_1[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_9,1,"Assertion","main",
+ "!\\initialized(&buf_1[3])","tests/libc/sprintf.c",30);
+ }
+ /*@ assert ¬\initialized(&buf_1[3]); */ ;
+ __e_acsl_delete_block((void *)(buf_1));
+ }
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
new file mode 100644
index 00000000000..ce223677a59
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
@@ -0,0 +1,959 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+#include "string.h"
+char *__gen_e_acsl_literal_string;
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+/*@ requires valid_string_src: valid_read_string(src);
+ requires room_string: \valid(dest + (0 .. strlen(src)));
+ requires
+ separation:
+ \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
+ ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest + (0 .. strlen{Old}(src))), \result;
+ assigns *(dest + (0 .. strlen{Old}(src)))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+ */
+char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src);
+
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
+ requires room_nstring: \valid(dest + (0 .. n - 1));
+ requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
+ ensures result_ptr: \result ≡ \old(dest);
+ ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
+ assigns *(dest + (0 .. n - 1)), \result;
+ assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
+ assigns \result \from dest;
+
+ behavior complete:
+ assumes src_fits: strlen(src) < n;
+ ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
+
+ behavior partial:
+ assumes src_too_long: n ≤ strlen(src);
+ ensures
+ equal_prefix:
+ memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
+ */
+char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
+ size_t n);
+
+/*@ requires valid_string_src: valid_read_string(src);
+ requires valid_string_dest: valid_string(dest);
+ requires room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)));
+ ensures
+ sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
+ ensures
+ initialization: dest:
+ \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
+ ensures
+ dest_null_terminated:
+ *(\old(dest) + \old(strlen(dest) + strlen(src))) ≡ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest +
+ (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
+ \result;
+ assigns
+ *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+ */
+char *__gen_e_acsl_strcat(char * restrict dest, char const * restrict src);
+
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
+ requires valid_string_dest: valid_string(dest);
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)), \result;
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
+ \from *(src + (0 .. n));
+ assigns \result \from dest;
+
+ behavior complete:
+ assumes
+ valid_string_src_fits: valid_read_string(src) ∧ strlen(src) ≤ n;
+ requires
+ room_string: \valid((dest + strlen(dest)) + (0 .. strlen(src)));
+ ensures
+ sum_of_lengths:
+ strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
+ assigns *(dest +
+ (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
+ \result;
+ assigns
+ *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+
+ behavior partial:
+ assumes
+ valid_string_src_too_large:
+ ¬(valid_read_string(src) ∧ strlen(src) ≤ n);
+ requires room_string: \valid((dest + strlen(dest)) + (0 .. n));
+ ensures
+ sum_of_bounded_lengths:
+ strlen(\old(dest)) ≡ \old(strlen(dest)) + \old(n);
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)),
+ \result;
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+ */
+char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
+ size_t n);
+
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
+ requires valid_string_dest: valid_string(dest);
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)), \result;
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
+ \from *(src + (0 .. n));
+ assigns \result \from dest;
+
+ behavior complete:
+ assumes
+ valid_string_src_fits: valid_read_string(src) ∧ strlen(src) ≤ n;
+ requires
+ room_string: \valid((dest + strlen(dest)) + (0 .. strlen(src)));
+ ensures
+ sum_of_lengths:
+ strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
+ assigns *(dest +
+ (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
+ \result;
+ assigns
+ *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+
+ behavior partial:
+ assumes
+ valid_string_src_too_large:
+ ¬(valid_read_string(src) ∧ strlen(src) ≤ n);
+ requires room_string: \valid((dest + strlen(dest)) + (0 .. n));
+ ensures
+ sum_of_bounded_lengths:
+ strlen(\old(dest)) ≡ \old(strlen(dest)) + \old(n);
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)),
+ \result;
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+ */
+char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
+ size_t n)
+{
+ char *__gen_e_acsl_at;
+ unsigned long __gen_e_acsl_strcat_dest_size;
+ unsigned long __gen_e_acsl_strcat_src_size;
+ __e_acsl_contract_t *__gen_e_acsl_contract;
+ char *__retres;
+ __e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
+ __gen_e_acsl_strcat_src_size = __e_acsl_builtin_strlen(src);
+ if (n < __gen_e_acsl_strcat_src_size) __gen_e_acsl_strcat_src_size = n;
+ __gen_e_acsl_strcat_dest_size = __e_acsl_builtin_strlen((char const *)dest);
+ __gen_e_acsl_at = dest;
+ __retres = strncat(dest,src,n);
+ {
+ __e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_strcat_src_size;
+ __e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_strcat_dest_size;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_le;
+ unsigned long __gen_e_acsl_size;
+ __gmpz_init_set_ui(__gen_e_acsl___gen_e_acsl_strcat_src_size,
+ __gen_e_acsl_strcat_src_size);
+ __gmpz_init_set_ui(__gen_e_acsl___gen_e_acsl_strcat_dest_size,
+ __gen_e_acsl_strcat_dest_size);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl___gen_e_acsl_strcat_src_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl___gen_e_acsl_strcat_dest_size));
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_ui(__gen_e_acsl__2,18446744073709551615UL);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __e_acsl_assert(__gen_e_acsl_le <= 0,1,"RTE","strncat",
+ "size_lesser_or_eq_than_SIZE_MAX:\n (__gen_e_acsl_strcat_src_size + __gen_e_acsl_strcat_dest_size) + 1 <=\n 18446744073709551615",
+ "FRAMAC_SHARE/libc/string.h",438);
+ __gen_e_acsl_size = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __e_acsl_initialize((void *)dest,__gen_e_acsl_size);
+ __gmpz_clear(__gen_e_acsl___gen_e_acsl_strcat_src_size);
+ __gmpz_clear(__gen_e_acsl___gen_e_acsl_strcat_dest_size);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl__2);
+ }
+ __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","strncat",
+ "result_ptr: \\result == \\old(dest)",
+ "FRAMAC_SHARE/libc/string.h",443);
+ __e_acsl_contract_clean(__gen_e_acsl_contract);
+ __e_acsl_delete_block((void *)(& dest));
+ return __retres;
+}
+
+/*@ requires valid_string_src: valid_read_string(src);
+ requires valid_string_dest: valid_string(dest);
+ requires room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)));
+ ensures
+ sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
+ ensures
+ initialization: dest:
+ \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
+ ensures
+ dest_null_terminated:
+ *(\old(dest) + \old(strlen(dest) + strlen(src))) ≡ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest +
+ (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
+ \result;
+ assigns
+ *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+ */
+char *__gen_e_acsl_strcat(char * restrict dest, char const * restrict src)
+{
+ char *__gen_e_acsl_at;
+ unsigned long __gen_e_acsl_strcat_dest_size;
+ unsigned long __gen_e_acsl_strcat_src_size;
+ char *__retres;
+ __e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gen_e_acsl_strcat_src_size = __e_acsl_builtin_strlen(src);
+ __gen_e_acsl_strcat_dest_size = __e_acsl_builtin_strlen((char const *)dest);
+ __gen_e_acsl_at = dest;
+ __retres = strcat(dest,src);
+ {
+ __e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_strcat_src_size;
+ __e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_strcat_dest_size;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_le;
+ unsigned long __gen_e_acsl_size;
+ __gmpz_init_set_ui(__gen_e_acsl___gen_e_acsl_strcat_src_size,
+ __gen_e_acsl_strcat_src_size);
+ __gmpz_init_set_ui(__gen_e_acsl___gen_e_acsl_strcat_dest_size,
+ __gen_e_acsl_strcat_dest_size);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl___gen_e_acsl_strcat_src_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl___gen_e_acsl_strcat_dest_size));
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_ui(__gen_e_acsl__2,18446744073709551615UL);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __e_acsl_assert(__gen_e_acsl_le <= 0,1,"RTE","strcat",
+ "size_lesser_or_eq_than_SIZE_MAX:\n (__gen_e_acsl_strcat_src_size + __gen_e_acsl_strcat_dest_size) + 1 <=\n 18446744073709551615",
+ "FRAMAC_SHARE/libc/string.h",423);
+ __gen_e_acsl_size = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __e_acsl_initialize((void *)dest,__gen_e_acsl_size);
+ __gmpz_clear(__gen_e_acsl___gen_e_acsl_strcat_src_size);
+ __gmpz_clear(__gen_e_acsl___gen_e_acsl_strcat_dest_size);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl__2);
+ }
+ __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","strcat",
+ "result_ptr: \\result == \\old(dest)",
+ "FRAMAC_SHARE/libc/string.h",434);
+ __e_acsl_delete_block((void *)(& dest));
+ return __retres;
+}
+
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
+ requires room_nstring: \valid(dest + (0 .. n - 1));
+ requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
+ ensures result_ptr: \result ≡ \old(dest);
+ ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
+ assigns *(dest + (0 .. n - 1)), \result;
+ assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
+ assigns \result \from dest;
+
+ behavior complete:
+ assumes src_fits: strlen(src) < n;
+ ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
+
+ behavior partial:
+ assumes src_too_long: n ≤ strlen(src);
+ ensures
+ equal_prefix:
+ memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
+ */
+char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
+ size_t n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_at_3;
+ char *__gen_e_acsl_at_2;
+ char *__gen_e_acsl_at;
+ __e_acsl_contract_t *__gen_e_acsl_contract;
+ char *__retres;
+ {
+ unsigned long __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ unsigned long __gen_e_acsl__3;
+ unsigned long __gen_e_acsl_if;
+ int __gen_e_acsl_valid;
+ unsigned long __gen_e_acsl_size_2;
+ unsigned long __gen_e_acsl__4;
+ unsigned long __gen_e_acsl_if_2;
+ int __gen_e_acsl_valid_read;
+ unsigned long __gen_e_acsl_size_3;
+ unsigned long __gen_e_acsl__5;
+ unsigned long __gen_e_acsl_if_3;
+ int __gen_e_acsl_valid_read_2;
+ unsigned long __gen_e_acsl_size_4;
+ unsigned long __gen_e_acsl__6;
+ unsigned long __gen_e_acsl_if_4;
+ unsigned long __gen_e_acsl_size_5;
+ unsigned long __gen_e_acsl__7;
+ unsigned long __gen_e_acsl_if_5;
+ int __gen_e_acsl_separated;
+ __e_acsl_store_block((void *)(& src),(size_t)8);
+ __e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
+ __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size = 1UL * __gen_e_acsl__3;
+ if (__gen_e_acsl_size <= 0UL) __gen_e_acsl_if = 0UL;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(dest + 1 * 0),
+ __gen_e_acsl_if,(void *)dest,
+ (void *)(& dest));
+ __e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","strncpy",
+ "room_nstring: \\valid(dest + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",380);
+ __gen_e_acsl__4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_2 = 1UL * __gen_e_acsl__4;
+ if (__gen_e_acsl_size_2 <= 0UL) __gen_e_acsl_if_2 = 0UL;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(dest + 1 * 0),
+ __gen_e_acsl_if_2,
+ (void *)dest,
+ (void *)(& dest));
+ __e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","strncpy",
+ "separated_guard: \\valid_read(dest + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",382);
+ __gen_e_acsl__5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_3 = 1UL * __gen_e_acsl__5;
+ if (__gen_e_acsl_size_3 <= 0UL) __gen_e_acsl_if_3 = 0UL;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(src + 1 * 0),
+ __gen_e_acsl_if_3,
+ (void *)src,
+ (void *)(& src));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","strncpy",
+ "separated_guard: \\valid_read(src + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",382);
+ __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_4 = 1UL * __gen_e_acsl__6;
+ if (__gen_e_acsl_size_4 <= 0UL) __gen_e_acsl_if_4 = 0UL;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl__7 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_5 = 1UL * __gen_e_acsl__7;
+ if (__gen_e_acsl_size_5 <= 0UL) __gen_e_acsl_if_5 = 0UL;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl_separated = __e_acsl_separated((size_t)2,dest + 1 * 0,
+ __gen_e_acsl_if_4,
+ src + 1 * 0,
+ __gen_e_acsl_if_5);
+ __e_acsl_assert(__gen_e_acsl_separated,1,"Precondition","strncpy",
+ "separation: \\separated(dest + (0 .. n - 1), src + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",382);
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __gmpz_init_set_ui(__gen_e_acsl_n_2,n);
+ __gmpz_init_set(__gen_e_acsl_at_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
+ __gmpz_clear(__gen_e_acsl_n_2);
+ }
+ __gen_e_acsl_at_2 = dest;
+ __gen_e_acsl_at = dest;
+ __retres = strncpy(dest,src,n);
+ __e_acsl_initialize((void *)dest,n);
+ {
+ unsigned long __gen_e_acsl_size_6;
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl_sub_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ unsigned long __gen_e_acsl__10;
+ unsigned long __gen_e_acsl_if_6;
+ int __gen_e_acsl_initialized;
+ __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","strncpy",
+ "result_ptr: \\result == \\old(dest)",
+ "FRAMAC_SHARE/libc/string.h",385);
+ __gmpz_init_set_si(__gen_e_acsl__8,1L);
+ __gmpz_init(__gen_e_acsl_sub_3);
+ __gmpz_sub(__gen_e_acsl_sub_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gmpz_init_set_si(__gen_e_acsl__9,0L);
+ __gmpz_init(__gen_e_acsl_sub_4);
+ __gmpz_sub(__gen_e_acsl_sub_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gen_e_acsl__10 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gen_e_acsl_size_6 = 1UL * __gen_e_acsl__10;
+ if (__gen_e_acsl_size_6 <= 0UL) __gen_e_acsl_if_6 = 0UL;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 +
+ 1 * 0),
+ __gen_e_acsl_if_6);
+ __e_acsl_assert(__gen_e_acsl_initialized,1,"Postcondition","strncpy",
+ "initialization: \\initialized(\\old(dest) + (0 .. \\old(n) - 1))",
+ "FRAMAC_SHARE/libc/string.h",386);
+ __e_acsl_contract_clean(__gen_e_acsl_contract);
+ __e_acsl_delete_block((void *)(& src));
+ __e_acsl_delete_block((void *)(& dest));
+ __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl_sub_3);
+ __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl_at_3);
+ return __retres;
+ }
+}
+
+/*@ requires valid_string_src: valid_read_string(src);
+ requires room_string: \valid(dest + (0 .. strlen(src)));
+ requires
+ separation:
+ \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
+ ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest + (0 .. strlen{Old}(src))), \result;
+ assigns *(dest + (0 .. strlen{Old}(src)))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+ */
+char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
+{
+ char *__gen_e_acsl_at;
+ unsigned long __gen_e_acsl_strcpy_src_size;
+ char *__retres;
+ __e_acsl_store_block((void *)(& src),(size_t)8);
+ __e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
+ __gen_e_acsl_at = dest;
+ __retres = strcpy(dest,src);
+ {
+ __e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_strcpy_src_size;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_le;
+ unsigned long __gen_e_acsl_size;
+ __gmpz_init_set_ui(__gen_e_acsl___gen_e_acsl_strcpy_src_size,
+ __gen_e_acsl_strcpy_src_size);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl___gen_e_acsl_strcpy_src_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_ui(__gen_e_acsl__2,18446744073709551615UL);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __e_acsl_assert(__gen_e_acsl_le <= 0,1,"RTE","strcpy",
+ "size_lesser_or_eq_than_SIZE_MAX:\n __gen_e_acsl_strcpy_src_size + 1 <= 18446744073709551615",
+ "FRAMAC_SHARE/libc/string.h",367);
+ __gen_e_acsl_size = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __e_acsl_initialize((void *)dest,__gen_e_acsl_size);
+ __gmpz_clear(__gen_e_acsl___gen_e_acsl_strcpy_src_size);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl__2);
+ }
+ __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","strcpy",
+ "result_ptr: \\result == \\old(dest)",
+ "FRAMAC_SHARE/libc/string.h",374);
+ __e_acsl_delete_block((void *)(& src));
+ __e_acsl_delete_block((void *)(& dest));
+ return __retres;
+}
+
+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 = "a";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("a"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+ }
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
+ {
+ char dest[4];
+ __e_acsl_store_block((void *)(dest),(size_t)4);
+ char src[2] = {(char)'b', (char)'\000'};
+ __e_acsl_store_block((void *)(src),(size_t)2);
+ __e_acsl_full_init((void *)(& src));
+ {
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_size = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(dest + 1 * 0),
+ (size_t)__gen_e_acsl_if);
+ __e_acsl_assert(! __gen_e_acsl_initialized,1,"Assertion","main",
+ "!\\initialized(&dest[0 .. 3])","tests/libc/str.c",12);
+ }
+ /*@ assert ¬\initialized(&dest[0 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
+ int __gen_e_acsl_initialized_2;
+ __gen_e_acsl_size_2 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(src + 1 * 0),
+ (size_t)__gen_e_acsl_if_2);
+ __e_acsl_assert(__gen_e_acsl_initialized_2,1,"Assertion","main",
+ "\\initialized(&src[0 .. 1])","tests/libc/str.c",13);
+ }
+ /*@ assert \initialized(&src[0 .. 1]); */ ;
+ __gen_e_acsl_strcpy(dest,(char const *)(src));
+ {
+ int __gen_e_acsl_size_3;
+ int __gen_e_acsl_if_3;
+ int __gen_e_acsl_initialized_3;
+ __gen_e_acsl_size_3 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_3 <= 0) __gen_e_acsl_if_3 = 0;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(dest + 1 * 0),
+ (size_t)__gen_e_acsl_if_3);
+ __e_acsl_assert(__gen_e_acsl_initialized_3,1,"Assertion","main",
+ "\\initialized(&dest[0 .. 1])","tests/libc/str.c",16);
+ }
+ /*@ assert \initialized(&dest[0 .. 1]); */ ;
+ {
+ int __gen_e_acsl_size_4;
+ int __gen_e_acsl_if_4;
+ int __gen_e_acsl_initialized_4;
+ __gen_e_acsl_size_4 = 1 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size_4 <= 0) __gen_e_acsl_if_4 = 0;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(dest + 1 * 2),
+ (size_t)__gen_e_acsl_if_4);
+ __e_acsl_assert(! __gen_e_acsl_initialized_4,1,"Assertion","main",
+ "!\\initialized(&dest[2 .. 3])","tests/libc/str.c",17);
+ }
+ /*@ assert ¬\initialized(&dest[2 .. 3]); */ ;
+ __e_acsl_delete_block((void *)(src));
+ __e_acsl_delete_block((void *)(dest));
+ }
+ {
+ char dest_0[4];
+ __e_acsl_store_block((void *)(dest_0),(size_t)4);
+ char src_0[4] = {(char)'a', (char)'b', (char)'\000'};
+ __e_acsl_store_block((void *)(src_0),(size_t)4);
+ __e_acsl_full_init((void *)(& src_0));
+ {
+ int __gen_e_acsl_size_5;
+ int __gen_e_acsl_if_5;
+ int __gen_e_acsl_initialized_5;
+ __gen_e_acsl_size_5 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_5 <= 0) __gen_e_acsl_if_5 = 0;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(dest_0 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_5);
+ __e_acsl_assert(! __gen_e_acsl_initialized_5,1,"Assertion","main",
+ "!\\initialized(&dest_0[0 .. 3])","tests/libc/str.c",
+ 22);
+ }
+ /*@ assert ¬\initialized(&dest_0[0 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_6;
+ int __gen_e_acsl_if_6;
+ int __gen_e_acsl_initialized_6;
+ __gen_e_acsl_size_6 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_6 <= 0) __gen_e_acsl_if_6 = 0;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(src_0 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_6);
+ __e_acsl_assert(__gen_e_acsl_initialized_6,1,"Assertion","main",
+ "\\initialized(&src_0[0 .. 3])","tests/libc/str.c",23);
+ }
+ /*@ assert \initialized(&src_0[0 .. 3]); */ ;
+ __gen_e_acsl_strncpy(dest_0,(char const *)(src_0),(unsigned long)1);
+ {
+ int __gen_e_acsl_initialized_7;
+ __gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(dest_0),
+ sizeof(char));
+ __e_acsl_assert(__gen_e_acsl_initialized_7,1,"Assertion","main",
+ "\\initialized((char *)dest_0)","tests/libc/str.c",26);
+ }
+ /*@ assert \initialized((char *)dest_0); */ ;
+ {
+ int __gen_e_acsl_size_7;
+ int __gen_e_acsl_if_7;
+ int __gen_e_acsl_initialized_8;
+ __gen_e_acsl_size_7 = 1 * ((3 - 1) + 1);
+ if (__gen_e_acsl_size_7 <= 0) __gen_e_acsl_if_7 = 0;
+ else __gen_e_acsl_if_7 = __gen_e_acsl_size_7;
+ __gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(dest_0 +
+ 1 * 1),
+ (size_t)__gen_e_acsl_if_7);
+ __e_acsl_assert(! __gen_e_acsl_initialized_8,1,"Assertion","main",
+ "!\\initialized(&dest_0[1 .. 3])","tests/libc/str.c",
+ 27);
+ }
+ /*@ assert ¬\initialized(&dest_0[1 .. 3]); */ ;
+ __e_acsl_delete_block((void *)(src_0));
+ __e_acsl_delete_block((void *)(dest_0));
+ }
+ {
+ char dest_1[4];
+ __e_acsl_store_block((void *)(dest_1),(size_t)4);
+ char src_1[4] = {(char)'b', (char)'\000'};
+ __e_acsl_store_block((void *)(src_1),(size_t)4);
+ __e_acsl_full_init((void *)(& src_1));
+ {
+ int __gen_e_acsl_size_8;
+ int __gen_e_acsl_if_8;
+ int __gen_e_acsl_initialized_9;
+ __gen_e_acsl_size_8 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_8 <= 0) __gen_e_acsl_if_8 = 0;
+ else __gen_e_acsl_if_8 = __gen_e_acsl_size_8;
+ __gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)(dest_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_8);
+ __e_acsl_assert(! __gen_e_acsl_initialized_9,1,"Assertion","main",
+ "!\\initialized(&dest_1[0 .. 3])","tests/libc/str.c",
+ 32);
+ }
+ /*@ assert ¬\initialized(&dest_1[0 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_9;
+ int __gen_e_acsl_if_9;
+ int __gen_e_acsl_initialized_10;
+ __gen_e_acsl_size_9 = 1 * ((3 - 0) + 1);
+ if (__gen_e_acsl_size_9 <= 0) __gen_e_acsl_if_9 = 0;
+ else __gen_e_acsl_if_9 = __gen_e_acsl_size_9;
+ __gen_e_acsl_initialized_10 = __e_acsl_initialized((void *)(src_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_9);
+ __e_acsl_assert(__gen_e_acsl_initialized_10,1,"Assertion","main",
+ "\\initialized(&src_1[0 .. 3])","tests/libc/str.c",33);
+ }
+ /*@ assert \initialized(&src_1[0 .. 3]); */ ;
+ __gen_e_acsl_strncpy(dest_1,(char const *)(src_1),(unsigned long)3);
+ {
+ int __gen_e_acsl_size_10;
+ int __gen_e_acsl_if_10;
+ int __gen_e_acsl_initialized_11;
+ __gen_e_acsl_size_10 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_10 <= 0) __gen_e_acsl_if_10 = 0;
+ else __gen_e_acsl_if_10 = __gen_e_acsl_size_10;
+ __gen_e_acsl_initialized_11 = __e_acsl_initialized((void *)(dest_1 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_10);
+ __e_acsl_assert(__gen_e_acsl_initialized_11,1,"Assertion","main",
+ "\\initialized(&dest_1[0 .. 2])","tests/libc/str.c",36);
+ }
+ /*@ assert \initialized(&dest_1[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_12;
+ __gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& dest_1[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_12,1,"Assertion","main",
+ "!\\initialized(&dest_1[3])","tests/libc/str.c",37);
+ }
+ /*@ assert ¬\initialized(&dest_1[3]); */ ;
+ __e_acsl_delete_block((void *)(src_1));
+ __e_acsl_delete_block((void *)(dest_1));
+ }
+ {
+ char dest_2[4];
+ __e_acsl_store_block((void *)(dest_2),(size_t)4);
+ __gen_e_acsl_strcpy(dest_2,__gen_e_acsl_literal_string);
+ char src_2[2] = {(char)'b', (char)'\000'};
+ __e_acsl_store_block((void *)(src_2),(size_t)2);
+ __e_acsl_full_init((void *)(& src_2));
+ {
+ int __gen_e_acsl_size_11;
+ int __gen_e_acsl_if_11;
+ int __gen_e_acsl_initialized_13;
+ __gen_e_acsl_size_11 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_11 <= 0) __gen_e_acsl_if_11 = 0;
+ else __gen_e_acsl_if_11 = __gen_e_acsl_size_11;
+ __gen_e_acsl_initialized_13 = __e_acsl_initialized((void *)(dest_2 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_11);
+ __e_acsl_assert(__gen_e_acsl_initialized_13,1,"Assertion","main",
+ "\\initialized(&dest_2[0 .. 1])","tests/libc/str.c",43);
+ }
+ /*@ assert \initialized(&dest_2[0 .. 1]); */ ;
+ {
+ int __gen_e_acsl_size_12;
+ int __gen_e_acsl_if_12;
+ int __gen_e_acsl_initialized_14;
+ __gen_e_acsl_size_12 = 1 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size_12 <= 0) __gen_e_acsl_if_12 = 0;
+ else __gen_e_acsl_if_12 = __gen_e_acsl_size_12;
+ __gen_e_acsl_initialized_14 = __e_acsl_initialized((void *)(dest_2 +
+ 1 * 2),
+ (size_t)__gen_e_acsl_if_12);
+ __e_acsl_assert(! __gen_e_acsl_initialized_14,1,"Assertion","main",
+ "!\\initialized(&dest_2[2 .. 3])","tests/libc/str.c",
+ 44);
+ }
+ /*@ assert ¬\initialized(&dest_2[2 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_13;
+ int __gen_e_acsl_if_13;
+ int __gen_e_acsl_initialized_15;
+ __gen_e_acsl_size_13 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_13 <= 0) __gen_e_acsl_if_13 = 0;
+ else __gen_e_acsl_if_13 = __gen_e_acsl_size_13;
+ __gen_e_acsl_initialized_15 = __e_acsl_initialized((void *)(src_2 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_13);
+ __e_acsl_assert(__gen_e_acsl_initialized_15,1,"Assertion","main",
+ "\\initialized(&src_2[0 .. 1])","tests/libc/str.c",45);
+ }
+ /*@ assert \initialized(&src_2[0 .. 1]); */ ;
+ __gen_e_acsl_strcat(dest_2,(char const *)(src_2));
+ {
+ int __gen_e_acsl_size_14;
+ int __gen_e_acsl_if_14;
+ int __gen_e_acsl_initialized_16;
+ __gen_e_acsl_size_14 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_14 <= 0) __gen_e_acsl_if_14 = 0;
+ else __gen_e_acsl_if_14 = __gen_e_acsl_size_14;
+ __gen_e_acsl_initialized_16 = __e_acsl_initialized((void *)(dest_2 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_14);
+ __e_acsl_assert(__gen_e_acsl_initialized_16,1,"Assertion","main",
+ "\\initialized(&dest_2[0 .. 2])","tests/libc/str.c",48);
+ }
+ /*@ assert \initialized(&dest_2[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_17;
+ __gen_e_acsl_initialized_17 = __e_acsl_initialized((void *)(& dest_2[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_17,1,"Assertion","main",
+ "!\\initialized(&dest_2[3])","tests/libc/str.c",49);
+ }
+ /*@ assert ¬\initialized(&dest_2[3]); */ ;
+ __e_acsl_delete_block((void *)(src_2));
+ __e_acsl_delete_block((void *)(dest_2));
+ }
+ {
+ char dest_3[4];
+ __e_acsl_store_block((void *)(dest_3),(size_t)4);
+ __gen_e_acsl_strcpy(dest_3,__gen_e_acsl_literal_string);
+ char src_3[3] = {(char)'b', (char)'c', (char)'\000'};
+ __e_acsl_store_block((void *)(src_3),(size_t)3);
+ __e_acsl_full_init((void *)(& src_3));
+ {
+ int __gen_e_acsl_size_15;
+ int __gen_e_acsl_if_15;
+ int __gen_e_acsl_initialized_18;
+ __gen_e_acsl_size_15 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_15 <= 0) __gen_e_acsl_if_15 = 0;
+ else __gen_e_acsl_if_15 = __gen_e_acsl_size_15;
+ __gen_e_acsl_initialized_18 = __e_acsl_initialized((void *)(dest_3 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_15);
+ __e_acsl_assert(__gen_e_acsl_initialized_18,1,"Assertion","main",
+ "\\initialized(&dest_3[0 .. 1])","tests/libc/str.c",55);
+ }
+ /*@ assert \initialized(&dest_3[0 .. 1]); */ ;
+ {
+ int __gen_e_acsl_size_16;
+ int __gen_e_acsl_if_16;
+ int __gen_e_acsl_initialized_19;
+ __gen_e_acsl_size_16 = 1 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size_16 <= 0) __gen_e_acsl_if_16 = 0;
+ else __gen_e_acsl_if_16 = __gen_e_acsl_size_16;
+ __gen_e_acsl_initialized_19 = __e_acsl_initialized((void *)(dest_3 +
+ 1 * 2),
+ (size_t)__gen_e_acsl_if_16);
+ __e_acsl_assert(! __gen_e_acsl_initialized_19,1,"Assertion","main",
+ "!\\initialized(&dest_3[2 .. 3])","tests/libc/str.c",
+ 56);
+ }
+ /*@ assert ¬\initialized(&dest_3[2 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_17;
+ int __gen_e_acsl_if_17;
+ int __gen_e_acsl_initialized_20;
+ __gen_e_acsl_size_17 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_17 <= 0) __gen_e_acsl_if_17 = 0;
+ else __gen_e_acsl_if_17 = __gen_e_acsl_size_17;
+ __gen_e_acsl_initialized_20 = __e_acsl_initialized((void *)(src_3 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_17);
+ __e_acsl_assert(__gen_e_acsl_initialized_20,1,"Assertion","main",
+ "\\initialized(&src_3[0 .. 2])","tests/libc/str.c",57);
+ }
+ /*@ assert \initialized(&src_3[0 .. 2]); */ ;
+ __gen_e_acsl_strncat(dest_3,(char const *)(src_3),(unsigned long)1);
+ {
+ int __gen_e_acsl_size_18;
+ int __gen_e_acsl_if_18;
+ int __gen_e_acsl_initialized_21;
+ __gen_e_acsl_size_18 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_18 <= 0) __gen_e_acsl_if_18 = 0;
+ else __gen_e_acsl_if_18 = __gen_e_acsl_size_18;
+ __gen_e_acsl_initialized_21 = __e_acsl_initialized((void *)(dest_3 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_18);
+ __e_acsl_assert(__gen_e_acsl_initialized_21,1,"Assertion","main",
+ "\\initialized(&dest_3[0 .. 2])","tests/libc/str.c",60);
+ }
+ /*@ assert \initialized(&dest_3[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_22;
+ __gen_e_acsl_initialized_22 = __e_acsl_initialized((void *)(& dest_3[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_22,1,"Assertion","main",
+ "!\\initialized(&dest_3[3])","tests/libc/str.c",61);
+ }
+ /*@ assert ¬\initialized(&dest_3[3]); */ ;
+ __e_acsl_delete_block((void *)(src_3));
+ __e_acsl_delete_block((void *)(dest_3));
+ }
+ {
+ char dest_4[4];
+ __e_acsl_store_block((void *)(dest_4),(size_t)4);
+ __gen_e_acsl_strcpy(dest_4,__gen_e_acsl_literal_string);
+ char src_4[2] = {(char)'b', (char)'\000'};
+ __e_acsl_store_block((void *)(src_4),(size_t)2);
+ __e_acsl_full_init((void *)(& src_4));
+ {
+ int __gen_e_acsl_size_19;
+ int __gen_e_acsl_if_19;
+ int __gen_e_acsl_initialized_23;
+ __gen_e_acsl_size_19 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_19 <= 0) __gen_e_acsl_if_19 = 0;
+ else __gen_e_acsl_if_19 = __gen_e_acsl_size_19;
+ __gen_e_acsl_initialized_23 = __e_acsl_initialized((void *)(dest_4 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_19);
+ __e_acsl_assert(__gen_e_acsl_initialized_23,1,"Assertion","main",
+ "\\initialized(&dest_4[0 .. 1])","tests/libc/str.c",67);
+ }
+ /*@ assert \initialized(&dest_4[0 .. 1]); */ ;
+ {
+ int __gen_e_acsl_size_20;
+ int __gen_e_acsl_if_20;
+ int __gen_e_acsl_initialized_24;
+ __gen_e_acsl_size_20 = 1 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size_20 <= 0) __gen_e_acsl_if_20 = 0;
+ else __gen_e_acsl_if_20 = __gen_e_acsl_size_20;
+ __gen_e_acsl_initialized_24 = __e_acsl_initialized((void *)(dest_4 +
+ 1 * 2),
+ (size_t)__gen_e_acsl_if_20);
+ __e_acsl_assert(! __gen_e_acsl_initialized_24,1,"Assertion","main",
+ "!\\initialized(&dest_4[2 .. 3])","tests/libc/str.c",
+ 68);
+ }
+ /*@ assert ¬\initialized(&dest_4[2 .. 3]); */ ;
+ {
+ int __gen_e_acsl_size_21;
+ int __gen_e_acsl_if_21;
+ int __gen_e_acsl_initialized_25;
+ __gen_e_acsl_size_21 = 1 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_21 <= 0) __gen_e_acsl_if_21 = 0;
+ else __gen_e_acsl_if_21 = __gen_e_acsl_size_21;
+ __gen_e_acsl_initialized_25 = __e_acsl_initialized((void *)(src_4 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_21);
+ __e_acsl_assert(__gen_e_acsl_initialized_25,1,"Assertion","main",
+ "\\initialized(&src_4[0 .. 1])","tests/libc/str.c",69);
+ }
+ /*@ assert \initialized(&src_4[0 .. 1]); */ ;
+ __gen_e_acsl_strncat(dest_4,(char const *)(src_4),(unsigned long)2);
+ {
+ int __gen_e_acsl_size_22;
+ int __gen_e_acsl_if_22;
+ int __gen_e_acsl_initialized_26;
+ __gen_e_acsl_size_22 = 1 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_22 <= 0) __gen_e_acsl_if_22 = 0;
+ else __gen_e_acsl_if_22 = __gen_e_acsl_size_22;
+ __gen_e_acsl_initialized_26 = __e_acsl_initialized((void *)(dest_4 +
+ 1 * 0),
+ (size_t)__gen_e_acsl_if_22);
+ __e_acsl_assert(__gen_e_acsl_initialized_26,1,"Assertion","main",
+ "\\initialized(&dest_4[0 .. 2])","tests/libc/str.c",72);
+ }
+ /*@ assert \initialized(&dest_4[0 .. 2]); */ ;
+ {
+ int __gen_e_acsl_initialized_27;
+ __gen_e_acsl_initialized_27 = __e_acsl_initialized((void *)(& dest_4[3]),
+ sizeof(char));
+ __e_acsl_assert(! __gen_e_acsl_initialized_27,1,"Assertion","main",
+ "!\\initialized(&dest_4[3])","tests/libc/str.c",73);
+ }
+ /*@ assert ¬\initialized(&dest_4[3]); */ ;
+ __e_acsl_delete_block((void *)(src_4));
+ __e_acsl_delete_block((void *)(dest_4));
+ }
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
new file mode 100644
index 00000000000..0cb515ff9dc
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
@@ -0,0 +1,45 @@
+[e-acsl] beginning translation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:134: Warning:
+ E-ACSL construct `user-defined logic type' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:120: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:121: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:120: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:124: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:96: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:101: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] FRAMAC_SHARE/libc/string.h:134: Warning:
+ function __gen_e_acsl_memset: postcondition 'acsl_c_equiv' got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:98: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:101: Warning:
+ function __gen_e_acsl_memcpy: postcondition 'copied_contents' got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:124: Warning:
+ function __gen_e_acsl_memmove: postcondition 'copied_contents' got status unknown.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/sprintf.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/sprintf.res.oracle
new file mode 100644
index 00000000000..11886784cad
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/oracle/sprintf.res.oracle
@@ -0,0 +1,15 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/libc/sprintf.c:13: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/libc/sprintf.c:14: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/libc/sprintf.c:21: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/libc/sprintf.c:22: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/libc/sprintf.c:22: Warning: assertion got status unknown.
+[eva:alarm] tests/libc/sprintf.c:29: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] tests/libc/sprintf.c:30: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
new file mode 100644
index 00000000000..c78ac288df7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
@@ -0,0 +1,118 @@
+[e-acsl] beginning translation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:445: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:453: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:439: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:446: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:454: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:438: Warning:
+ Some assumes clauses could not be translated.
+ Ignoring complete and disjoint behaviors annotations.
+[e-acsl] FRAMAC_SHARE/libc/string.h:438: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:443: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:450: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:450: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:458: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:424: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:426: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:423: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:429: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:432: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:433: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:388: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:391: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:379: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:378: Warning:
+ Some assumes clauses could not be translated.
+ Ignoring complete and disjoint behaviors annotations.
+[e-acsl] FRAMAC_SHARE/libc/string.h:378: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:389: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:392: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:368: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:370: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:373: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] FRAMAC_SHARE/libc/string.h:367: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:373: Warning:
+ function __gen_e_acsl_strcpy: postcondition 'equal_contents' got status unknown.
+[eva:alarm] tests/libc/str.c:16: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
diff --git a/src/plugins/e-acsl/tests/libc/oracle_dev/file.e-acsl.err.log b/src/plugins/e-acsl/tests/libc/oracle_dev/file.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/libc/oracle_dev/mem.e-acsl.err.log b/src/plugins/e-acsl/tests/libc/oracle_dev/mem.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/libc/oracle_dev/sprintf.e-acsl.err.log b/src/plugins/e-acsl/tests/libc/oracle_dev/sprintf.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/libc/oracle_dev/str.e-acsl.err.log b/src/plugins/e-acsl/tests/libc/oracle_dev/str.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/libc/sprintf.c b/src/plugins/e-acsl/tests/libc/sprintf.c
new file mode 100644
index 00000000000..3dab08bceda
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/sprintf.c
@@ -0,0 +1,33 @@
+/* run.config
+ COMMENT: Test non built-in `sprintf` memory tracking
+*/
+
+#include <stdio.h>
+
+int main() {
+ {
+ char buf[4];
+ //@ assert !\initialized(&buf[0..3]);
+
+ sprintf(buf, "%d", 10);
+ //@ assert \initialized(&buf[0..2]);
+ //@ assert !\initialized(&buf[3]);
+ }
+ { // snprintf with n < what would be printed
+ char buf[4];
+ //@ assert !\initialized(&buf[0..3]);
+
+ snprintf(buf, 2, "%d", 10);
+ //@ assert \initialized(&buf[0..1]);
+ //@ assert !\initialized(&buf[2..3]);
+ }
+ { // snprintf with n >= what would be printed
+ char buf[4];
+ //@ assert !\initialized(&buf[0..3]);
+
+ snprintf(buf, 4, "%d", 10);
+ //@ assert \initialized(&buf[0..2]);
+ //@ assert !\initialized(&buf[3]);
+ }
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/libc/str.c b/src/plugins/e-acsl/tests/libc/str.c
new file mode 100644
index 00000000000..dca113d6d15
--- /dev/null
+++ b/src/plugins/e-acsl/tests/libc/str.c
@@ -0,0 +1,76 @@
+/* run.config
+ COMMENT: Test non built-in `strcpy`, `strncpy`, `strcat` and `strncat` memory
+ COMMENT: tracking
+*/
+
+#include <string.h>
+
+int main() {
+ {
+ char dest[4];
+ char src[] = "b";
+ //@ assert !\initialized(&dest[0..3]);
+ //@ assert \initialized(&src[0..1]);
+
+ strcpy(dest, src);
+ //@ assert \initialized(&dest[0..1]);
+ //@ assert !\initialized(&dest[2..3]);
+ }
+ { // strncpy with n < strlen(src)
+ char dest[4];
+ char src[4] = "ab";
+ //@ assert !\initialized(&dest[0..3]);
+ //@ assert \initialized(&src[0..3]);
+
+ strncpy(dest, src, 1);
+ //@ assert \initialized(&dest[0]);
+ //@ assert !\initialized(&dest[1..3]);
+ }
+ { // strncpy with n >= strlen(src)
+ char dest[4];
+ char src[4] = "b";
+ //@ assert !\initialized(&dest[0..3]);
+ //@ assert \initialized(&src[0..3]);
+
+ strncpy(dest, src, 3);
+ //@ assert \initialized(&dest[0..2]);
+ //@ assert !\initialized(&dest[3]);
+ }
+ {
+ char dest[4];
+ strcpy(dest, "a");
+ char src[] = "b";
+ //@ assert \initialized(&dest[0..1]);
+ //@ assert !\initialized(&dest[2..3]);
+ //@ assert \initialized(&src[0..1]);
+
+ strcat(dest, src);
+ //@ assert \initialized(&dest[0..2]);
+ //@ assert !\initialized(&dest[3]);
+ }
+ { // strncat with n < strlen(src)
+ char dest[4];
+ strcpy(dest, "a");
+ char src[] = "bc";
+ //@ assert \initialized(&dest[0..1]);
+ //@ assert !\initialized(&dest[2..3]);
+ //@ assert \initialized(&src[0..2]);
+
+ strncat(dest, src, 1);
+ //@ assert \initialized(&dest[0..2]);
+ //@ assert !\initialized(&dest[3]);
+ }
+ { // strncat with n >= strlen(src)
+ char dest[4];
+ strcpy(dest, "a");
+ char src[] = "b";
+ //@ assert \initialized(&dest[0..1]);
+ //@ assert !\initialized(&dest[2..3]);
+ //@ assert \initialized(&src[0..1]);
+
+ strncat(dest, src, 2);
+ //@ assert \initialized(&dest[0..2]);
+ //@ assert !\initialized(&dest[3]);
+ }
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
index 8af8c087c3b..74706f9a7b5 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
@@ -406,6 +406,7 @@ void *__gen_e_acsl_memset(void *s, int c, size_t n)
__e_acsl_temporal_memset(s,c,n);
__gen_e_acsl_at = s;
__retres = memset(s,c,n);
+ __e_acsl_initialize(s,n);
__e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","memset",
"result_ptr: \\result == \\old(s)",
"FRAMAC_SHARE/libc/string.h",135);
@@ -527,6 +528,7 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
}
__gen_e_acsl_at = dest;
__retres = memcpy(dest,src,n);
+ __e_acsl_initialize(dest,n);
__e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","memcpy",
"result_ptr: \\result == \\old(dest)",
"FRAMAC_SHARE/libc/string.h",102);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index b2e2ee7e00a..e7b1b71eea0 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -1,10 +1,4 @@
[e-acsl] beginning translation.
-[e-acsl] Warning: annotating undefined function `memcpy':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `memset':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning:
E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
--
GitLab