From 7528a3ef44c78dfc878ff2e3e44652e89c985022 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 29 Mar 2024 09:51:57 +0000
Subject: [PATCH] [libc] variants of pthread_t have a coherent size
---
share/libc/__fc_define_pthread_types.h | 2 +-
.../e-acsl/tests/concurrency/oracle/gen_parallel_threads.c | 6 +++---
.../tests/concurrency/oracle/gen_sequential_threads.c | 4 ++--
.../e-acsl/tests/concurrency/oracle/gen_threads_debug.c | 6 +++---
.../tests/concurrency/oracle/gen_threads_safe_locations.c | 4 ++--
tests/libc/oracle/fc_libc.1.res.oracle | 2 +-
6 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/share/libc/__fc_define_pthread_types.h b/share/libc/__fc_define_pthread_types.h
index d7be74b4d9d..3e102d19894 100644
--- a/share/libc/__fc_define_pthread_types.h
+++ b/share/libc/__fc_define_pthread_types.h
@@ -50,7 +50,7 @@ typedef struct __fc_pthread_spinlock_t { int _fc; } pthread_spinlock_t;
// such code to be parsed.
typedef unsigned long pthread_t;
#else
-typedef struct __fc_pthread_t { int _fc; } pthread_t;
+typedef struct __fc_pthread_t { unsigned long _fc; } pthread_t;
#endif
__END_DECLS
__POP_FC_STDLIB
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 7f656ff4aa6..c63e0856f11 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
@@ -1103,7 +1103,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
int __gen_e_acsl_or;
int __gen_e_acsl_valid_2;
__e_acsl_store_block((void *)(& retval),8UL);
- __e_acsl_store_block((void *)(& thread),4UL);
+ __e_acsl_store_block((void *)(& thread),8UL);
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"retval",
@@ -1851,8 +1851,8 @@ int main(void)
__e_acsl_store_block((void *)(& tmp_0),4UL);
__e_acsl_store_block((void *)(& tmp),4UL);
__e_acsl_store_block((void *)(args),40UL);
- __e_acsl_store_block((void *)(readers),40UL);
- __e_acsl_store_block((void *)(writers),40UL);
+ __e_acsl_store_block((void *)(readers),80UL);
+ __e_acsl_store_block((void *)(writers),80UL);
__e_acsl_store_block((void *)(& __retres),4UL);
__e_acsl_full_init((void *)(& tmp));
tmp = __gen_e_acsl_pthread_mutex_init(& write_mutex,
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 ba28a676db6..08aa527836d 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
@@ -207,7 +207,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
int __gen_e_acsl_or;
int __gen_e_acsl_valid_2;
__e_acsl_store_block((void *)(& retval),8UL);
- __e_acsl_store_block((void *)(& thread),4UL);
+ __e_acsl_store_block((void *)(& thread),8UL);
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"retval",
@@ -515,7 +515,7 @@ int main(void)
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
__e_acsl_store_block((void *)(args),40UL);
- __e_acsl_store_block((void *)(& t),4UL);
+ __e_acsl_store_block((void *)(& t),8UL);
__e_acsl_store_block((void *)(& __retres),4UL);
{
int i = 0;
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 6a4c17bd9fe..329f8afa81c 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
@@ -785,7 +785,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
int __gen_e_acsl_or;
int __gen_e_acsl_valid_2;
__e_acsl_store_block((void *)(& retval),8UL);
- __e_acsl_store_block((void *)(& thread),4UL);
+ __e_acsl_store_block((void *)(& thread),8UL);
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"retval",
@@ -1533,8 +1533,8 @@ int main(void)
__e_acsl_store_block((void *)(& tmp_0),4UL);
__e_acsl_store_block((void *)(& tmp),4UL);
__e_acsl_store_block((void *)(args),40UL);
- __e_acsl_store_block((void *)(readers),40UL);
- __e_acsl_store_block((void *)(writers),40UL);
+ __e_acsl_store_block((void *)(readers),80UL);
+ __e_acsl_store_block((void *)(writers),80UL);
__e_acsl_store_block((void *)(& __retres),4UL);
__e_acsl_full_init((void *)(& tmp));
tmp = __gen_e_acsl_pthread_mutex_init(& write_mutex,
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 3113cefa8b2..2bb83096a37 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
@@ -256,7 +256,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
int __gen_e_acsl_or;
int __gen_e_acsl_valid_2;
__e_acsl_store_block((void *)(& retval),8UL);
- __e_acsl_store_block((void *)(& thread),4UL);
+ __e_acsl_store_block((void *)(& thread),8UL);
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"retval",
@@ -562,7 +562,7 @@ int main(void)
pthread_t t;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& t),4UL);
+ __e_acsl_store_block((void *)(& t),8UL);
__e_acsl_store_block((void *)(& __retres),4UL);
__gen_e_acsl_pthread_create(& t,(pthread_attr_t const *)0,& thread_start,
(void *)0);
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 8bc8f679bba..b5874f1ef25 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -113,7 +113,7 @@ struct __fc_pthread_mutexattr_t {
};
typedef struct __fc_pthread_mutexattr_t pthread_mutexattr_t;
struct __fc_pthread_t {
- int _fc ;
+ unsigned long _fc ;
};
typedef struct __fc_pthread_t pthread_t;
typedef int pid_t;
--
GitLab