diff --git a/src/plugins/e-acsl/tests/bts/bts2252.c b/src/plugins/e-acsl/tests/bts/bts2252.c index 6b268ff1b972407ce4a818a1a12faf233318db7b..c52b56d04f0cd46500998328172f2f3c9d3c43a3 100644 --- a/src/plugins/e-acsl/tests/bts/bts2252.c +++ b/src/plugins/e-acsl/tests/bts/bts2252.c @@ -2,12 +2,24 @@ COMMENT: bts #2252, failures due to typing of offsets */ -int *p; -int main(void) { - int i = -1; - int t[10]; - /*@ assert ! \valid_read(t+i); */ - p = t; - /*@ assert ! \valid_read(p+i); */ - return 0; +#include <stdlib.h> + +int main() { + char* srcbuf = "Test Code"; + int i, loc = 1; + + char * destbuf = (char*)malloc(10*sizeof(char)); + char ch = 'o'; + + if (destbuf != NULL) { + for (i = -1; i < 0; i++) { + /*@ assert ! \valid_read(srcbuf + i); */ + if (srcbuf[i] == ch) { /* ERROR: Buffer Underrun */ + loc = i; + } + } + + strncpy (&destbuf[loc], &srcbuf[loc], 1); + free(destbuf); + } } 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 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..3e7b66c55fac4ab43c317b9b34c90f04a6ea19b8 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle @@ -1,4 +1,7 @@ +tests/bts/bts2252.c:22:[kernel] warning: Calling undeclared function strncpy. Old style K&R code? [e-acsl] beginning translation. FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype +tests/bts/bts2252.c:22:[kernel] warning: Neither code nor specification for function strncpy, generating default assigns from the prototype [e-acsl] translation done in project "e-acsl". FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. +tests/bts/bts2252.c:17:[value] warning: out of bounds read. assert \valid_read(srcbuf + i); 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 3a492d48a045028e7511ffdd78c9d9cdf55e40d3..17547beac1f1023c14821f42b8154d44bae42d1c 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c +++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c @@ -1,45 +1,61 @@ /* Generated by Frama-C */ -int *p; +char *__gen_e_acsl_literal_string; +/*@ assigns \result, *(x_0 + (0 ..)), *(x_1 + (0 ..)); + assigns \result \from *(x_0 + (0 ..)), *(x_1 + (0 ..)), x_2; + assigns *(x_0 + (0 ..)) \from *(x_0 + (0 ..)), *(x_1 + (0 ..)), x_2; + assigns *(x_1 + (0 ..)) \from *(x_0 + (0 ..)), *(x_1 + (0 ..)), x_2; + */ +extern int ( /* missing proto */ strncpy)(char *x_0, char *x_1, int x_2); + void __e_acsl_globals_init(void) { - __e_acsl_store_block((void *)(& p),8UL); - __e_acsl_full_init((void *)(& p)); + __gen_e_acsl_literal_string = "Test Code"; + __e_acsl_store_block((void *)__gen_e_acsl_literal_string, + sizeof("Test Code")); + __e_acsl_full_init((void *)__gen_e_acsl_literal_string); + __e_acsl_readonly((void *)__gen_e_acsl_literal_string); return; } int main(void) { int __retres; + char *srcbuf; int i; - int t[10]; + int loc; + char *destbuf; + char ch; __e_acsl_memory_init((int *)0,(char ***)0,8UL); __e_acsl_globals_init(); - __e_acsl_store_block((void *)(t),40UL); - i = -1; - /*@ assert ¬\valid_read(&t[i]); */ - { - { - int __gen_e_acsl_valid_read; - __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& t[i]), - sizeof(int)); - __e_acsl_assert(! __gen_e_acsl_valid_read,(char *)"Assertion", - (char *)"main",(char *)"!\\valid_read(&t[i])",9); - } - } - p = t; - /*@ assert ¬\valid_read(p + i); */ - { - { - int __gen_e_acsl_valid_read_2; - __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + i), - sizeof(int)); - __e_acsl_assert(! __gen_e_acsl_valid_read_2,(char *)"Assertion", - (char *)"main",(char *)"!\\valid_read(p + i)",11); + __e_acsl_store_block((void *)(& srcbuf),8UL); + __e_acsl_full_init((void *)(& srcbuf)); + srcbuf = (char *)__gen_e_acsl_literal_string; + loc = 1; + destbuf = (char *)malloc((unsigned long)10 * sizeof(char)); + ch = (char)'o'; + if (destbuf != (char *)0) { + i = -1; + while (i < 0) { + /*@ assert ¬\valid_read(srcbuf + i); */ + { + { + int __gen_e_acsl_valid_read; + __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(srcbuf + i), + sizeof(char)); + __e_acsl_assert(! __gen_e_acsl_valid_read,(char *)"Assertion", + (char *)"main",(char *)"!\\valid_read(srcbuf + i)", + 16); + } + } + /*@ assert Value: mem_access: \valid_read(srcbuf + i); */ + if ((int)*(srcbuf + i) == (int)ch) loc = i; + i ++; } + strncpy(destbuf + loc,srcbuf + loc,1); + free((void *)destbuf); } __retres = 0; - __e_acsl_delete_block((void *)(& p)); - __e_acsl_delete_block((void *)(t)); + __e_acsl_delete_block((void *)(& srcbuf)); __e_acsl_memory_clean(); return __retres; }