CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
windows.c
Go to the documentation of this file.
1/* FUNCTION: QueryPerformanceFrequency */
2
3#ifdef _WIN32
4#include <windows.h>
5
6BOOL 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
23VOID 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
35HANDLE 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