CBMC
threads.c
Go to the documentation of this file.
1 /* FUNCTION: thrd_create */
2 
3 // following http://en.cppreference.com/w/c/thread
4 
5 #ifndef __CPROVER_THREADS_H_INCLUDED
6 #include <threads.h>
7 #define __CPROVER_THREADS_H_INCLUDED
8 #endif
9 
10 int thrd_create(thrd_t *thr, thrd_start_t func, void *arg)
11 {
12 }
13 
14 /* FUNCTION: thrd_equal */
15 
16 #ifndef __CPROVER_THREADS_H_INCLUDED
17 #include <threads.h>
18 #define __CPROVER_THREADS_H_INCLUDED
19 #endif
20 
21 int thrd_equal( thrd_t lhs, thrd_t rhs )
22 {
23 }
24 
25 /* FUNCTION: thrd_current */
26 
27 #ifndef __CPROVER_THREADS_H_INCLUDED
28 #include <threads.h>
29 #define __CPROVER_THREADS_H_INCLUDED
30 #endif
31 
32 thrd_t thrd_current()
33 {
34 }
35 
36 /* FUNCTION: thrd_sleep */
37 
38 #ifndef __CPROVER_THREADS_H_INCLUDED
39 #include <threads.h>
40 #define __CPROVER_THREADS_H_INCLUDED
41 #endif
42 
43 int thrd_sleep(const struct timespec* time_point,
44  struct timespec* remaining)
45 {
46 }
47 
48 /* FUNCTION: thrd_yield */
49 
50 void thrd_yield()
51 {
52 }
53 
54 /* FUNCTION: thrd_exit */
55 
56 void thrd_exit(int res)
57 {
58  __CPROVER_assume(0);
59 }
60 
61 /* FUNCTION: mtx_init */
62 
63 #ifndef __CPROVER_THREADS_H_INCLUDED
64 #include <threads.h>
65 #define __CPROVER_THREADS_H_INCLUDED
66 #endif
67 
68 int mtx_init( mtx_t* mutex, int type )
69 {
70 }
71 
72 /* FUNCTION: mtx_lock */
73 
74 #ifndef __CPROVER_THREADS_H_INCLUDED
75 #include <threads.h>
76 #define __CPROVER_THREADS_H_INCLUDED
77 #endif
78 
79 int mtx_lock(mtx_t* mutex)
80 {
81 }
82 
83 /* FUNCTION: mtx_timedlock */
84 
85 #ifndef __CPROVER_THREADS_H_INCLUDED
86 #include <threads.h>
87 #define __CPROVER_THREADS_H_INCLUDED
88 #endif
89 
90 int mtx_timedlock(mtx_t *restrict mutex,
91  const struct timespec *restrict time_point)
92 {
93 
94 }
95 
96 /* FUNCTION: mtx_trylock */
97 
98 #ifndef __CPROVER_THREADS_H_INCLUDED
99 #include <threads.h>
100 #define __CPROVER_THREADS_H_INCLUDED
101 #endif
102 
103 int mtx_trylock(mtx_t *mutex)
104 {
105 }
106 
107 /* FUNCTION: mtx_unlock */
108 
109 #ifndef __CPROVER_THREADS_H_INCLUDED
110 #include <threads.h>
111 #define __CPROVER_THREADS_H_INCLUDED
112 #endif
113 
114 int mtx_unlock(mtx_t *mutex)
115 {
116 
117 }
118 
119 /* FUNCTION: mtx_destroy */
120 
121 #ifndef __CPROVER_THREADS_H_INCLUDED
122 #include <threads.h>
123 #define __CPROVER_THREADS_H_INCLUDED
124 #endif
125 
126 void mtx_destroy(mtx_t *mutex)
127 {
128 }
129 
130 /* FUNCTION: call_once */
131 
132 #ifndef __CPROVER_THREADS_H_INCLUDED
133 #include <threads.h>
134 #define __CPROVER_THREADS_H_INCLUDED
135 #endif
136 
137 void call_once(once_flag* flag, void (*func)(void))
138 {
139 }
140 
141 /* FUNCTION: cnd_init */
142 
143 #ifndef __CPROVER_THREADS_H_INCLUDED
144 #include <threads.h>
145 #define __CPROVER_THREADS_H_INCLUDED
146 #endif
147 
148 int cnd_init(cnd_t* cond)
149 {
150 }
151 
152 /* FUNCTION: cnd_signal */
153 
154 #ifndef __CPROVER_THREADS_H_INCLUDED
155 #include <threads.h>
156 #define __CPROVER_THREADS_H_INCLUDED
157 #endif
158 
159 int cnd_signal(cnd_t *cond)
160 {
161 
162 }
163 
164 /* FUNCTION: cnd_broadcast */
165 
166 #ifndef __CPROVER_THREADS_H_INCLUDED
167 #include <threads.h>
168 #define __CPROVER_THREADS_H_INCLUDED
169 #endif
170 
171 int cnd_broadcast(cnd_t *cond)
172 {
173 }
174 
175 /* FUNCTION: cnd_wait */
176 
177 #ifndef __CPROVER_THREADS_H_INCLUDED
178 #include <threads.h>
179 #define __CPROVER_THREADS_H_INCLUDED
180 #endif
181 
182 int cnd_wait(cnd_t* cond, mtx_t* mutex)
183 {
184 }
185 
186 /* FUNCTION: cnd_timedwait */
187 
188 #ifndef __CPROVER_THREADS_H_INCLUDED
189 #include <threads.h>
190 #define __CPROVER_THREADS_H_INCLUDED
191 #endif
192 
193 int cnd_timedwait(cnd_t* restrict cond, mtx_t* restrict mutex,
194  const struct timespec* restrict time_point)
195 {
196 }
197 
198 /* FUNCTION: cnd_destroy */
199 
200 #ifndef __CPROVER_THREADS_H_INCLUDED
201 #include <threads.h>
202 #define __CPROVER_THREADS_H_INCLUDED
203 #endif
204 
205 void cnd_destroy(cnd_t* cond)
206 {
207 }
__CPROVER_assume
void __CPROVER_assume(__CPROVER_bool assumption)
restrict
mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
Definition: miniBDD.cpp:551
mtx_trylock
int mtx_trylock(mtx_t *mutex)
Definition: threads.c:103
cnd_init
int cnd_init(cnd_t *cond)
Definition: threads.c:148
thrd_create
int thrd_create(thrd_t *thr, thrd_start_t func, void *arg)
Definition: threads.c:10
thrd_sleep
int thrd_sleep(const struct timespec *time_point, struct timespec *remaining)
Definition: threads.c:43
thrd_equal
int thrd_equal(thrd_t lhs, thrd_t rhs)
Definition: threads.c:21
cnd_broadcast
int cnd_broadcast(cnd_t *cond)
Definition: threads.c:171
mtx_lock
int mtx_lock(mtx_t *mutex)
Definition: threads.c:79
mtx_timedlock
int mtx_timedlock(mtx_t *restrict mutex, const struct timespec *restrict time_point)
Definition: threads.c:90
cnd_wait
int cnd_wait(cnd_t *cond, mtx_t *mutex)
Definition: threads.c:182
mtx_destroy
void mtx_destroy(mtx_t *mutex)
Definition: threads.c:126
cnd_destroy
void cnd_destroy(cnd_t *cond)
Definition: threads.c:205
call_once
void call_once(once_flag *flag, void(*func)(void))
Definition: threads.c:137
mtx_unlock
int mtx_unlock(mtx_t *mutex)
Definition: threads.c:114
thrd_current
thrd_t thrd_current()
Definition: threads.c:32
thrd_yield
void thrd_yield()
Definition: threads.c:50
thrd_exit
void thrd_exit(int res)
Definition: threads.c:56
mtx_init
int mtx_init(mtx_t *mutex, int type)
Definition: threads.c:68
cnd_signal
int cnd_signal(cnd_t *cond)
Definition: threads.c:159
cnd_timedwait
int cnd_timedwait(cnd_t *restrict cond, mtx_t *restrict mutex, const struct timespec *restrict time_point)
Definition: threads.c:193