diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c index f36822ef19ede5e6bf632b077a65e20d6e178494..5270202b6e3bcccf26a1def51016a900a951c2d2 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c @@ -4,8 +4,9 @@ EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts14782.c > /dev/null && ./gcc_test.sh bts14782 */ -int global_i = 0; +int global_i; int* global_i_ptr = &global_i; +int global_i = 0; /*@ requires global_i == 0; requires \valid(global_i_ptr); diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle index 63841d478c452e284f2fcf7e6326119300bd0cf6..646927eca204f29f389f8c2f13c1d6ad84bf625b 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle @@ -22,9 +22,9 @@ global_i_ptr ∈ {{ &global_i }} [value] using specification for function __store_block [value] using specification for function __full_init -tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid. tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid. tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid. +tests/e-acsl-runtime/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid. [value] using specification for function __gmpz_init_set_si FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp @@ -36,9 +36,9 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] using specification for function __gmpz_clear FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/bts1478.c:10:[value] Function loop: precondition got status valid. tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid. tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid. +tests/e-acsl-runtime/bts1478.c:13:[value] Function loop: precondition got status valid. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle index d8cdc32d4bf37f76bc52779cd67233dc95e7e6d2..819a1984571441405e02d25f21d8592e3f2702b1 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle @@ -22,16 +22,16 @@ global_i_ptr ∈ {{ &global_i }} [value] using specification for function __store_block [value] using specification for function __full_init -tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid. tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid. tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid. +tests/e-acsl-runtime/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid. [value] using specification for function e_acsl_assert FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] using specification for function __valid FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/bts1478.c:10:[value] Function loop: precondition got status valid. tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid. tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid. +tests/e-acsl-runtime/bts1478.c:13:[value] Function loop: precondition got status valid. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c index ce1a2038dc845eba24da525c20adb6625d02331b..291c1d24a8272a564dd7f3d43866773611073709 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c @@ -62,8 +62,10 @@ extern size_t __memory_size; predicate diffSize{L1, L2}(ℤ i) = \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i; */ -int global_i = 0; +int global_i; + int *global_i_ptr = & global_i; +int global_i = 0; /*@ requires global_i ≡ 0; requires \valid(global_i_ptr); requires global_i_ptr ≡ &global_i; @@ -82,12 +84,12 @@ void __e_acsl_loop(void) { int __e_acsl_valid; e_acsl_assert(global_i == 0,(char *)"Precondition",(char *)"loop", - (char *)"global_i == 0",10); + (char *)"global_i == 0",11); __e_acsl_valid = __valid((void *)global_i_ptr,sizeof(int)); e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"loop", - (char *)"\\valid(global_i_ptr)",11); + (char *)"\\valid(global_i_ptr)",12); e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition", - (char *)"loop",(char *)"global_i_ptr == &global_i",12); + (char *)"loop",(char *)"global_i_ptr == &global_i",13); loop(); } return; diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c index ef98386277da8542f8df7e3e143ecf4399d7e671..5bfa785f3bf44761c346e8bec1dcc3926ae61453 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c @@ -85,8 +85,10 @@ extern size_t __memory_size; predicate diffSize{L1, L2}(ℤ i) = \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i; */ -int global_i = 0; +int global_i; + int *global_i_ptr = & global_i; +int global_i = 0; /*@ requires global_i ≡ 0; requires \valid(global_i_ptr); requires global_i_ptr ≡ &global_i; @@ -112,12 +114,12 @@ void __e_acsl_loop(void) __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_global_i), (__mpz_struct const *)(__e_acsl)); e_acsl_assert(__e_acsl_eq == 0,(char *)"Precondition",(char *)"loop", - (char *)"global_i == 0",10); + (char *)"global_i == 0",11); __e_acsl_valid = __valid((void *)global_i_ptr,sizeof(int)); e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"loop", - (char *)"\\valid(global_i_ptr)",11); + (char *)"\\valid(global_i_ptr)",12); e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition", - (char *)"loop",(char *)"global_i_ptr == &global_i",12); + (char *)"loop",(char *)"global_i_ptr == &global_i",13); __gmpz_clear(__e_acsl_global_i); __gmpz_clear(__e_acsl); loop();