[e-acsl] never monitor function pointers

src/plugins/e-acsl/src/analyses/memory_tracking.ml

@@ -39,6 +39,9 @@ let must_never_monitor vi =
   ||
   (* incomplete types cannot be properly monitored. See BTS #2406. *)
   not (Cil.isCompleteType vi.vtype)
+  ||
+  (* function pointers are not yet supported. *)
+  Cil.isFunctionType vi.vtype
 
 (* ********************************************************************** *)
 (* Backward dataflow analysis to compute a sound over-approximation of what

src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c

@@ -38,8 +38,6 @@ void __e_acsl_globals_init(void)
   static char __e_acsl_already_run = 0;
   if (! __e_acsl_already_run) {
     __e_acsl_already_run = 1;
-    __e_acsl_store_block((void *)(& b),1UL);
-    __e_acsl_full_init((void *)(& b));
     __e_acsl_store_block((void *)(& a),2UL);
     __e_acsl_full_init((void *)(& a));
   }
@@ -48,7 +46,6 @@ void __e_acsl_globals_init(void)
 
 void __e_acsl_globals_clean(void)
 {
-  __e_acsl_delete_block((void *)(& b));
   __e_acsl_delete_block((void *)(& a));
   return;
 }

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

@@ -1647,36 +1647,6 @@ void __e_acsl_globals_init(void)
                          sizeof("Unable to broadcast to read cond var"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
-    __e_acsl_store_block((void *)(& __gen_e_acsl_read_value),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_read_value));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_write_value),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_write_value));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_usleep),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_usleep));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_exit),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_perror),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_perror));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_mutex_unlock),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_mutex_unlock));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_mutex_lock),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_mutex_lock));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_mutex_init),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_mutex_init));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_join),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_join));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_create),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_create));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_cond_wait),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_cond_wait));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_cond_init),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_cond_init));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_cond_broadcast),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_cond_broadcast));
-    __e_acsl_store_block((void *)(& read_value),1UL);
-    __e_acsl_full_init((void *)(& read_value));
-    __e_acsl_store_block((void *)(& write_value),1UL);
-    __e_acsl_full_init((void *)(& write_value));
     __e_acsl_store_block((void *)(& read_mutex),4UL);
     __e_acsl_full_init((void *)(& read_mutex));
     __e_acsl_store_block((void *)(& write_mutex),4UL);
@@ -1691,20 +1661,12 @@ void __e_acsl_globals_init(void)
     __e_acsl_full_init((void *)(& write_count));
     __e_acsl_store_block((void *)(values),80UL);
     __e_acsl_full_init((void *)(& values));
-    __e_acsl_store_block((void *)(& usleep),1UL);
-    __e_acsl_full_init((void *)(& usleep));
     __e_acsl_store_block((void *)(& __fc_p_ttyname),8UL);
     __e_acsl_full_init((void *)(& __fc_p_ttyname));
     __e_acsl_store_block((void *)(ttyname),32UL);
     __e_acsl_full_init((void *)(& ttyname));
     __e_acsl_store_block((void *)(& Frama_C_entropy_source),4UL);
     __e_acsl_full_init((void *)(& Frama_C_entropy_source));
-    __e_acsl_store_block((void *)(& exit),1UL);
-    __e_acsl_full_init((void *)(& exit));
-    __e_acsl_store_block((void *)(& free),1UL);
-    __e_acsl_full_init((void *)(& free));
-    __e_acsl_store_block((void *)(& malloc),1UL);
-    __e_acsl_full_init((void *)(& malloc));
     __e_acsl_store_block((void *)(& __fc_p_random48_counter),8UL);
     __e_acsl_full_init((void *)(& __fc_p_random48_counter));
     __e_acsl_store_block((void *)(random48_counter),6UL);
@@ -1713,8 +1675,6 @@ void __e_acsl_globals_init(void)
     __e_acsl_full_init((void *)(& __fc_random48_init));
     __e_acsl_store_block((void *)(& __fc_rand_max),8UL);
     __e_acsl_full_init((void *)(& __fc_rand_max));
-    __e_acsl_store_block((void *)(& perror),1UL);
-    __e_acsl_full_init((void *)(& perror));
     __e_acsl_store_block((void *)(& __fc_p_tmpnam),8UL);
     __e_acsl_full_init((void *)(& __fc_p_tmpnam));
     __e_acsl_store_block((void *)(__fc_tmpnam),20UL);
@@ -1743,24 +1703,6 @@ void __e_acsl_globals_init(void)
     __e_acsl_full_init((void *)(& __fc_p_sigaction));
     __e_acsl_store_block((void *)(sigaction),2080UL);
     __e_acsl_full_init((void *)(& sigaction));
-    __e_acsl_store_block((void *)(& pthread_mutex_unlock),1UL);
-    __e_acsl_full_init((void *)(& pthread_mutex_unlock));
-    __e_acsl_store_block((void *)(& pthread_mutex_trylock),1UL);
-    __e_acsl_full_init((void *)(& pthread_mutex_trylock));
-    __e_acsl_store_block((void *)(& pthread_mutex_lock),1UL);
-    __e_acsl_full_init((void *)(& pthread_mutex_lock));
-    __e_acsl_store_block((void *)(& pthread_mutex_init),1UL);
-    __e_acsl_full_init((void *)(& pthread_mutex_init));
-    __e_acsl_store_block((void *)(& pthread_join),1UL);
-    __e_acsl_full_init((void *)(& pthread_join));
-    __e_acsl_store_block((void *)(& pthread_create),1UL);
-    __e_acsl_full_init((void *)(& pthread_create));
-    __e_acsl_store_block((void *)(& pthread_cond_wait),1UL);
-    __e_acsl_full_init((void *)(& pthread_cond_wait));
-    __e_acsl_store_block((void *)(& pthread_cond_init),1UL);
-    __e_acsl_full_init((void *)(& pthread_cond_init));
-    __e_acsl_store_block((void *)(& pthread_cond_broadcast),1UL);
-    __e_acsl_full_init((void *)(& pthread_cond_broadcast));
     __e_acsl_store_block((void *)(& errno),4UL);
     __e_acsl_full_init((void *)(& errno));
   }
@@ -1769,21 +1711,6 @@ void __e_acsl_globals_init(void)
 
 void __e_acsl_globals_clean(void)
 {
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_read_value));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_write_value));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_usleep));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_exit));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_perror));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_mutex_unlock));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_mutex_lock));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_mutex_init));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_join));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_create));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_cond_wait));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_cond_init));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_cond_broadcast));
-  __e_acsl_delete_block((void *)(& read_value));
-  __e_acsl_delete_block((void *)(& write_value));
   __e_acsl_delete_block((void *)(& read_mutex));
   __e_acsl_delete_block((void *)(& write_mutex));
   __e_acsl_delete_block((void *)(& read_cond));
@@ -1791,18 +1718,13 @@ void __e_acsl_globals_clean(void)
   __e_acsl_delete_block((void *)(& read_count));
   __e_acsl_delete_block((void *)(& write_count));
   __e_acsl_delete_block((void *)(values));
-  __e_acsl_delete_block((void *)(& usleep));
   __e_acsl_delete_block((void *)(& __fc_p_ttyname));
   __e_acsl_delete_block((void *)(ttyname));
   __e_acsl_delete_block((void *)(& Frama_C_entropy_source));
-  __e_acsl_delete_block((void *)(& exit));
-  __e_acsl_delete_block((void *)(& free));
-  __e_acsl_delete_block((void *)(& malloc));
   __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
   __e_acsl_delete_block((void *)(random48_counter));
   __e_acsl_delete_block((void *)(& __fc_random48_init));
   __e_acsl_delete_block((void *)(& __fc_rand_max));
-  __e_acsl_delete_block((void *)(& perror));
   __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
   __e_acsl_delete_block((void *)(__fc_tmpnam));
   __e_acsl_delete_block((void *)(& __fc_p_fopen));
@@ -1817,15 +1739,6 @@ void __e_acsl_globals_clean(void)
   __e_acsl_delete_block((void *)(& __fc_time));
   __e_acsl_delete_block((void *)(& __fc_p_sigaction));
   __e_acsl_delete_block((void *)(sigaction));
-  __e_acsl_delete_block((void *)(& pthread_mutex_unlock));
-  __e_acsl_delete_block((void *)(& pthread_mutex_trylock));
-  __e_acsl_delete_block((void *)(& pthread_mutex_lock));
-  __e_acsl_delete_block((void *)(& pthread_mutex_init));
-  __e_acsl_delete_block((void *)(& pthread_join));
-  __e_acsl_delete_block((void *)(& pthread_create));
-  __e_acsl_delete_block((void *)(& pthread_cond_wait));
-  __e_acsl_delete_block((void *)(& pthread_cond_init));
-  __e_acsl_delete_block((void *)(& pthread_cond_broadcast));
   __e_acsl_delete_block((void *)(& errno));
   return;
 }

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

@@ -435,20 +435,8 @@ void __e_acsl_globals_init(void)
   static char __e_acsl_already_run = 0;
   if (! __e_acsl_already_run) {
     __e_acsl_already_run = 1;
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_join),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_join));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_create),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_create));
-    __e_acsl_store_block((void *)(& read_value),1UL);
-    __e_acsl_full_init((void *)(& read_value));
-    __e_acsl_store_block((void *)(& write_value),1UL);
-    __e_acsl_full_init((void *)(& write_value));
     __e_acsl_store_block((void *)(values),80UL);
     __e_acsl_full_init((void *)(& values));
-    __e_acsl_store_block((void *)(& free),1UL);
-    __e_acsl_full_init((void *)(& free));
-    __e_acsl_store_block((void *)(& malloc),1UL);
-    __e_acsl_full_init((void *)(& malloc));
     __e_acsl_store_block((void *)(& __fc_p_random48_counter),8UL);
     __e_acsl_full_init((void *)(& __fc_p_random48_counter));
     __e_acsl_store_block((void *)(random48_counter),6UL);
@@ -473,23 +461,13 @@ void __e_acsl_globals_init(void)
     __e_acsl_full_init((void *)(& __fc_p_sigaction));
     __e_acsl_store_block((void *)(sigaction),2080UL);
     __e_acsl_full_init((void *)(& sigaction));
-    __e_acsl_store_block((void *)(& pthread_join),1UL);
-    __e_acsl_full_init((void *)(& pthread_join));
-    __e_acsl_store_block((void *)(& pthread_create),1UL);
-    __e_acsl_full_init((void *)(& pthread_create));
   }
   return;
 }
 
 void __e_acsl_globals_clean(void)
 {
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_join));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_create));
-  __e_acsl_delete_block((void *)(& read_value));
-  __e_acsl_delete_block((void *)(& write_value));
   __e_acsl_delete_block((void *)(values));
-  __e_acsl_delete_block((void *)(& free));
-  __e_acsl_delete_block((void *)(& malloc));
   __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
   __e_acsl_delete_block((void *)(random48_counter));
   __e_acsl_delete_block((void *)(& __fc_random48_init));
@@ -502,8 +480,6 @@ void __e_acsl_globals_clean(void)
   __e_acsl_delete_block((void *)(& __fc_time));
   __e_acsl_delete_block((void *)(& __fc_p_sigaction));
   __e_acsl_delete_block((void *)(sigaction));
-  __e_acsl_delete_block((void *)(& pthread_join));
-  __e_acsl_delete_block((void *)(& pthread_create));
   return;
 }
 

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

@@ -1329,36 +1329,6 @@ void __e_acsl_globals_init(void)
                          sizeof("Unable to broadcast to read cond var"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
-    __e_acsl_store_block((void *)(& __gen_e_acsl_read_value),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_read_value));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_write_value),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_write_value));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_usleep),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_usleep));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_exit),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_perror),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_perror));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_mutex_unlock),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_mutex_unlock));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_mutex_lock),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_mutex_lock));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_mutex_init),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_mutex_init));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_join),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_join));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_create),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_create));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_cond_wait),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_cond_wait));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_cond_init),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_cond_init));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_cond_broadcast),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_cond_broadcast));
-    __e_acsl_store_block((void *)(& read_value),1UL);
-    __e_acsl_full_init((void *)(& read_value));
-    __e_acsl_store_block((void *)(& write_value),1UL);
-    __e_acsl_full_init((void *)(& write_value));
     __e_acsl_store_block((void *)(& read_mutex),4UL);
     __e_acsl_full_init((void *)(& read_mutex));
     __e_acsl_store_block((void *)(& write_mutex),4UL);
@@ -1373,20 +1343,12 @@ void __e_acsl_globals_init(void)
     __e_acsl_full_init((void *)(& write_count));
     __e_acsl_store_block((void *)(values),80UL);
     __e_acsl_full_init((void *)(& values));
-    __e_acsl_store_block((void *)(& usleep),1UL);
-    __e_acsl_full_init((void *)(& usleep));
     __e_acsl_store_block((void *)(& __fc_p_ttyname),8UL);
     __e_acsl_full_init((void *)(& __fc_p_ttyname));
     __e_acsl_store_block((void *)(ttyname),32UL);
     __e_acsl_full_init((void *)(& ttyname));
     __e_acsl_store_block((void *)(& Frama_C_entropy_source),4UL);
     __e_acsl_full_init((void *)(& Frama_C_entropy_source));
-    __e_acsl_store_block((void *)(& exit),1UL);
-    __e_acsl_full_init((void *)(& exit));
-    __e_acsl_store_block((void *)(& free),1UL);
-    __e_acsl_full_init((void *)(& free));
-    __e_acsl_store_block((void *)(& malloc),1UL);
-    __e_acsl_full_init((void *)(& malloc));
     __e_acsl_store_block((void *)(& __fc_p_random48_counter),8UL);
     __e_acsl_full_init((void *)(& __fc_p_random48_counter));
     __e_acsl_store_block((void *)(random48_counter),6UL);
@@ -1395,8 +1357,6 @@ void __e_acsl_globals_init(void)
     __e_acsl_full_init((void *)(& __fc_random48_init));
     __e_acsl_store_block((void *)(& __fc_rand_max),8UL);
     __e_acsl_full_init((void *)(& __fc_rand_max));
-    __e_acsl_store_block((void *)(& perror),1UL);
-    __e_acsl_full_init((void *)(& perror));
     __e_acsl_store_block((void *)(& __fc_p_tmpnam),8UL);
     __e_acsl_full_init((void *)(& __fc_p_tmpnam));
     __e_acsl_store_block((void *)(__fc_tmpnam),20UL);
@@ -1425,24 +1385,6 @@ void __e_acsl_globals_init(void)
     __e_acsl_full_init((void *)(& __fc_p_sigaction));
     __e_acsl_store_block((void *)(sigaction),2080UL);
     __e_acsl_full_init((void *)(& sigaction));
-    __e_acsl_store_block((void *)(& pthread_mutex_unlock),1UL);
-    __e_acsl_full_init((void *)(& pthread_mutex_unlock));
-    __e_acsl_store_block((void *)(& pthread_mutex_trylock),1UL);
-    __e_acsl_full_init((void *)(& pthread_mutex_trylock));
-    __e_acsl_store_block((void *)(& pthread_mutex_lock),1UL);
-    __e_acsl_full_init((void *)(& pthread_mutex_lock));
-    __e_acsl_store_block((void *)(& pthread_mutex_init),1UL);
-    __e_acsl_full_init((void *)(& pthread_mutex_init));
-    __e_acsl_store_block((void *)(& pthread_join),1UL);
-    __e_acsl_full_init((void *)(& pthread_join));
-    __e_acsl_store_block((void *)(& pthread_create),1UL);
-    __e_acsl_full_init((void *)(& pthread_create));
-    __e_acsl_store_block((void *)(& pthread_cond_wait),1UL);
-    __e_acsl_full_init((void *)(& pthread_cond_wait));
-    __e_acsl_store_block((void *)(& pthread_cond_init),1UL);
-    __e_acsl_full_init((void *)(& pthread_cond_init));
-    __e_acsl_store_block((void *)(& pthread_cond_broadcast),1UL);
-    __e_acsl_full_init((void *)(& pthread_cond_broadcast));
     __e_acsl_store_block((void *)(& errno),4UL);
     __e_acsl_full_init((void *)(& errno));
   }
@@ -1451,21 +1393,6 @@ void __e_acsl_globals_init(void)
 
 void __e_acsl_globals_clean(void)
 {
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_read_value));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_write_value));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_usleep));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_exit));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_perror));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_mutex_unlock));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_mutex_lock));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_mutex_init));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_join));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_create));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_cond_wait));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_cond_init));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_cond_broadcast));
-  __e_acsl_delete_block((void *)(& read_value));
-  __e_acsl_delete_block((void *)(& write_value));
   __e_acsl_delete_block((void *)(& read_mutex));
   __e_acsl_delete_block((void *)(& write_mutex));
   __e_acsl_delete_block((void *)(& read_cond));
@@ -1473,18 +1400,13 @@ void __e_acsl_globals_clean(void)
   __e_acsl_delete_block((void *)(& read_count));
   __e_acsl_delete_block((void *)(& write_count));
   __e_acsl_delete_block((void *)(values));
-  __e_acsl_delete_block((void *)(& usleep));
   __e_acsl_delete_block((void *)(& __fc_p_ttyname));
   __e_acsl_delete_block((void *)(ttyname));
   __e_acsl_delete_block((void *)(& Frama_C_entropy_source));
-  __e_acsl_delete_block((void *)(& exit));
-  __e_acsl_delete_block((void *)(& free));
-  __e_acsl_delete_block((void *)(& malloc));
   __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
   __e_acsl_delete_block((void *)(random48_counter));
   __e_acsl_delete_block((void *)(& __fc_random48_init));
   __e_acsl_delete_block((void *)(& __fc_rand_max));
-  __e_acsl_delete_block((void *)(& perror));
   __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
   __e_acsl_delete_block((void *)(__fc_tmpnam));
   __e_acsl_delete_block((void *)(& __fc_p_fopen));
@@ -1499,15 +1421,6 @@ void __e_acsl_globals_clean(void)
   __e_acsl_delete_block((void *)(& __fc_time));
   __e_acsl_delete_block((void *)(& __fc_p_sigaction));
   __e_acsl_delete_block((void *)(sigaction));
-  __e_acsl_delete_block((void *)(& pthread_mutex_unlock));
-  __e_acsl_delete_block((void *)(& pthread_mutex_trylock));
-  __e_acsl_delete_block((void *)(& pthread_mutex_lock));
-  __e_acsl_delete_block((void *)(& pthread_mutex_init));
-  __e_acsl_delete_block((void *)(& pthread_join));
-  __e_acsl_delete_block((void *)(& pthread_create));
-  __e_acsl_delete_block((void *)(& pthread_cond_wait));
-  __e_acsl_delete_block((void *)(& pthread_cond_init));
-  __e_acsl_delete_block((void *)(& pthread_cond_broadcast));
   __e_acsl_delete_block((void *)(& errno));
   return;
 }

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

@@ -485,12 +485,6 @@ void __e_acsl_globals_init(void)
   static char __e_acsl_already_run = 0;
   if (! __e_acsl_already_run) {
     __e_acsl_already_run = 1;
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_join),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_join));
-    __e_acsl_store_block((void *)(& __gen_e_acsl_pthread_create),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_pthread_create));
-    __e_acsl_store_block((void *)(& thread_start),1UL);
-    __e_acsl_full_init((void *)(& thread_start));
     __e_acsl_store_block((void *)(& __fc_p_tmpnam),8UL);
     __e_acsl_full_init((void *)(& __fc_p_tmpnam));
     __e_acsl_store_block((void *)(__fc_tmpnam),20UL);
@@ -521,10 +515,6 @@ void __e_acsl_globals_init(void)
     __e_acsl_full_init((void *)(& __fc_p_sigaction));
     __e_acsl_store_block((void *)(sigaction),2080UL);
     __e_acsl_full_init((void *)(& sigaction));
-    __e_acsl_store_block((void *)(& pthread_join),1UL);
-    __e_acsl_full_init((void *)(& pthread_join));
-    __e_acsl_store_block((void *)(& pthread_create),1UL);
-    __e_acsl_full_init((void *)(& pthread_create));
     __e_acsl_store_block((void *)(& errno),4UL);
     __e_acsl_full_init((void *)(& errno));
   }
@@ -533,9 +523,6 @@ void __e_acsl_globals_init(void)
 
 void __e_acsl_globals_clean(void)
 {
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_join));
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_pthread_create));
-  __e_acsl_delete_block((void *)(& thread_start));
   __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
   __e_acsl_delete_block((void *)(__fc_tmpnam));
   __e_acsl_delete_block((void *)(& __fc_p_fopen));
@@ -551,8 +538,6 @@ void __e_acsl_globals_clean(void)
   __e_acsl_delete_block((void *)(& __fc_time));
   __e_acsl_delete_block((void *)(& __fc_p_sigaction));
   __e_acsl_delete_block((void *)(sigaction));
-  __e_acsl_delete_block((void *)(& pthread_join));
-  __e_acsl_delete_block((void *)(& pthread_create));
   __e_acsl_delete_block((void *)(& errno));
   return;
 }

src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c

@@ -48,28 +48,10 @@ void f(void)
   return;
 }
 
-void __e_acsl_globals_init(void)
-{
-  static char __e_acsl_already_run = 0;
-  if (! __e_acsl_already_run) {
-    __e_acsl_already_run = 1;
-    __e_acsl_store_block((void *)(& f),1UL);
-    __e_acsl_full_init((void *)(& f));
-  }
-  return;
-}
-
-void __e_acsl_globals_clean(void)
-{
-  __e_acsl_delete_block((void *)(& f));
-  return;
-}
-
 int main(void)
 {
   int __retres;
   __e_acsl_memory_init((int *)0,(char ***)0,8UL);
-  __e_acsl_globals_init();
   __e_acsl_store_block((void *)(& __retres),4UL);
   int x = 0;
   __e_acsl_store_block((void *)(& x),4UL);
@@ -95,7 +77,6 @@ int main(void)
   __retres = 0;
   __e_acsl_delete_block((void *)(& x));
   __e_acsl_delete_block((void *)(& __retres));
-  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

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

@@ -157,8 +157,6 @@ void __e_acsl_globals_init(void)
   static char __e_acsl_already_run = 0;
   if (! __e_acsl_already_run) {
     __e_acsl_already_run = 1;
-    __e_acsl_store_block((void *)(& __gen_e_acsl_time),1UL);
-    __e_acsl_full_init((void *)(& __gen_e_acsl_time));
     __e_acsl_store_block((void *)(& __fc_interrupted),4UL);
     __e_acsl_full_init((void *)(& __fc_interrupted));
     __e_acsl_store_block((void *)(& __fc_p_time_tm),8UL);
@@ -169,8 +167,6 @@ void __e_acsl_globals_init(void)
     __e_acsl_full_init((void *)(& __fc_p_ctime));
     __e_acsl_store_block((void *)(__fc_ctime),26UL);
     __e_acsl_full_init((void *)(& __fc_ctime));
-    __e_acsl_store_block((void *)(& time),1UL);
-    __e_acsl_full_init((void *)(& time));
     __e_acsl_store_block((void *)(& __fc_time),4UL);
     __e_acsl_full_init((void *)(& __fc_time));
     __e_acsl_store_block((void *)(& __fc_p_sigaction),8UL);
@@ -183,13 +179,11 @@ void __e_acsl_globals_init(void)
 
 void __e_acsl_globals_clean(void)
 {
-  __e_acsl_delete_block((void *)(& __gen_e_acsl_time));
   __e_acsl_delete_block((void *)(& __fc_interrupted));
   __e_acsl_delete_block((void *)(& __fc_p_time_tm));
   __e_acsl_delete_block((void *)(& __fc_time_tm));
   __e_acsl_delete_block((void *)(& __fc_p_ctime));
   __e_acsl_delete_block((void *)(__fc_ctime));
-  __e_acsl_delete_block((void *)(& time));
   __e_acsl_delete_block((void *)(& __fc_time));
   __e_acsl_delete_block((void *)(& __fc_p_sigaction));
   __e_acsl_delete_block((void *)(sigaction));

src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c

@@ -14,29 +14,11 @@ int *foo(int *p)
   return q;
 }
 
-void __e_acsl_globals_init(void)
-{
-  static char __e_acsl_already_run = 0;
-  if (! __e_acsl_already_run) {
-    __e_acsl_already_run = 1;
-    __e_acsl_store_block((void *)(& foo),1UL);
-    __e_acsl_full_init((void *)(& foo));
-  }
-  return;
-}
-
-void __e_acsl_globals_clean(void)
-{
-  __e_acsl_delete_block((void *)(& foo));
-  return;
-}
-
 int main(int argc, char const **argv)
 {
   int __retres;
   int *q;
   __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
-  __e_acsl_globals_init();
   __e_acsl_store_block((void *)(& q),8UL);
   int *p = & argc;
   __e_acsl_temporal_store_nblock((void *)(& p),(void *)(& argc));
@@ -98,7 +80,6 @@ int main(int argc, char const **argv)
   __e_acsl_delete_block((void *)(& fp));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& p));
-  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }