From e89f9539c41f0c50437225502a36a98b2e82e7ed Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 15 Sep 2023 11:47:17 +0200
Subject: [PATCH] [e-acsl] never monitor function pointers
---
.../e-acsl/src/analyses/memory_tracking.ml | 3 +
.../tests/bts/oracle/gen_issue-eacsl-91.c | 3 -
.../concurrency/oracle/gen_parallel_threads.c | 87 -------------------
.../oracle/gen_sequential_threads.c | 24 -----
.../concurrency/oracle/gen_threads_debug.c | 87 -------------------
.../oracle/gen_threads_safe_locations.c | 15 ----
.../tests/full-mtracking/oracle/gen_addrOf.c | 19 ----
.../e-acsl/tests/memory/oracle/gen_vdso.c | 6 --
.../e-acsl/tests/temporal/oracle/gen_t_fptr.c | 19 ----
9 files changed, 3 insertions(+), 260 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index ddc26d216b4..f4c318a3f63 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/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
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c
index fcc437fd3e6..1b33aaf3884 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
index c63e0856f11..6726aca133c 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_sequential_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_sequential_threads.c
index 08aa527836d..27941103b5c 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_sequential_threads.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
index 329f8afa81c..680fcfdaecb 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c
index 7b343fbdcb2..e1865e3750f 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c
index 5d2a9b181cc..818f2b0111b 100644
--- a/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vdso.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vdso.c
index 665134feeaa..1c80eb77fcb 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_vdso.c
+++ b/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));
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c
index 55cab83484e..e6f88bf1447 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c
+++ b/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;
}
--
GitLab