[e-acsl] fix two tests; stdin is read-only

src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c

@@ -126,20 +126,21 @@ void *thread_start(void *arg)
   }
   /*@ assert \valid(__fc_stderr) && \initialized(__fc_stderr); */ ;
   {
-    int __gen_e_acsl_valid_3;
+    int __gen_e_acsl_valid_read;
     int __gen_e_acsl_and_3;
     __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
       {.values = (void *)0};
-    __gen_e_acsl_valid_3 = __e_acsl_valid((void *)stdin,sizeof(FILE),
-                                          (void *)stdin,(void *)(& stdin));
+    __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)stdin,sizeof(FILE),
+                                                  (void *)stdin,
+                                                  (void *)(& stdin));
     __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"__fc_stdin",
                                  (void *)stdin);
     __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
                                    "sizeof(FILE)",0,sizeof(FILE));
     __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
-                                 "\\valid(__fc_stdin)",0,
-                                 __gen_e_acsl_valid_3);
-    if (__gen_e_acsl_valid_3) {
+                                 "\\valid_read(__fc_stdin)",0,
+                                 __gen_e_acsl_valid_read);
+    if (__gen_e_acsl_valid_read) {
       int __gen_e_acsl_initialized_3;
       __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)stdin,
                                                         sizeof(FILE));
@@ -155,14 +156,14 @@ void *thread_start(void *arg)
     else __gen_e_acsl_and_3 = 0;
     __gen_e_acsl_assert_data_3.blocking = 1;
     __gen_e_acsl_assert_data_3.kind = "Assertion";
-    __gen_e_acsl_assert_data_3.pred_txt = "\\valid(__fc_stdin) && \\initialized(__fc_stdin)";
+    __gen_e_acsl_assert_data_3.pred_txt = "\\valid_read(__fc_stdin) && \\initialized(__fc_stdin)";
     __gen_e_acsl_assert_data_3.file = "threads_safe_locations.c";
     __gen_e_acsl_assert_data_3.fct = "thread_start";
     __gen_e_acsl_assert_data_3.line = 8;
     __e_acsl_assert(__gen_e_acsl_and_3,& __gen_e_acsl_assert_data_3);
     __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
   }
-  /*@ assert \valid(__fc_stdin) && \initialized(__fc_stdin); */ ;
+  /*@ assert \valid_read(__fc_stdin) && \initialized(__fc_stdin); */ ;
   int *addrof_errno = & errno;
   __e_acsl_store_block((void *)(& addrof_errno),8UL);
   __e_acsl_full_init((void *)(& addrof_errno));
@@ -182,8 +183,8 @@ void *thread_start(void *arg)
                                  "\\initialized(&addrof_errno)",0,
                                  __gen_e_acsl_initialized_4);
     if (__gen_e_acsl_initialized_4) {
-      int __gen_e_acsl_valid_4;
-      __gen_e_acsl_valid_4 = __e_acsl_valid((void *)addrof_errno,sizeof(int),
+      int __gen_e_acsl_valid_3;
+      __gen_e_acsl_valid_3 = __e_acsl_valid((void *)addrof_errno,sizeof(int),
                                             (void *)addrof_errno,
                                             (void *)(& addrof_errno));
       __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,
@@ -192,8 +193,8 @@ void *thread_start(void *arg)
                                      "sizeof(int)",0,sizeof(int));
       __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
                                    "\\valid(addrof_errno)",0,
-                                   __gen_e_acsl_valid_4);
-      __gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
+                                   __gen_e_acsl_valid_3);
+      __gen_e_acsl_and_4 = __gen_e_acsl_valid_3;
     }
     else __gen_e_acsl_and_4 = 0;
     if (__gen_e_acsl_and_4) {

src/plugins/e-acsl/tests/concurrency/threads_safe_locations.c

@@ -5,7 +5,7 @@
 void *thread_start(void *arg) {
   //@ assert \valid(stdout) && \initialized(stdout);
   //@ assert \valid(stderr) && \initialized(stderr);
-  //@ assert \valid(stdin) && \initialized(stdin);
+  //@ assert \valid_read(stdin) && \initialized(stdin);
   int *addrof_errno = &errno;
   //@ assert \valid(addrof_errno) && \initialized(addrof_errno);
   return NULL;

src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c

@@ -58,33 +58,34 @@ int main(void)
   }
   /*@ assert \valid(__fc_stderr); */ ;
   {
-    int __gen_e_acsl_valid_2;
+    int __gen_e_acsl_valid_read;
     __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
       {.values = (void *)0};
-    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stdin,sizeof(FILE),
-                                          (void *)stdin,(void *)(& stdin));
+    __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)stdin,sizeof(FILE),
+                                                  (void *)stdin,
+                                                  (void *)(& stdin));
     __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"__fc_stdin",
                                  (void *)stdin);
     __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
                                    "sizeof(FILE)",0,sizeof(FILE));
     __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
-                                 "\\valid(__fc_stdin)",0,
-                                 __gen_e_acsl_valid_2);
+                                 "\\valid_read(__fc_stdin)",0,
+                                 __gen_e_acsl_valid_read);
     __gen_e_acsl_assert_data_2.blocking = 1;
     __gen_e_acsl_assert_data_2.kind = "Assertion";
-    __gen_e_acsl_assert_data_2.pred_txt = "\\valid(__fc_stdin)";
+    __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(__fc_stdin)";
     __gen_e_acsl_assert_data_2.file = "stdout.c";
     __gen_e_acsl_assert_data_2.fct = "main";
     __gen_e_acsl_assert_data_2.line = 9;
-    __e_acsl_assert(__gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_2);
+    __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_2);
     __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
   }
-  /*@ assert \valid(__fc_stdin); */ ;
+  /*@ assert \valid_read(__fc_stdin); */ ;
   {
-    int __gen_e_acsl_valid_3;
+    int __gen_e_acsl_valid_2;
     __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
       {.values = (void *)0};
-    __gen_e_acsl_valid_3 = __e_acsl_valid((void *)stdout,sizeof(FILE),
+    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stdout,sizeof(FILE),
                                           (void *)stdout,(void *)(& stdout));
     __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"__fc_stdout",
                                  (void *)stdout);
@@ -92,14 +93,14 @@ int main(void)
                                    "sizeof(FILE)",0,sizeof(FILE));
     __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
                                  "\\valid(__fc_stdout)",0,
-                                 __gen_e_acsl_valid_3);
+                                 __gen_e_acsl_valid_2);
     __gen_e_acsl_assert_data_3.blocking = 1;
     __gen_e_acsl_assert_data_3.kind = "Assertion";
     __gen_e_acsl_assert_data_3.pred_txt = "\\valid(__fc_stdout)";
     __gen_e_acsl_assert_data_3.file = "stdout.c";
     __gen_e_acsl_assert_data_3.fct = "main";
     __gen_e_acsl_assert_data_3.line = 10;
-    __e_acsl_assert(__gen_e_acsl_valid_3,& __gen_e_acsl_assert_data_3);
+    __e_acsl_assert(__gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_3);
     __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
   }
   /*@ assert \valid(__fc_stdout); */ ;

src/plugins/e-acsl/tests/memory/stdout.c

@@ -6,7 +6,7 @@
 
 int main(void) {
   /*@assert \valid(stderr); */
-  /*@assert \valid(stdin); */
+  /*@assert \valid_read(stdin); */
   /*@assert \valid(stdout); */
   return 0;
 }