CBMC
process.c
Go to the documentation of this file.
1 /* FUNCTION: _beginthread */
2 
3 __CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t(void);
4 
5 __CPROVER_size_t _beginthread(
6  void (*start_address)(void *),
7  unsigned stack_size,
8  void *arglist)
9 {
10  __CPROVER_HIDE:;
11  __CPROVER_ASYNC_1: start_address(arglist);
12  (void)stack_size;
13  __CPROVER_size_t handle=__VERIFIER_nondet___CPROVER_size_t();
14  return handle;
15 }
16 
17 /* FUNCTION: _beginthreadex */
18 
19 __CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t(void);
20 
21 __CPROVER_size_t _beginthreadex(
22  void *security,
23  unsigned stack_size,
24  unsigned (*start_address )(void *),
25  void *arglist,
26  unsigned initflag,
27  unsigned *thrdaddr)
28 {
29  __CPROVER_HIDE:;
30  __CPROVER_ASYNC_1: start_address(arglist);
31  if(security)
32  (void)*(char*)security;
33  (void)stack_size;
34  (void)initflag;
35  (void)*thrdaddr;
36  __CPROVER_size_t handle=__VERIFIER_nondet___CPROVER_size_t();
37  return handle;
38 }
_beginthread
__CPROVER_size_t _beginthread(void(*start_address)(void *), unsigned stack_size, void *arglist)
Definition: process.c:5
_beginthreadex
__CPROVER_size_t _beginthreadex(void *security, unsigned stack_size, unsigned(*start_address)(void *), void *arglist, unsigned initflag, unsigned *thrdaddr)
Definition: process.c:21
__VERIFIER_nondet___CPROVER_size_t
__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t(void)