[Libc] add __FC_PTHREAD_T_IS_SCALAR to handle non-portable code

share/libc/__fc_define_pthread_types.h

@@ -44,7 +44,14 @@ 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 { int _fc; } pthread_t;
+#endif
 __END_DECLS
 __POP_FC_STDLIB
 #endif

tests/libc/oracle/pthread_h.res.oracle → tests/libc/oracle/pthread_h.0.res.oracle

@@ -6,73 +6,73 @@
   retval ∈ {0}
   v ∈ [--..--]
 [eva] computing for function pthread_create <- main.
-  Called from pthread_h.c:17.
+  Called from pthread_h.c:23.
 [eva] using specification for function pthread_create
-[eva] pthread_h.c:17: 
+[eva] pthread_h.c:23: 
   function pthread_create: precondition 'valid_thread' got status valid.
-[eva] pthread_h.c:17: 
+[eva] pthread_h.c:23: 
   function pthread_create: precondition 'valid_null_attr' got status valid.
-[eva] pthread_h.c:17: 
+[eva] pthread_h.c:23: 
   function pthread_create: precondition 'valid_routine' got status valid.
-[eva] pthread_h.c:17: 
+[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:19.
+  Called from pthread_h.c:25.
 [eva] using specification for function printf_va_2
-[eva] pthread_h.c:19: function printf_va_2: precondition got status valid.
+[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:22.
+  Called from pthread_h.c:28.
 [eva] using specification for function printf_va_3
-[eva] pthread_h.c:22: function printf_va_3: precondition got status valid.
+[eva] pthread_h.c:28: 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:23.
+  Called from pthread_h.c:29.
 [eva] using specification for function pthread_setname_np
-[eva] pthread_h.c:23: 
+[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:26.
+  Called from pthread_h.c:32.
 [eva] using specification for function pthread_getname_np
-[eva] pthread_h.c:26: 
+[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:27.
+  Called from pthread_h.c:33.
 [eva] using specification for function printf_va_4
-[eva:alarm] pthread_h.c:27: Warning: 
+[eva:alarm] pthread_h.c:33: Warning: 
   function printf_va_4: precondition valid_read_string(param0) got status unknown.
-[eva] pthread_h.c:27: 
+[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:32.
+  Called from pthread_h.c:38.
 [eva] computing for function printf_va_1 <- start_routine <- main.
-  Called from pthread_h.c:8.
+  Called from pthread_h.c:14.
 [eva] using specification for function printf_va_1
-[eva] pthread_h.c:8: function printf_va_1: precondition got status valid.
+[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:34.
+  Called from pthread_h.c:40.
 [eva] using specification for function pthread_join
-[eva] pthread_h.c:34: 
+[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:36.
+  Called from pthread_h.c:42.
 [eva] using specification for function printf_va_5
-[eva] pthread_h.c:36: function printf_va_5: precondition got status valid.
+[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:39: Warning: 
+[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:39.
+  Called from pthread_h.c:45.
 [eva] using specification for function printf_va_6
-[eva] pthread_h.c:39: function printf_va_6: precondition got status valid.
+[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

tests/libc/oracle/pthread_h.1.res.oracle

+[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] ∈ [--..--]

tests/libc/oracle/pthread_h.2.res.oracle

+[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.

tests/libc/pthread_h.c

+/*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>
@@ -37,5 +43,13 @@ 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;
 }