Commit 9bd40552 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl:tests] Fix missing include in bts2252.c

parent b6d2d297
......@@ -3,6 +3,7 @@
*/
#include <stdlib.h>
#include <string.h>
int main() {
char* srcbuf = "Test Code";
......
[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);
/* 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;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment