CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
10int 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
21int 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
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
43int thrd_sleep(const struct timespec* time_point,
44 struct timespec* remaining)
45{
46}
47
48/* FUNCTION: thrd_yield */
49
50void thrd_yield()
51{
52}
53
54/* FUNCTION: thrd_exit */
55
56void 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
68int 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
79int 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
90int 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
103int 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
114int 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
126void 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
137void 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
148int 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
159int 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
171int 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
182int 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
193int 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
205void cnd_destroy(cnd_t* cond)
206{
207}
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)
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