CBMC
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
__CPROVER_assume
void __CPROVER_assume(__CPROVER_bool assumption)
thread_id
const std::string thread_id
Definition: java_bytecode_concurrency_instrumentation.cpp:25