diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore index 961b1be371372dbca6dc5054966d33ab3c268119..a76fdee561c4288a70fd4b3473fd29e6caf5ef14 100644 --- a/src/plugins/e-acsl/.gitignore +++ b/src/plugins/e-acsl/.gitignore @@ -56,6 +56,7 @@ /tests/test_config /tests/runtime/*.cm* /tests/runtime/result/* +/tests/temporal/result/* /tests/no-main/result/* /tests/full-mmodel/result/* /tests/bts/result/* @@ -79,3 +80,4 @@ lib/libeacsl-rtl-bittree.a lib/libeacsl-rtl-segment.a lib/libeacsl-rtl-bittree-dbg.a lib/libeacsl-rtl-segment-dbg.a +tests/csrv14/* diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c index c1e706f89286ec32db531e296d95f9baf8285f49..bd10ab4363940a8a9530bf3022ad7e42f6d90255 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c +++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c @@ -98,11 +98,8 @@ int main(void) } else __gen_e_acsl_and_4 = 0; __e_acsl_assert(! __gen_e_acsl_and_4,(char *)"Assertion", - (char *)"main",(char *)"!\\valid(q)",23); + (char *)"main",(char *)"!\\valid(q)",24); } - /*@ assert Value: dangling_pointer: ¬\dangling(&q); */ - __e_acsl_initialize((void *)q,sizeof(int)); - *q = 1; /*@ assert \valid(&j); */ { int __gen_e_acsl_valid_5; @@ -131,6 +128,7 @@ int main(void) sizeof(int *)); if (__gen_e_acsl_initialized_5) { int __gen_e_acsl_valid_6; + /*@ assert Value: dangling_pointer: ¬\dangling(&p); */ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)p,sizeof(int), (void *)p,(void *)(& p)); __gen_e_acsl_and_5 = __gen_e_acsl_valid_6; diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle index 5b5f54b8ce52a0a388f5d11ebab96a8c9744c966..6d86bdfbac779cfd93fba867c425bdfe043b6b09 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle +++ b/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle @@ -2,4 +2,7 @@ [e-acsl] translation done in project "e-acsl". tests/temporal/t_scope.c:10:[value] warning: locals {i} escaping the scope of a block of main through p tests/temporal/t_scope.c:10:[value] warning: locals {i} escaping the scope of a block of main through q -[scope:rm_asserts] removing 2 assertion(s) +tests/temporal/t_scope.c:19:[value] warning: locals {j} escaping the scope of a block of main through p +tests/temporal/t_scope.c:33:[value] warning: locals {a} escaping the scope of a block of main through p +tests/temporal/t_scope.c:33:[value] warning: locals {a} escaping the scope of a block of main through q +[scope:rm_asserts] removing 1 assertion(s) diff --git a/src/plugins/e-acsl/tests/temporal/t_scope.c b/src/plugins/e-acsl/tests/temporal/t_scope.c index 14435dc27e60b4f6bb479ae642803d3ec9fef830..d023e0fb4971bc3bba5d01a973b341698a94751b 100644 --- a/src/plugins/e-acsl/tests/temporal/t_scope.c +++ b/src/plugins/e-acsl/tests/temporal/t_scope.c @@ -20,8 +20,8 @@ int main() { p = &j; /*@assert \valid(p); */ *p = 1; + /* `q` now may point to `j`, bit not necessarily */ /*@assert ! \valid(q); */ - *q = 1; /*@assert \valid(&j); */ }