CBMC
Toggle main menu visibility
Main Page
Related Pages
Namespaces
Namespace List
Namespace Members
All
a
c
d
e
f
g
j
l
m
r
t
w
Functions
a
c
d
f
g
r
t
w
Typedefs
Enumerations
Classes
Class List
Class Hierarchy
Class Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Variables
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Typedefs
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
Enumerations
a
b
c
d
e
f
g
i
k
l
m
o
p
r
s
t
u
v
w
Enumerator
a
b
c
d
e
f
h
i
k
l
m
n
o
p
q
r
s
t
u
v
Related Symbols
b
c
d
e
g
i
j
m
n
o
s
t
u
v
Files
File List
File Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
r
s
t
u
v
w
x
y
z
Variables
_
a
b
c
d
e
f
g
i
l
m
n
o
p
r
s
t
u
w
y
Typedefs
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
r
s
t
u
v
w
Enumerations
_
a
b
c
d
f
g
i
l
m
p
r
s
t
u
v
w
Enumerator
_
a
c
d
e
f
g
h
i
l
m
n
o
p
r
s
t
u
v
w
Macros
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
q
r
s
t
u
v
w
x
y
•
All
Classes
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Friends
Macros
Modules
Pages
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
}
5
__CPROVER_size_t
_beginthread
( {
…
}
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
}
21
__CPROVER_size_t
_beginthreadex
( {
…
}
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