CBMC
Loading...
Searching...
No Matches
windows.c
Go to the documentation of this file.
1
/* FUNCTION: QueryPerformanceFrequency */
2
3
#ifdef _WIN32
4
#include <windows.h>
5
6
BOOL
QueryPerformanceFrequency
(
LARGE_INTEGER
*
lpFrequency
)
7
{
8
__CPROVER_HIDE
:;
9
__int64
result;
10
lpFrequency
->QuadPart=result;
11
__CPROVER_bool
error;
12
if
(error)
return
0;
13
__CPROVER_assume
(result!=0);
14
return
1;
15
}
16
#endif
17
18
/* FUNCTION: ExitThread */
19
20
#ifdef _WIN32
21
#include <windows.h>
22
23
VOID
ExitThread
(
DWORD
dwExitCode
)
24
{
25
// never returns
26
__CPROVER_assume
(0);
27
}
28
#endif
29
30
/* FUNCTION: CreateThread */
31
32
#ifdef _WIN32
33
#include <windows.h>
34
35
HANDLE
CreateThread
(
36
LPSECURITY_ATTRIBUTES
lpThreadAttributes
,
37
SIZE_T
dwStackSize
,
38
LPTHREAD_START_ROUTINE
lpStartAddress
,
39
LPVOID
lpParameter
,
40
DWORD
dwCreationFlags
,
41
LPDWORD
lpThreadId
)
42
{
43
__CPROVER_HIDE
:;
44
DWORD
thread_id
;
45
46
if
(
lpThreadId
) *
lpThreadId
=
thread_id
;
47
__CPROVER_ASYNC_1
:
lpStartAddress
(
lpParameter
);
48
49
HANDLE
handle;
50
return
handle;
51
}
52
#endif
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition
ai.h:562
__CPROVER_assume
void __CPROVER_assume(__CPROVER_bool assumption)
thread_id
const std::string thread_id
Definition
java_bytecode_concurrency_instrumentation.cpp:25
src
ansi-c
library
windows.c
Generated by
1.9.8