Bugfix for t_scope testcase

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/*

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;

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)

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); */
   }