From d9ba9820fd166755a808a7e9307ef61e15fb2683 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 12 Sep 2024 09:18:25 +0200
Subject: [PATCH] update test oracles
---
.../concurrency/oracle/gen_parallel_threads.c | 69 +++++++++-----
.../oracle/gen_sequential_threads.c | 12 +--
.../concurrency/oracle/gen_threads_debug.c | 69 +++++++++-----
.../oracle/gen_threads_safe_locations.c | 12 +--
.../oracle/parallel_threads.res.oracle | 95 ++++++++++---------
.../oracle/sequential_threads.res.oracle | 36 +++----
.../oracle/threads_debug.res.oracle | 95 ++++++++++---------
.../oracle/threads_safe_locations.res.oracle | 30 +++---
tests/builtins/oracle/memcpy.0.res.oracle | 69 ++++++++++++--
tests/libc/oracle/argz_c.res.oracle | 2 +
tests/libc/oracle/coverage.res.oracle | 2 +-
tests/libc/oracle/fc_libc.0.res.oracle | 9 +-
tests/libc/oracle/fc_libc.2.res.oracle | 1 +
tests/libc/oracle/fc_libc.4.res.oracle | 2 +-
tests/libc/oracle/netdb_c.res.oracle | 13 +++
tests/libc/oracle/signal_h.res.oracle | 2 +-
tests/libc/oracle/spawn_h.res.oracle | 24 -----
17 files changed, 322 insertions(+), 220 deletions(-)
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 b6071854f7c..27f2d290b54 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
@@ -113,6 +113,12 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
*/
int __gen_e_acsl_pthread_mutex_lock(pthread_mutex_t *mutex);
+/*@ assigns \result, *mutex;
+ assigns \result \from *mutex;
+ assigns *mutex \from *mutex;
+ */
+int __gen_e_acsl_pthread_mutex_trylock(pthread_mutex_t *mutex);
+
/*@ requires mutex_valid: \valid(mutex);
ensures success_or_error: \result == 0 || \result == 1;
assigns *mutex, \result;
@@ -828,7 +834,7 @@ int __gen_e_acsl_pthread_mutex_unlock(pthread_mutex_t *mutex)
__gen_e_acsl_assert_data.pred_txt = "\\valid(mutex)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_mutex_unlock";
- __gen_e_acsl_assert_data.line = 313;
+ __gen_e_acsl_assert_data.line = 499;
__gen_e_acsl_assert_data.name = "mutex_valid";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -851,7 +857,7 @@ int __gen_e_acsl_pthread_mutex_unlock(pthread_mutex_t *mutex)
__gen_e_acsl_assert_data_2.pred_txt = "\\result == 0 || \\result == 1";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_mutex_unlock";
- __gen_e_acsl_assert_data_2.line = 316;
+ __gen_e_acsl_assert_data_2.line = 502;
__gen_e_acsl_assert_data_2.name = "success_or_error";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -861,6 +867,21 @@ int __gen_e_acsl_pthread_mutex_unlock(pthread_mutex_t *mutex)
}
}
+/*@ assigns \result, *mutex;
+ assigns \result \from *mutex;
+ assigns *mutex \from *mutex;
+ */
+int __gen_e_acsl_pthread_mutex_trylock(pthread_mutex_t *mutex)
+{
+ int __retres;
+ __e_acsl_store_block((void *)(& __retres),4UL);
+ __e_acsl_store_block((void *)(& mutex),8UL);
+ __retres = pthread_mutex_trylock(mutex);
+ __e_acsl_delete_block((void *)(& mutex));
+ __e_acsl_delete_block((void *)(& __retres));
+ return __retres;
+}
+
/*@ requires mutex_valid: \valid(mutex);
ensures
success_or_error:
@@ -892,7 +913,7 @@ int __gen_e_acsl_pthread_mutex_lock(pthread_mutex_t *mutex)
__gen_e_acsl_assert_data.pred_txt = "\\valid(mutex)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_mutex_lock";
- __gen_e_acsl_assert_data.line = 295;
+ __gen_e_acsl_assert_data.line = 467;
__gen_e_acsl_assert_data.name = "mutex_valid";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -929,7 +950,7 @@ int __gen_e_acsl_pthread_mutex_lock(pthread_mutex_t *mutex)
__gen_e_acsl_assert_data_2.pred_txt = "\\result == 0 || \\result == 11 || \\result == 22 || \\result == 35";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_mutex_lock";
- __gen_e_acsl_assert_data_2.line = 299;
+ __gen_e_acsl_assert_data_2.line = 471;
__gen_e_acsl_assert_data_2.name = "success_or_error";
__e_acsl_assert(__gen_e_acsl_or_3,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -977,7 +998,7 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
__gen_e_acsl_assert_data.pred_txt = "\\valid(mutex)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_mutex_init";
- __gen_e_acsl_assert_data.line = 279;
+ __gen_e_acsl_assert_data.line = 451;
__gen_e_acsl_assert_data.name = "mutex_valid";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -1007,7 +1028,7 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
__gen_e_acsl_assert_data_2.pred_txt = "attrs == \\null || \\valid_read(attrs)";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_mutex_init";
- __gen_e_acsl_assert_data_2.line = 280;
+ __gen_e_acsl_assert_data_2.line = 452;
__gen_e_acsl_assert_data_2.name = "attrs_valid_or_null";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -1067,7 +1088,7 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
__gen_e_acsl_assert_data_3.pred_txt = "(\\result == 0 && \\initialized(\\old(mutex))) || \\result == 11 || \\result == 12 ||\n\\result == 1 || \\result == 22";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_3.fct = "pthread_mutex_init";
- __gen_e_acsl_assert_data_3.line = 285;
+ __gen_e_acsl_assert_data_3.line = 457;
__gen_e_acsl_assert_data_3.name = "initialization/success_or_error";
__e_acsl_assert(__gen_e_acsl_or_5,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
@@ -1129,7 +1150,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
__gen_e_acsl_assert_data.pred_txt = "retval == \\null || \\valid(retval)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_join";
- __gen_e_acsl_assert_data.line = 247;
+ __gen_e_acsl_assert_data.line = 405;
__gen_e_acsl_assert_data.name = "valid_or_null_retval";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -1172,7 +1193,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
__gen_e_acsl_assert_data_2.pred_txt = "\\result == 0 || \\result == 35 || \\result == 22 || \\result == 3";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_join";
- __gen_e_acsl_assert_data_2.line = 251;
+ __gen_e_acsl_assert_data_2.line = 409;
__gen_e_acsl_assert_data_2.name = "success_or_error";
__e_acsl_assert(__gen_e_acsl_or_4,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -1227,7 +1248,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data.pred_txt = "\\valid(thread)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_create";
- __gen_e_acsl_assert_data.line = 223;
+ __gen_e_acsl_assert_data.line = 355;
__gen_e_acsl_assert_data.name = "valid_thread";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -1257,7 +1278,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_2.pred_txt = "attr == \\null || \\valid_read(attr)";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_create";
- __gen_e_acsl_assert_data_2.line = 224;
+ __gen_e_acsl_assert_data_2.line = 356;
__gen_e_acsl_assert_data_2.name = "valid_null_attr";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -1282,7 +1303,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_4.pred_txt = "arg == \\null || \\valid((char *)arg)";
__gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_4.fct = "pthread_create";
- __gen_e_acsl_assert_data_4.line = 226;
+ __gen_e_acsl_assert_data_4.line = 358;
__gen_e_acsl_assert_data_4.name = "valid_null_arg";
__e_acsl_assert(__gen_e_acsl_or_2,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -1334,7 +1355,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_5.pred_txt = "(\\result == 0 && \\initialized(\\old(thread))) || \\result == 11 ||\n\\result == 22 || \\result == 1";
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_5.fct = "pthread_create";
- __gen_e_acsl_assert_data_5.line = 230;
+ __gen_e_acsl_assert_data_5.line = 362;
__gen_e_acsl_assert_data_5.name = "initialization/success_or_error";
__e_acsl_assert(__gen_e_acsl_or_5,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
@@ -1378,7 +1399,7 @@ int __gen_e_acsl_pthread_cond_wait(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data.pred_txt = "\\valid(cond)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_cond_wait";
- __gen_e_acsl_assert_data.line = 203;
+ __gen_e_acsl_assert_data.line = 317;
__gen_e_acsl_assert_data.name = "valid_cond";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -1399,7 +1420,7 @@ int __gen_e_acsl_pthread_cond_wait(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data_2.pred_txt = "\\valid(mutex)";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_cond_wait";
- __gen_e_acsl_assert_data_2.line = 204;
+ __gen_e_acsl_assert_data_2.line = 318;
__gen_e_acsl_assert_data_2.name = "valid_mutex";
__e_acsl_assert(__gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -1415,7 +1436,7 @@ int __gen_e_acsl_pthread_cond_wait(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data_3.pred_txt = "\\result == 0";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_3.fct = "pthread_cond_wait";
- __gen_e_acsl_assert_data_3.line = 206;
+ __gen_e_acsl_assert_data_3.line = 320;
__gen_e_acsl_assert_data_3.name = "success";
__e_acsl_assert(__retres == 0,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
@@ -1461,7 +1482,7 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data.pred_txt = "\\valid(cond)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_cond_init";
- __gen_e_acsl_assert_data.line = 187;
+ __gen_e_acsl_assert_data.line = 294;
__gen_e_acsl_assert_data.name = "valid_cond";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -1491,7 +1512,7 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data_2.pred_txt = "attr == \\null || \\valid_read(attr)";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_cond_init";
- __gen_e_acsl_assert_data_2.line = 188;
+ __gen_e_acsl_assert_data_2.line = 295;
__gen_e_acsl_assert_data_2.name = "valid_null_attr";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -1516,7 +1537,7 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data_3.pred_txt = "\\initialized(\\old(cond))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_3.fct = "pthread_cond_init";
- __gen_e_acsl_assert_data_3.line = 191;
+ __gen_e_acsl_assert_data_3.line = 298;
__gen_e_acsl_assert_data_3.name = "initialization/cond";
__e_acsl_assert(__gen_e_acsl_initialized,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
@@ -1529,7 +1550,7 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data_4.pred_txt = "\\result == 0";
__gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_4.fct = "pthread_cond_init";
- __gen_e_acsl_assert_data_4.line = 192;
+ __gen_e_acsl_assert_data_4.line = 299;
__gen_e_acsl_assert_data_4.name = "success";
__e_acsl_assert(__retres == 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -1567,7 +1588,7 @@ int __gen_e_acsl_pthread_cond_broadcast(pthread_cond_t *cond)
__gen_e_acsl_assert_data.pred_txt = "\\valid(cond)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_cond_broadcast";
- __gen_e_acsl_assert_data.line = 173;
+ __gen_e_acsl_assert_data.line = 280;
__gen_e_acsl_assert_data.name = "valid_cond";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -1583,7 +1604,7 @@ int __gen_e_acsl_pthread_cond_broadcast(pthread_cond_t *cond)
__gen_e_acsl_assert_data_2.pred_txt = "\\result == 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_cond_broadcast";
- __gen_e_acsl_assert_data_2.line = 175;
+ __gen_e_acsl_assert_data_2.line = 282;
__gen_e_acsl_assert_data_2.name = "sucess";
__e_acsl_assert(__retres == 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -1826,7 +1847,7 @@ int main(void)
__e_acsl_delete_block((void *)(& i));
}
while (1) {
- int res = pthread_mutex_trylock(& write_mutex);
+ int res = __gen_e_acsl_pthread_mutex_trylock(& write_mutex);
__e_acsl_store_block((void *)(& res),4UL);
__e_acsl_full_init((void *)(& res));
if (res == 0) {
@@ -1847,7 +1868,7 @@ int main(void)
__e_acsl_delete_block((void *)(& res));
}
while (1) {
- int res_0 = pthread_mutex_trylock(& read_mutex);
+ int res_0 = __gen_e_acsl_pthread_mutex_trylock(& read_mutex);
__e_acsl_store_block((void *)(& res_0),4UL);
__e_acsl_full_init((void *)(& res_0));
if (res_0 == 0) {
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 36d1dce6d27..6cd1e48d014 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
@@ -231,7 +231,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
__gen_e_acsl_assert_data.pred_txt = "retval == \\null || \\valid(retval)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_join";
- __gen_e_acsl_assert_data.line = 247;
+ __gen_e_acsl_assert_data.line = 405;
__gen_e_acsl_assert_data.name = "valid_or_null_retval";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -274,7 +274,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
__gen_e_acsl_assert_data_2.pred_txt = "\\result == 0 || \\result == 35 || \\result == 22 || \\result == 3";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_join";
- __gen_e_acsl_assert_data_2.line = 251;
+ __gen_e_acsl_assert_data_2.line = 409;
__gen_e_acsl_assert_data_2.name = "success_or_error";
__e_acsl_assert(__gen_e_acsl_or_4,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -329,7 +329,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data.pred_txt = "\\valid(thread)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_create";
- __gen_e_acsl_assert_data.line = 223;
+ __gen_e_acsl_assert_data.line = 355;
__gen_e_acsl_assert_data.name = "valid_thread";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -359,7 +359,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_2.pred_txt = "attr == \\null || \\valid_read(attr)";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_create";
- __gen_e_acsl_assert_data_2.line = 224;
+ __gen_e_acsl_assert_data_2.line = 356;
__gen_e_acsl_assert_data_2.name = "valid_null_attr";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -384,7 +384,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_4.pred_txt = "arg == \\null || \\valid((char *)arg)";
__gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_4.fct = "pthread_create";
- __gen_e_acsl_assert_data_4.line = 226;
+ __gen_e_acsl_assert_data_4.line = 358;
__gen_e_acsl_assert_data_4.name = "valid_null_arg";
__e_acsl_assert(__gen_e_acsl_or_2,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -436,7 +436,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_5.pred_txt = "(\\result == 0 && \\initialized(\\old(thread))) || \\result == 11 ||\n\\result == 22 || \\result == 1";
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_5.fct = "pthread_create";
- __gen_e_acsl_assert_data_5.line = 230;
+ __gen_e_acsl_assert_data_5.line = 362;
__gen_e_acsl_assert_data_5.name = "initialization/success_or_error";
__e_acsl_assert(__gen_e_acsl_or_5,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
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 2a778a1f8cc..5b9c35ce05b 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
@@ -113,6 +113,12 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
*/
int __gen_e_acsl_pthread_mutex_lock(pthread_mutex_t *mutex);
+/*@ assigns \result, *mutex;
+ assigns \result \from *mutex;
+ assigns *mutex \from *mutex;
+ */
+int __gen_e_acsl_pthread_mutex_trylock(pthread_mutex_t *mutex);
+
/*@ requires mutex_valid: \valid(mutex);
ensures success_or_error: \result == 0 || \result == 1;
assigns *mutex, \result;
@@ -510,7 +516,7 @@ int __gen_e_acsl_pthread_mutex_unlock(pthread_mutex_t *mutex)
__gen_e_acsl_assert_data.pred_txt = "\\valid(mutex)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_mutex_unlock";
- __gen_e_acsl_assert_data.line = 313;
+ __gen_e_acsl_assert_data.line = 499;
__gen_e_acsl_assert_data.name = "mutex_valid";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -533,7 +539,7 @@ int __gen_e_acsl_pthread_mutex_unlock(pthread_mutex_t *mutex)
__gen_e_acsl_assert_data_2.pred_txt = "\\result == 0 || \\result == 1";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_mutex_unlock";
- __gen_e_acsl_assert_data_2.line = 316;
+ __gen_e_acsl_assert_data_2.line = 502;
__gen_e_acsl_assert_data_2.name = "success_or_error";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -543,6 +549,21 @@ int __gen_e_acsl_pthread_mutex_unlock(pthread_mutex_t *mutex)
}
}
+/*@ assigns \result, *mutex;
+ assigns \result \from *mutex;
+ assigns *mutex \from *mutex;
+ */
+int __gen_e_acsl_pthread_mutex_trylock(pthread_mutex_t *mutex)
+{
+ int __retres;
+ __e_acsl_store_block((void *)(& __retres),4UL);
+ __e_acsl_store_block((void *)(& mutex),8UL);
+ __retres = pthread_mutex_trylock(mutex);
+ __e_acsl_delete_block((void *)(& mutex));
+ __e_acsl_delete_block((void *)(& __retres));
+ return __retres;
+}
+
/*@ requires mutex_valid: \valid(mutex);
ensures
success_or_error:
@@ -574,7 +595,7 @@ int __gen_e_acsl_pthread_mutex_lock(pthread_mutex_t *mutex)
__gen_e_acsl_assert_data.pred_txt = "\\valid(mutex)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_mutex_lock";
- __gen_e_acsl_assert_data.line = 295;
+ __gen_e_acsl_assert_data.line = 467;
__gen_e_acsl_assert_data.name = "mutex_valid";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -611,7 +632,7 @@ int __gen_e_acsl_pthread_mutex_lock(pthread_mutex_t *mutex)
__gen_e_acsl_assert_data_2.pred_txt = "\\result == 0 || \\result == 11 || \\result == 22 || \\result == 35";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_mutex_lock";
- __gen_e_acsl_assert_data_2.line = 299;
+ __gen_e_acsl_assert_data_2.line = 471;
__gen_e_acsl_assert_data_2.name = "success_or_error";
__e_acsl_assert(__gen_e_acsl_or_3,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -659,7 +680,7 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
__gen_e_acsl_assert_data.pred_txt = "\\valid(mutex)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_mutex_init";
- __gen_e_acsl_assert_data.line = 279;
+ __gen_e_acsl_assert_data.line = 451;
__gen_e_acsl_assert_data.name = "mutex_valid";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -689,7 +710,7 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
__gen_e_acsl_assert_data_2.pred_txt = "attrs == \\null || \\valid_read(attrs)";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_mutex_init";
- __gen_e_acsl_assert_data_2.line = 280;
+ __gen_e_acsl_assert_data_2.line = 452;
__gen_e_acsl_assert_data_2.name = "attrs_valid_or_null";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -749,7 +770,7 @@ int __gen_e_acsl_pthread_mutex_init(pthread_mutex_t * restrict mutex,
__gen_e_acsl_assert_data_3.pred_txt = "(\\result == 0 && \\initialized(\\old(mutex))) || \\result == 11 || \\result == 12 ||\n\\result == 1 || \\result == 22";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_3.fct = "pthread_mutex_init";
- __gen_e_acsl_assert_data_3.line = 285;
+ __gen_e_acsl_assert_data_3.line = 457;
__gen_e_acsl_assert_data_3.name = "initialization/success_or_error";
__e_acsl_assert(__gen_e_acsl_or_5,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
@@ -811,7 +832,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
__gen_e_acsl_assert_data.pred_txt = "retval == \\null || \\valid(retval)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_join";
- __gen_e_acsl_assert_data.line = 247;
+ __gen_e_acsl_assert_data.line = 405;
__gen_e_acsl_assert_data.name = "valid_or_null_retval";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -854,7 +875,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
__gen_e_acsl_assert_data_2.pred_txt = "\\result == 0 || \\result == 35 || \\result == 22 || \\result == 3";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_join";
- __gen_e_acsl_assert_data_2.line = 251;
+ __gen_e_acsl_assert_data_2.line = 409;
__gen_e_acsl_assert_data_2.name = "success_or_error";
__e_acsl_assert(__gen_e_acsl_or_4,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -909,7 +930,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data.pred_txt = "\\valid(thread)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_create";
- __gen_e_acsl_assert_data.line = 223;
+ __gen_e_acsl_assert_data.line = 355;
__gen_e_acsl_assert_data.name = "valid_thread";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -939,7 +960,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_2.pred_txt = "attr == \\null || \\valid_read(attr)";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_create";
- __gen_e_acsl_assert_data_2.line = 224;
+ __gen_e_acsl_assert_data_2.line = 356;
__gen_e_acsl_assert_data_2.name = "valid_null_attr";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -964,7 +985,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_4.pred_txt = "arg == \\null || \\valid((char *)arg)";
__gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_4.fct = "pthread_create";
- __gen_e_acsl_assert_data_4.line = 226;
+ __gen_e_acsl_assert_data_4.line = 358;
__gen_e_acsl_assert_data_4.name = "valid_null_arg";
__e_acsl_assert(__gen_e_acsl_or_2,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -1016,7 +1037,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_5.pred_txt = "(\\result == 0 && \\initialized(\\old(thread))) || \\result == 11 ||\n\\result == 22 || \\result == 1";
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_5.fct = "pthread_create";
- __gen_e_acsl_assert_data_5.line = 230;
+ __gen_e_acsl_assert_data_5.line = 362;
__gen_e_acsl_assert_data_5.name = "initialization/success_or_error";
__e_acsl_assert(__gen_e_acsl_or_5,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
@@ -1060,7 +1081,7 @@ int __gen_e_acsl_pthread_cond_wait(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data.pred_txt = "\\valid(cond)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_cond_wait";
- __gen_e_acsl_assert_data.line = 203;
+ __gen_e_acsl_assert_data.line = 317;
__gen_e_acsl_assert_data.name = "valid_cond";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -1081,7 +1102,7 @@ int __gen_e_acsl_pthread_cond_wait(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data_2.pred_txt = "\\valid(mutex)";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_cond_wait";
- __gen_e_acsl_assert_data_2.line = 204;
+ __gen_e_acsl_assert_data_2.line = 318;
__gen_e_acsl_assert_data_2.name = "valid_mutex";
__e_acsl_assert(__gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -1097,7 +1118,7 @@ int __gen_e_acsl_pthread_cond_wait(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data_3.pred_txt = "\\result == 0";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_3.fct = "pthread_cond_wait";
- __gen_e_acsl_assert_data_3.line = 206;
+ __gen_e_acsl_assert_data_3.line = 320;
__gen_e_acsl_assert_data_3.name = "success";
__e_acsl_assert(__retres == 0,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
@@ -1143,7 +1164,7 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data.pred_txt = "\\valid(cond)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_cond_init";
- __gen_e_acsl_assert_data.line = 187;
+ __gen_e_acsl_assert_data.line = 294;
__gen_e_acsl_assert_data.name = "valid_cond";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -1173,7 +1194,7 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data_2.pred_txt = "attr == \\null || \\valid_read(attr)";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_cond_init";
- __gen_e_acsl_assert_data_2.line = 188;
+ __gen_e_acsl_assert_data_2.line = 295;
__gen_e_acsl_assert_data_2.name = "valid_null_attr";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -1198,7 +1219,7 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data_3.pred_txt = "\\initialized(\\old(cond))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_3.fct = "pthread_cond_init";
- __gen_e_acsl_assert_data_3.line = 191;
+ __gen_e_acsl_assert_data_3.line = 298;
__gen_e_acsl_assert_data_3.name = "initialization/cond";
__e_acsl_assert(__gen_e_acsl_initialized,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
@@ -1211,7 +1232,7 @@ int __gen_e_acsl_pthread_cond_init(pthread_cond_t * restrict cond,
__gen_e_acsl_assert_data_4.pred_txt = "\\result == 0";
__gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_4.fct = "pthread_cond_init";
- __gen_e_acsl_assert_data_4.line = 192;
+ __gen_e_acsl_assert_data_4.line = 299;
__gen_e_acsl_assert_data_4.name = "success";
__e_acsl_assert(__retres == 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -1249,7 +1270,7 @@ int __gen_e_acsl_pthread_cond_broadcast(pthread_cond_t *cond)
__gen_e_acsl_assert_data.pred_txt = "\\valid(cond)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_cond_broadcast";
- __gen_e_acsl_assert_data.line = 173;
+ __gen_e_acsl_assert_data.line = 280;
__gen_e_acsl_assert_data.name = "valid_cond";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -1265,7 +1286,7 @@ int __gen_e_acsl_pthread_cond_broadcast(pthread_cond_t *cond)
__gen_e_acsl_assert_data_2.pred_txt = "\\result == 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_cond_broadcast";
- __gen_e_acsl_assert_data_2.line = 175;
+ __gen_e_acsl_assert_data_2.line = 282;
__gen_e_acsl_assert_data_2.name = "sucess";
__e_acsl_assert(__retres == 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -1508,7 +1529,7 @@ int main(void)
__e_acsl_delete_block((void *)(& i));
}
while (1) {
- int res = pthread_mutex_trylock(& write_mutex);
+ int res = __gen_e_acsl_pthread_mutex_trylock(& write_mutex);
__e_acsl_store_block((void *)(& res),4UL);
__e_acsl_full_init((void *)(& res));
if (res == 0) {
@@ -1529,7 +1550,7 @@ int main(void)
__e_acsl_delete_block((void *)(& res));
}
while (1) {
- int res_0 = pthread_mutex_trylock(& read_mutex);
+ int res_0 = __gen_e_acsl_pthread_mutex_trylock(& read_mutex);
__e_acsl_store_block((void *)(& res_0),4UL);
__e_acsl_full_init((void *)(& res_0));
if (res_0 == 0) {
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 2b24521f078..945951d9514 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
@@ -203,7 +203,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
__gen_e_acsl_assert_data.pred_txt = "retval == \\null || \\valid(retval)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_join";
- __gen_e_acsl_assert_data.line = 247;
+ __gen_e_acsl_assert_data.line = 405;
__gen_e_acsl_assert_data.name = "valid_or_null_retval";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -246,7 +246,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
__gen_e_acsl_assert_data_2.pred_txt = "\\result == 0 || \\result == 35 || \\result == 22 || \\result == 3";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_join";
- __gen_e_acsl_assert_data_2.line = 251;
+ __gen_e_acsl_assert_data_2.line = 409;
__gen_e_acsl_assert_data_2.name = "success_or_error";
__e_acsl_assert(__gen_e_acsl_or_4,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -301,7 +301,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data.pred_txt = "\\valid(thread)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data.fct = "pthread_create";
- __gen_e_acsl_assert_data.line = 223;
+ __gen_e_acsl_assert_data.line = 355;
__gen_e_acsl_assert_data.name = "valid_thread";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -331,7 +331,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_2.pred_txt = "attr == \\null || \\valid_read(attr)";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_2.fct = "pthread_create";
- __gen_e_acsl_assert_data_2.line = 224;
+ __gen_e_acsl_assert_data_2.line = 356;
__gen_e_acsl_assert_data_2.name = "valid_null_attr";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -356,7 +356,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_4.pred_txt = "arg == \\null || \\valid((char *)arg)";
__gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_4.fct = "pthread_create";
- __gen_e_acsl_assert_data_4.line = 226;
+ __gen_e_acsl_assert_data_4.line = 358;
__gen_e_acsl_assert_data_4.name = "valid_null_arg";
__e_acsl_assert(__gen_e_acsl_or_2,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -408,7 +408,7 @@ int __gen_e_acsl_pthread_create(pthread_t * restrict thread,
__gen_e_acsl_assert_data_5.pred_txt = "(\\result == 0 && \\initialized(\\old(thread))) || \\result == 11 ||\n\\result == 22 || \\result == 1";
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/pthread.h";
__gen_e_acsl_assert_data_5.fct = "pthread_create";
- __gen_e_acsl_assert_data_5.line = 230;
+ __gen_e_acsl_assert_data_5.line = 362;
__gen_e_acsl_assert_data_5.name = "initialization/success_or_error";
__e_acsl_assert(__gen_e_acsl_or_5,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
index 97e24b1e6ab..24ff5e96514 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
@@ -23,6 +23,9 @@
[e-acsl] Warning: annotating undefined function `pthread_mutex_lock':
the generated program may miss memory instrumentation
if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `pthread_mutex_trylock':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] Warning: annotating undefined function `pthread_mutex_unlock':
the generated program may miss memory instrumentation
if there are memory-related annotations.
@@ -57,131 +60,131 @@
[e-acsl] FRAMAC_SHARE/libc/stdio.h:485: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:312: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:498: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:493: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:294: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:466: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:278: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:450: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:247: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:405: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:252: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:410: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:255: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:413: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:225: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:357: Warning:
E-ACSL construct `\valid_function' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:355: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:203: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:317: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:186: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:293: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:173: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:280: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:279: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:451: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:279: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:451: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:285: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:457: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:285: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:457: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:285: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:457: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:286: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:458: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:287: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:459: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:288: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:460: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:289: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:461: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:285: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:457: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:187: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:294: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:187: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:294: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:191: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:298: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:191: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:298: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:355: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:355: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:358: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:358: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:358: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __gen_e_acsl_pthread_create: postcondition 'initialization,success_or_error' got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:355: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:358: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[kernel:annot:missing-spec] parallel_threads.c:121: Warning:
- Neither code nor specification for function pthread_mutex_trylock,
- generating default assigns. See -generated-spec-* options for more info
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:313: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:499: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:313: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:499: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:316: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:502: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/unistd.h:1153: Warning:
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/sequential_threads.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/sequential_threads.res.oracle
index c9e7bf5db13..496843958f3 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/sequential_threads.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/sequential_threads.res.oracle
@@ -8,57 +8,57 @@
[e-acsl] Warning: annotating undefined function `pthread_join':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:247: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:405: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:252: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:410: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:255: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:413: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:225: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:357: Warning:
E-ACSL construct `\valid_function' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:355: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:355: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:355: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:358: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:358: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:358: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __gen_e_acsl_pthread_create: postcondition 'initialization,success_or_error' got status unknown.
[eva:alarm] sequential_threads.c:29: Warning:
accessing uninitialized left-value. assert \initialized(&t);
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
index 97e24b1e6ab..24ff5e96514 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
@@ -23,6 +23,9 @@
[e-acsl] Warning: annotating undefined function `pthread_mutex_lock':
the generated program may miss memory instrumentation
if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `pthread_mutex_trylock':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] Warning: annotating undefined function `pthread_mutex_unlock':
the generated program may miss memory instrumentation
if there are memory-related annotations.
@@ -57,131 +60,131 @@
[e-acsl] FRAMAC_SHARE/libc/stdio.h:485: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:312: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:498: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:493: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:294: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:466: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:278: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:450: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:247: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:405: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:252: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:410: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:255: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:413: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:225: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:357: Warning:
E-ACSL construct `\valid_function' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:355: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:203: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:317: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:186: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:293: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:173: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:280: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:279: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:451: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:279: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:451: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:285: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:457: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:285: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:457: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:285: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:457: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:286: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:458: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:287: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:459: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:288: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:460: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:289: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:461: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:285: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:457: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:187: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:294: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:187: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:294: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:191: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:298: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:191: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:298: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:355: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:355: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:358: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:358: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:358: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __gen_e_acsl_pthread_create: postcondition 'initialization,success_or_error' got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:355: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:358: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[kernel:annot:missing-spec] parallel_threads.c:121: Warning:
- Neither code nor specification for function pthread_mutex_trylock,
- generating default assigns. See -generated-spec-* options for more info
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:313: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:499: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:313: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:499: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:316: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:502: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/unistd.h:1153: Warning:
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/threads_safe_locations.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/threads_safe_locations.res.oracle
index 3130ac26669..03caab59913 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/threads_safe_locations.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/threads_safe_locations.res.oracle
@@ -8,48 +8,48 @@
[e-acsl] Warning: annotating undefined function `pthread_join':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:247: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:405: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:252: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:410: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:255: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:413: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:225: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:357: Warning:
E-ACSL construct `\valid_function' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[e-acsl] FRAMAC_SHARE/libc/pthread.h:355: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:355: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:223: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:355: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:231: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:363: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/pthread.h:230: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/pthread.h:362: Warning:
function __gen_e_acsl_pthread_create: postcondition 'initialization,success_or_error' got status unknown.
[eva:alarm] threads_safe_locations.c:17: Warning:
accessing uninitialized left-value. assert \initialized(&t);
diff --git a/tests/builtins/oracle/memcpy.0.res.oracle b/tests/builtins/oracle/memcpy.0.res.oracle
index f3394b79601..4f0cb38f1d5 100644
--- a/tests/builtins/oracle/memcpy.0.res.oracle
+++ b/tests/builtins/oracle/memcpy.0.res.oracle
@@ -1760,6 +1760,28 @@
[ Valid ] Default behavior
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function 'bcmp'
+--------------------------------------------------------------------------------
+
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 33)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'bcopy'
+--------------------------------------------------------------------------------
+
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/strings.h, line 39)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 39)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'bzero'
--------------------------------------------------------------------------------
@@ -1768,9 +1790,42 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'zero_initialized'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/strings.h, line 37)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/strings.h, line 45)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 45)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'ffs'
+--------------------------------------------------------------------------------
+
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 51)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'index'
+--------------------------------------------------------------------------------
+
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 56)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'rindex'
+--------------------------------------------------------------------------------
+
+[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 37)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 61)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1781,7 +1836,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 48)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 68)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1792,7 +1847,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 55)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 75)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -2215,9 +2270,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 169 Completely validated
+ 174 Completely validated
1 Locally validated
- 267 Considered valid
+ 277 Considered valid
36 To be validated
- 473 Total
+ 488 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/argz_c.res.oracle b/tests/libc/oracle/argz_c.res.oracle
index 21fe8e24b8a..9b0b7650e7e 100644
--- a/tests/libc/oracle/argz_c.res.oracle
+++ b/tests/libc/oracle/argz_c.res.oracle
@@ -49,6 +49,8 @@
\return(strndup) == 0 (auto)
\return(stpncpy) == 0 (auto)
\return(strsignal) == 0 (auto)
+ \return(index) == 0 (auto)
+ \return(rindex) == 0 (auto)
\return(argz_count) == 0, 6 (auto)
\return(argz_append) == 0, 6 (auto)
\return(argz_add) == 0, 6 (auto)
diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle
index 1b980123959..ad475976a58 100644
--- a/tests/libc/oracle/coverage.res.oracle
+++ b/tests/libc/oracle/coverage.res.oracle
@@ -28,7 +28,7 @@
main: 4 stmts out of 4 (100.0%)
[metrics] Eva coverage statistics
=======================
- Syntactically reachable functions = 2 (out of 103)
+ Syntactically reachable functions = 2 (out of 108)
Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 4c4b48b4a96..bec42d8aa6b 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -5,10 +5,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] fc_libc.c:209: assertion got status valid.
[eva] fc_libc.c:210: assertion got status valid.
[eva] fc_libc.c:211: assertion got status valid.
[eva] fc_libc.c:212: assertion got status valid.
+[eva] fc_libc.c:213: assertion got status valid.
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
@@ -21,6 +21,7 @@
#include "__fc_gcc_builtins.h"
#include "__fc_integer.h"
#include "__fc_select.h"
+#include "__fc_utmp_constants.h"
#include "alloca.h"
#include "argz.c"
#include "argz.h"
@@ -41,6 +42,7 @@
#include "glob.c"
#include "glob.h"
#include "iconv.h"
+#include "ifaddrs.h"
#include "inttypes.c"
#include "inttypes.h"
#include "libgen.h"
@@ -55,9 +57,12 @@
#include "pthread.h"
#include "pwd.c"
#include "pwd.h"
+#include "sched.h"
+#include "semaphore.h"
#include "setjmp.h"
#include "signal.c"
#include "signal.h"
+#include "spawn.h"
#include "stdarg.h"
#include "stdatomic.c"
#include "stdatomic.h"
@@ -90,6 +95,8 @@
#include "uchar.h"
#include "unistd.c"
#include "unistd.h"
+#include "utmp.h"
+#include "utmpx.h"
#include "wchar.c"
#include "wchar.h"
void main(void)
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 09cc0099892..35a6f3be165 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -47,6 +47,7 @@
[kernel] Parsing FRAMAC_SHARE/libc/__fc_libc.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_select.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_string_axiomatic.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/libc/__fc_utmp_constants.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/aio.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/alloca.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/argz.h (with preprocessing)
diff --git a/tests/libc/oracle/fc_libc.4.res.oracle b/tests/libc/oracle/fc_libc.4.res.oracle
index 862bb1b108e..652d59eb985 100644
--- a/tests/libc/oracle/fc_libc.4.res.oracle
+++ b/tests/libc/oracle/fc_libc.4.res.oracle
@@ -4,5 +4,5 @@
[kernel] Parsing glibc_functions.json
[kernel] Parsing posix_identifiers.json
[kernel] Parsing nonstandard_identifiers.json
-[kernel] Warning: <uchar.h>:c8rtomb : unknown identifier
[kernel] Warning: <uchar.h>:mbrtoc8 : unknown identifier
+[kernel] Warning: <uchar.h>:c8rtomb : unknown identifier
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 1893865c64c..20d9dac5c58 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -46,6 +46,8 @@
\return(strndup) == 0 (auto)
\return(stpncpy) == 0 (auto)
\return(strsignal) == 0 (auto)
+ \return(index) == 0 (auto)
+ \return(rindex) == 0 (auto)
\return(bind) == 0 (auto)
\return(socket) == -1 (auto)
\return(signal) == 0 (auto)
@@ -57,7 +59,18 @@
\return(Frama_C_malloc_fresh) == 0 (auto)
\return(gai_strerror) == 0 (auto)
\return(getaddrinfo) == 0 (auto)
+ \return(gethostbyaddr) == 0 (auto)
\return(gethostbyname) == 0 (auto)
+ \return(gethostent) == 0 (auto)
+ \return(getnetbyaddr) == 0 (auto)
+ \return(getnetbyname) == 0 (auto)
+ \return(getnetent) == 0 (auto)
+ \return(getprotobyname) == 0 (auto)
+ \return(getprotobynumber) == 0 (auto)
+ \return(getprotoent) == 0 (auto)
+ \return(getservbyname) == 0 (auto)
+ \return(getservbyport) == 0 (auto)
+ \return(getservent) == 0 (auto)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index fe4f9414bf7..1219ddf39fa 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -129,7 +129,7 @@
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] signal_h.c:48:
function sigaction: precondition 'separation,separated_acts' got status valid.
-[eva] FRAMAC_SHARE/libc/signal.h:229:
+[eva] FRAMAC_SHARE/libc/signal.h:234:
cannot evaluate ACSL term, unsupported ACSL construct: logic coercion struct sigaction -> set<struct sigaction>
[eva:garbled-mix:assigns] signal_h.c:48:
The specification of function sigaction
diff --git a/tests/libc/oracle/spawn_h.res.oracle b/tests/libc/oracle/spawn_h.res.oracle
index c5b9d81f0e7..04ce3cdeaf2 100644
--- a/tests/libc/oracle/spawn_h.res.oracle
+++ b/tests/libc/oracle/spawn_h.res.oracle
@@ -11,30 +11,18 @@
The specification of function getopt has generated a garbled mix of addresses
for assigns clause \result.
[eva] Done for function getopt
-[kernel:annot:missing-spec] spawn_h.c:43: Warning:
- Neither code nor specification for function posix_spawn_file_actions_init,
- generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawn_file_actions_init <- main.
Called from spawn_h.c:43.
[eva] using specification for function posix_spawn_file_actions_init
[eva] Done for function posix_spawn_file_actions_init
-[kernel:annot:missing-spec] spawn_h.c:47: Warning:
- Neither code nor specification for function posix_spawn_file_actions_addclose,
- generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawn_file_actions_addclose <- main.
Called from spawn_h.c:47.
[eva] using specification for function posix_spawn_file_actions_addclose
[eva] Done for function posix_spawn_file_actions_addclose
-[kernel:annot:missing-spec] spawn_h.c:60: Warning:
- Neither code nor specification for function posix_spawnattr_init,
- generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawnattr_init <- main.
Called from spawn_h.c:60.
[eva] using specification for function posix_spawnattr_init
[eva] Done for function posix_spawnattr_init
-[kernel:annot:missing-spec] spawn_h.c:63: Warning:
- Neither code nor specification for function posix_spawnattr_setflags,
- generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawnattr_setflags <- main.
Called from spawn_h.c:63.
[eva] using specification for function posix_spawnattr_setflags
@@ -45,9 +33,6 @@
[eva] spawn_h.c:67:
function sigfillset: precondition 'valid_set' got status valid.
[eva] Done for function sigfillset
-[kernel:annot:missing-spec] spawn_h.c:68: Warning:
- Neither code nor specification for function posix_spawnattr_setsigmask,
- generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawnattr_setsigmask <- main.
Called from spawn_h.c:68.
[eva] using specification for function posix_spawnattr_setsigmask
@@ -104,9 +89,6 @@
out of bounds read. assert \valid_read(argv + optind);
[eva:garbled-mix:write] spawn_h.c:82:
Assigning imprecise value to file because of misaligned read of addresses.
-[kernel:annot:missing-spec] spawn_h.c:82: Warning:
- Neither code nor specification for function posix_spawnp,
- generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawnp <- main.
Called from spawn_h.c:82.
[eva] using specification for function posix_spawnp
@@ -116,9 +98,6 @@
[eva] spawn_h.c:85:
function perror: precondition 'valid_string_s' got status valid.
[eva] Done for function perror
-[kernel:annot:missing-spec] spawn_h.c:90: Warning:
- Neither code nor specification for function posix_spawnattr_destroy,
- generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawnattr_destroy <- main.
Called from spawn_h.c:90.
[eva] using specification for function posix_spawnattr_destroy
@@ -128,9 +107,6 @@
[eva] spawn_h.c:92:
function perror: precondition 'valid_string_s' got status valid.
[eva] Done for function perror
-[kernel:annot:missing-spec] spawn_h.c:96: Warning:
- Neither code nor specification for function posix_spawn_file_actions_destroy,
- generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawn_file_actions_destroy <- main.
Called from spawn_h.c:96.
[eva] using specification for function posix_spawn_file_actions_destroy
--
GitLab