CBMC
Loading...
Searching...
No Matches
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
}
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition
ai.h:562
_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)
src
ansi-c
library
process.c
Generated by
1.9.8