diff --git a/share/libc/__fc_define_pthread_types.h b/share/libc/__fc_define_pthread_types.h index d7be74b4d9d4bcfc5565d055002f92d70c256207..3e102d19894f21c048e0528be8cefd54c2c77254 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 7f656ff4aa67659c61002e0037cce0e3ea882059..c63e0856f119234bebfbb573d4b3d6f70b838f9e 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 ba28a676db6b9fb7449708c4eafb135d1741f684..08aa527836da75ff1801f7b3a1dec938dc19ad52 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 6a4c17bd9fe799e43e81072c64d4c02488159519..329f8afa81c9d07634f0b0efe4550a700cacb64d 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 3113cefa8b2f90ffb5b527648584b9295619fe39..2bb83096a37b444aaa320e4fa64a095c8e1e3c56 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 8bc8f679bba9a04c85d13e4e3d60bde10a6fa53b..b5874f1ef25baa4b60527857038a1a5052e3bc20 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;