[__spawned_thread.pointer_dereference.1] line 41 no candidates for dereferenced function pointer: FAILURE

[bupt01]

CBMC version:5.86.0 (cbmc-5.86.0-19-g6066b3409c) Operating system:Ubuntu 22.04.2 Exact command line resulting in the issue: ./cbmc /home/modelchecker/benchmark/Prog/test.c What behaviour did you expect: line 19 assertion x1 == x2: Failture What happened instead:line 19 assertion x1 == x2: SUCCESS、 [spawned_thread.pointer_dereference.1] line 41 no candidates for dereferenced function pointer: FAILURE C program: OUTPUT: `CBMC version 5.86.0 (cbmc-5.86.0-19-g6066b3409c) 64-bit x86_64 linux Parsing /home/modelchecker/benchmark/Prog/test.c Converting Type-checking test Generating GOTO Program Adding CPROVER library (x86_64) Removal of function pointers and virtual functions file <builtin-library-spawned_thread> line 41 function spawned_thread: replacing function pointer by 0 possible targets Generic Property Instrumentation Running with 8 object bits, 56 offset bits (default) Starting Bounded Model Checking aborting path on assume(false) at file line 41 function spawned_thread thread 1 Runtime Symex: 0.00352855s Adding SC constraints size of program expression: 242 steps no slicing due to threads Generated 1 VCC(s), 1 remaining after simplification Runtime Postprocess Equation: 0.000438464s Passing problem to propositional reduction converting SSA Runtime Convert SSA: 0.00177724s Running propositional reduction Post-processing Runtime Post-process: 0.000188041s Solving with MiniSAT 2.2.1 with simplifier 3140 variables, 2219 clauses SAT checker: instance is SATISFIABLE Runtime Solver: 0.00459519s Runtime decision procedure: 0.00641961s

** Results: /home/modelchecker/benchmark/Prog/test.c function thread1 [thread1.assertion.1] line 19 assertion x1 == x2: SUCCESS

function __spawned_thread [__spawned_thread.pointer_dereference.1] line 41 no candidates for dereferenced function pointer: FAILURE function pthread_mutex_unlock [pthread_mutex_unlock.assertion.1] line 39 must hold lock upon unlock: SUCCESS ** 1 of 3 failed (2 iterations) VERIFICATION FAILED`

[bupt01]

I have resolved it. The lines "void thread1()" and "void thread1()" should be replaced with "void thread1(void arg)" and "void thread1(void arg)" respectively.

[TGWDB]

I have resolved it. The lines "void thread1()" and "void thread1()" should be replaced with "void thread1(void arg)" and "void thread1(void arg)" respectively.

Should we close this issue then?