From abd27d22fb2accd9fdc8a02f542469577ee9ad23 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 18 Apr 2024 10:28:15 +0200
Subject: [PATCH] revert "[Libc] add __FC_PTHREAD_T_IS_SCALAR ..." and change
pthread_t type
This reverts commit 1e6f913593d3a32584f721e1a0441cf96b845eb7.
It also changes pthread_t to match the usual definition on a glibc + Linux.
---
share/libc/__fc_define_pthread_types.h | 9 +-
tests/libc/oracle/pthread_h.1.res.oracle | 94 -------------------
tests/libc/oracle/pthread_h.2.res.oracle | 10 --
...ad_h.0.res.oracle => pthread_h.res.oracle} | 52 +++++-----
tests/libc/pthread_h.c | 14 ---
5 files changed, 27 insertions(+), 152 deletions(-)
delete mode 100644 tests/libc/oracle/pthread_h.1.res.oracle
delete mode 100644 tests/libc/oracle/pthread_h.2.res.oracle
rename tests/libc/oracle/{pthread_h.0.res.oracle => pthread_h.res.oracle} (79%)
diff --git a/share/libc/__fc_define_pthread_types.h b/share/libc/__fc_define_pthread_types.h
index 66091ac3279..822b9af46e7 100644
--- a/share/libc/__fc_define_pthread_types.h
+++ b/share/libc/__fc_define_pthread_types.h
@@ -44,14 +44,7 @@ typedef struct __fc_pthread_once_t { int _fc; } pthread_once_t;
typedef struct __fc_pthread_rwlock_t { int _fc; } pthread_rwlock_t;
typedef struct __fc_pthread_rwlockattr_t { int _fc; } pthread_rwlockattr_t;
typedef struct __fc_pthread_spinlock_t { int _fc; } pthread_spinlock_t;
-
-#ifdef __FC_PTHREAD_T_IS_SCALAR
-// Some non-portable code assumes pthread_t as a scalar; this allows
-// such code to be parsed.
-typedef unsigned long pthread_t;
-#else
-typedef struct __fc_pthread_t { unsigned long _fc; } pthread_t;
-#endif
+typedef struct unsigned long pthread_t;
__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/tests/libc/oracle/pthread_h.1.res.oracle b/tests/libc/oracle/pthread_h.1.res.oracle
deleted file mode 100644
index e9962e514fb..00000000000
--- a/tests/libc/oracle/pthread_h.1.res.oracle
+++ /dev/null
@@ -1,94 +0,0 @@
-[kernel] Parsing pthread_h.c (with preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- retval ∈ {0}
- v ∈ [--..--]
-[eva] computing for function pthread_create <- main.
- Called from pthread_h.c:23.
-[eva] using specification for function pthread_create
-[eva] pthread_h.c:23:
- function pthread_create: precondition 'valid_thread' got status valid.
-[eva] pthread_h.c:23:
- function pthread_create: precondition 'valid_null_attr' got status valid.
-[eva] pthread_h.c:23:
- function pthread_create: precondition 'valid_routine' got status valid.
-[eva] pthread_h.c:23:
- function pthread_create: precondition 'valid_null_arg' got status valid.
-[eva] Done for function pthread_create
-[eva] computing for function printf_va_2 <- main.
- Called from pthread_h.c:25.
-[eva] using specification for function printf_va_2
-[eva] pthread_h.c:25: function printf_va_2: precondition got status valid.
-[eva] Done for function printf_va_2
-[eva] computing for function printf_va_3 <- main.
- Called from pthread_h.c:28.
-[eva] using specification for function printf_va_3
-[eva] pthread_h.c:28: function printf_va_3: precondition got status valid.
-[eva] Done for function printf_va_3
-[eva:alarm] pthread_h.c:29: Warning:
- accessing uninitialized left-value. assert \initialized(&thread);
-[eva] computing for function pthread_setname_np <- main.
- Called from pthread_h.c:29.
-[eva] using specification for function pthread_setname_np
-[eva] pthread_h.c:29:
- function pthread_setname_np: precondition 'valid_name' got status valid.
-[eva] Done for function pthread_setname_np
-[eva] computing for function pthread_getname_np <- main.
- Called from pthread_h.c:32.
-[eva] using specification for function pthread_getname_np
-[eva] pthread_h.c:32:
- function pthread_getname_np: precondition 'valid_name' got status valid.
-[eva] Done for function pthread_getname_np
-[eva] computing for function printf_va_4 <- main.
- Called from pthread_h.c:33.
-[eva] using specification for function printf_va_4
-[eva:alarm] pthread_h.c:33: Warning:
- function printf_va_4: precondition valid_read_string(param0) got status unknown.
-[eva] pthread_h.c:33:
- function printf_va_4: precondition valid_read_string(format) got status valid.
-[eva] Done for function printf_va_4
-[eva] computing for function start_routine <- main.
- Called from pthread_h.c:38.
-[eva] computing for function printf_va_1 <- start_routine <- main.
- Called from pthread_h.c:14.
-[eva] using specification for function printf_va_1
-[eva] pthread_h.c:14: function printf_va_1: precondition got status valid.
-[eva] Done for function printf_va_1
-[eva] Recording results for start_routine
-[eva] Done for function start_routine
-[eva] computing for function pthread_join <- main.
- Called from pthread_h.c:40.
-[eva] using specification for function pthread_join
-[eva] pthread_h.c:40:
- function pthread_join: precondition 'valid_or_null_retval' got status valid.
-[eva] Done for function pthread_join
-[eva] computing for function printf_va_5 <- main.
- Called from pthread_h.c:42.
-[eva] using specification for function printf_va_5
-[eva] pthread_h.c:42: function printf_va_5: precondition got status valid.
-[eva] Done for function printf_va_5
-[eva:alarm] pthread_h.c:45: Warning:
- out of bounds read. assert \valid_read(retv);
-[eva] computing for function printf_va_6 <- main.
- Called from pthread_h.c:45.
-[eva] using specification for function printf_va_6
-[eva] pthread_h.c:45: function printf_va_6: precondition got status valid.
-[eva] Done for function printf_va_6
-[eva] Recording results for main
-[eva] Done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function start_routine:
- retval ∈ {43}
- __retres ∈ {{ (void *)&retval }}
- S___fc_stdout[0..1] ∈ [--..--]
-[eva:final-states] Values at end of function main:
- retval ∈ {0; 43}
- thread ∈ [--..--] or UNINITIALIZED
- thread_arg ∈ {42}
- r ∈ [--..--]
- buf[0..15] ∈ [--..--] or UNINITIALIZED
- retv ∈ {{ NULL + [--..--] ; &retval }} or UNINITIALIZED
- __retres ∈ {0; 1; 2}
- S___fc_stdout[0..1] ∈ [--..--]
diff --git a/tests/libc/oracle/pthread_h.2.res.oracle b/tests/libc/oracle/pthread_h.2.res.oracle
deleted file mode 100644
index e4df7ae1f77..00000000000
--- a/tests/libc/oracle/pthread_h.2.res.oracle
+++ /dev/null
@@ -1,10 +0,0 @@
-[kernel] Parsing pthread_h.c (with preprocessing)
-[kernel] pthread_h.c:49: User Error:
- cannot perform the following comparison thread == 0
- 47 // Test non-portable usage of pthread_t
- 48 #ifdef NON_PORTABLE
- 49 if (thread == 0) {
- ^^^^^^^^^^^
- 50 return 2;
- 51 }
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/libc/oracle/pthread_h.0.res.oracle b/tests/libc/oracle/pthread_h.res.oracle
similarity index 79%
rename from tests/libc/oracle/pthread_h.0.res.oracle
rename to tests/libc/oracle/pthread_h.res.oracle
index 41d84474ca4..6511a6631d2 100644
--- a/tests/libc/oracle/pthread_h.0.res.oracle
+++ b/tests/libc/oracle/pthread_h.res.oracle
@@ -6,73 +6,73 @@
retval ∈ {0}
v ∈ [--..--]
[eva] computing for function pthread_create <- main.
- Called from pthread_h.c:23.
+ Called from pthread_h.c:17.
[eva] using specification for function pthread_create
-[eva] pthread_h.c:23:
+[eva] pthread_h.c:17:
function pthread_create: precondition 'valid_thread' got status valid.
-[eva] pthread_h.c:23:
+[eva] pthread_h.c:17:
function pthread_create: precondition 'valid_null_attr' got status valid.
-[eva] pthread_h.c:23:
+[eva] pthread_h.c:17:
function pthread_create: precondition 'valid_routine' got status valid.
-[eva] pthread_h.c:23:
+[eva] pthread_h.c:17:
function pthread_create: precondition 'valid_null_arg' got status valid.
[eva] Done for function pthread_create
[eva] computing for function printf_va_2 <- main.
- Called from pthread_h.c:25.
+ Called from pthread_h.c:19.
[eva] using specification for function printf_va_2
-[eva] pthread_h.c:25: function printf_va_2: precondition got status valid.
+[eva] pthread_h.c:19: function printf_va_2: precondition got status valid.
[eva] Done for function printf_va_2
[eva] computing for function printf_va_3 <- main.
- Called from pthread_h.c:28.
+ Called from pthread_h.c:22.
[eva] using specification for function printf_va_3
-[eva] pthread_h.c:28: function printf_va_3: precondition got status valid.
+[eva] pthread_h.c:22: function printf_va_3: precondition got status valid.
[eva] Done for function printf_va_3
[eva] computing for function pthread_setname_np <- main.
- Called from pthread_h.c:29.
+ Called from pthread_h.c:23.
[eva] using specification for function pthread_setname_np
-[eva] pthread_h.c:29:
+[eva] pthread_h.c:23:
function pthread_setname_np: precondition 'valid_name' got status valid.
[eva] Done for function pthread_setname_np
[eva] computing for function pthread_getname_np <- main.
- Called from pthread_h.c:32.
+ Called from pthread_h.c:26.
[eva] using specification for function pthread_getname_np
-[eva] pthread_h.c:32:
+[eva] pthread_h.c:26:
function pthread_getname_np: precondition 'valid_name' got status valid.
[eva] Done for function pthread_getname_np
[eva] computing for function printf_va_4 <- main.
- Called from pthread_h.c:33.
+ Called from pthread_h.c:27.
[eva] using specification for function printf_va_4
-[eva:alarm] pthread_h.c:33: Warning:
+[eva:alarm] pthread_h.c:27: Warning:
function printf_va_4: precondition valid_read_string(param0) got status unknown.
-[eva] pthread_h.c:33:
+[eva] pthread_h.c:27:
function printf_va_4: precondition valid_read_string(format) got status valid.
[eva] Done for function printf_va_4
[eva] computing for function start_routine <- main.
- Called from pthread_h.c:38.
+ Called from pthread_h.c:32.
[eva] computing for function printf_va_1 <- start_routine <- main.
- Called from pthread_h.c:14.
+ Called from pthread_h.c:8.
[eva] using specification for function printf_va_1
-[eva] pthread_h.c:14: function printf_va_1: precondition got status valid.
+[eva] pthread_h.c:8: function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] Recording results for start_routine
[eva] Done for function start_routine
[eva] computing for function pthread_join <- main.
- Called from pthread_h.c:40.
+ Called from pthread_h.c:34.
[eva] using specification for function pthread_join
-[eva] pthread_h.c:40:
+[eva] pthread_h.c:34:
function pthread_join: precondition 'valid_or_null_retval' got status valid.
[eva] Done for function pthread_join
[eva] computing for function printf_va_5 <- main.
- Called from pthread_h.c:42.
+ Called from pthread_h.c:36.
[eva] using specification for function printf_va_5
-[eva] pthread_h.c:42: function printf_va_5: precondition got status valid.
+[eva] pthread_h.c:36: function printf_va_5: precondition got status valid.
[eva] Done for function printf_va_5
-[eva:alarm] pthread_h.c:45: Warning:
+[eva:alarm] pthread_h.c:39: Warning:
out of bounds read. assert \valid_read(retv);
[eva] computing for function printf_va_6 <- main.
- Called from pthread_h.c:45.
+ Called from pthread_h.c:39.
[eva] using specification for function printf_va_6
-[eva] pthread_h.c:45: function printf_va_6: precondition got status valid.
+[eva] pthread_h.c:39: function printf_va_6: precondition got status valid.
[eva] Done for function printf_va_6
[eva] Recording results for main
[eva] Done for function main
diff --git a/tests/libc/pthread_h.c b/tests/libc/pthread_h.c
index 5b875173489..28ba09c9d47 100644
--- a/tests/libc/pthread_h.c
+++ b/tests/libc/pthread_h.c
@@ -1,9 +1,3 @@
-/*run.config
- STDOPT:
- STDOPT: -cpp-extra-args="-D__FC_PTHREAD_T_IS_SCALAR -DNON_PORTABLE"
- EXIT: 1
- STDOPT: -cpp-extra-args="-DNON_PORTABLE"
- */
#define _GNU_SOURCE // if you want to compile with GCC
#include <pthread.h>
#include <stdio.h>
@@ -43,13 +37,5 @@ int main() {
return 1;
}
printf("pthread_join succeeded, retval = %d\n", *retv);
-
- // Test non-portable usage of pthread_t
-#ifdef NON_PORTABLE
- if (thread == 0) {
- return 2;
- }
-#endif
-
return 0;
}
--
GitLab