diff --git a/src/plugins/e-acsl/tests/bts/bts2252.c b/src/plugins/e-acsl/tests/bts/bts2252.c
index c52b56d04f0cd46500998328172f2f3c9d3c43a3..7bd739ccc4fe5826554b48a894bb58c5c1264992 100644
--- a/src/plugins/e-acsl/tests/bts/bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/bts2252.c
@@ -3,6 +3,7 @@
*/
#include <stdlib.h>
+#include <string.h>
int main() {
char* srcbuf = "Test Code";
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
index 9516b93607c4dc48622167d15db9d2a662cdf286..c0d14a505d07b9519cd7815386d12346a4c15e42 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
@@ -1,6 +1,25 @@
-[kernel:typing:implicit-function-declaration] tests/bts/bts2252.c:22: Warning:
- Calling undeclared function strncpy. Old style K&R code?
[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:362: Warning:
+ E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:363: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:366: Warning:
+ E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:372: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:372: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:375: 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] tests/bts/bts2252.c:17: Warning:
+[eva:alarm] tests/bts/bts2252.c:18: Warning:
out of bounds read. assert \valid_read(srcbuf + i);
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
index 4ee6b66b44b57196aa0861c7e89c5fcd16e2ea9f..989bcb1766bd17886c7cc66d06c696124849a70f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
@@ -1,8 +1,149 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
+#include "string.h"
char *__gen_e_acsl_literal_string;
-extern int ( /* missing proto */ strncpy)(char *x_0, char *x_1, int x_2);
+extern int __e_acsl_sound_verdict;
+
+/*@ 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_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;
+ char *__retres;
+ {
+ __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;
+ int __gen_e_acsl_valid;
+ __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_valid = __e_acsl_valid((void *)(dest + 1 * 0),
+ __gen_e_acsl__3,(void *)dest,
+ (void *)(& dest));
+ __e_acsl_assert(__gen_e_acsl_valid,"Precondition","strncpy",
+ "\\valid(dest + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",364);
+ __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_mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl_sub_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ unsigned long __gen_e_acsl__6;
+ int __gen_e_acsl_initialized;
+ __e_acsl_assert(__retres == __gen_e_acsl_at,"Postcondition","strncpy",
+ "\\result == \\old(dest)","FRAMAC_SHARE/libc/string.h",
+ 369);
+ __gmpz_init_set_si(__gen_e_acsl__4,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__4));
+ __gmpz_init_set_si(__gen_e_acsl__5,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__5));
+ __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__4));
+ __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 +
+ 1 * 0),
+ __gen_e_acsl__6);
+ __e_acsl_assert(__gen_e_acsl_initialized,"Postcondition","strncpy",
+ "\\initialized(\\old(dest) + (0 .. \\old(n) - 1))",
+ "FRAMAC_SHARE/libc/string.h",370);
+ __e_acsl_delete_block((void *)(& dest));
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_sub_3);
+ __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl_at_3);
+ return __retres;
+ }
+}
void __e_acsl_globals_init(void)
{
@@ -29,6 +170,8 @@ int main(void)
__e_acsl_full_init((void *)(& srcbuf));
int loc = 1;
char *destbuf = malloc((unsigned long)10 * sizeof(char));
+ __e_acsl_store_block((void *)(& destbuf),(size_t)8);
+ __e_acsl_full_init((void *)(& destbuf));
char ch = (char)'o';
if (destbuf != (char *)0) {
i = -1;
@@ -40,17 +183,19 @@ int main(void)
(void *)srcbuf,
(void *)(& srcbuf));
__e_acsl_assert(! __gen_e_acsl_valid_read,"Assertion","main",
- "!\\valid_read(srcbuf + i)","tests/bts/bts2252.c",16);
+ "!\\valid_read(srcbuf + i)","tests/bts/bts2252.c",17);
}
/*@ assert ¬\valid_read(srcbuf + i); */ ;
/*@ assert Eva: mem_access: \valid_read(srcbuf + i); */
if ((int)*(srcbuf + i) == (int)ch) loc = i;
i ++;
}
- strncpy(destbuf + loc,srcbuf + loc,1);
+ __gen_e_acsl_strncpy(destbuf + loc,(char const *)(srcbuf + loc),
+ (unsigned long)1);
free((void *)destbuf);
}
__retres = 0;
+ __e_acsl_delete_block((void *)(& destbuf));
__e_acsl_delete_block((void *)(& srcbuf));
__e_acsl_memory_clean();
return __retres;