source: CIVL/examples/pthread/seqpthread/cs_fib_false-unreach-call.c@ bb03188

main test-branch
Last change on this file since bb03188 was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 17.0 KB
Line 
1/* Generated by CSeq 0.5 (-t2 -r6 -fcbmc) 2013-06-08 01:53:37 */
2
3#include <stdlib.h>
4#include <assert.h>
5
6void __VERIFIER_assert(int cond) {
7 if (!(cond)) {
8 ERROR:
9 goto ERROR;
10 }
11 return;
12}
13
14void __VERIFIER_assume(int expression) {
15 if (!expression)
16 {
17 ERROR:
18 goto ERROR;
19 }
20}
21
22
23#define __CS_type unsigned char
24#define __CS_pthread_t unsigned char
25#define __CS_pthread_mutex_t unsigned char
26#define __CS_pthread_cond_t unsigned char
27
28//cseq: max no. of rounds and threads (parameters for the translation)
29#define __CS_ROUNDS 6
30#define __CS_THREADS 2
31
32//cseq: main extra variables used for the simulation
33//// __CS_type __k;
34
35__CS_type __CS_round = 0; //cseq: index of the current round being simulated
36
37__CS_type __CS_ret = 0; //cseq: thread exit conditions
38const __CS_type __CS_ret_PREEMPTED = 0x01; //cseq: context-switch happened before thread end
39const __CS_type __CS_ret_ERROR = 0x02; //cseq: thread returned due to an error condition
40const __CS_type __CS_ret_FINISHED = 0x04; //cseq: thread finished without errors happening
41
42__CS_type __CS_error = 0; //cseq: set whenever an error is found and checked after thread-wrapping
43
44__CS_type __CS_error_detail = 0; //cseq: error condition details (tells why __CS_error was set)
45const __CS_type __ERR_MAXTHREADS_REACHED = 0x01;
46const __CS_type __ERR_ERROR_LABEL_REACHED = 0x02;
47const __CS_type __ERR_ASSERT_FAILURE = 0x04;
48const __CS_type __ERR_UNLOCK_ATTEMPT = 0x08;
49const __CS_type __ERR_JOIN_FAILED_WRONG_THREAD_ID = 0x10;
50const __CS_type __ERR_JOIN_FAILED_THREAD_NOT_CREATED = 0x20;
51const __CS_type __ERR_COND_WAIT_MUTEX_NOT_OWNED = 0x30;
52const __CS_type __ERR_MUTEX_DESTROY = 0x40;
53const __CS_type __ERR_MUTEX_NOT_OWNED = 0x80;
54
55//cseq: handling of the status of the threads
56__CS_type __CS_thread_index; //cseq: currently running thread ranging in [1..max+1], 1 being main()
57
58__CS_type __CS_thread_allocated[__CS_THREADS+1]; //cseq: threads used in the simulation
59__CS_type __CS_thread_born_round[__CS_THREADS+1]; //cseq: round when a thread is born
60
61void *(*__CS_thread[__CS_THREADS+1])(void *); //cseq: pointers to thread functions
62
63__CS_type __CS_thread_status[__CS_ROUNDS][__CS_THREADS+1]; //cseq: thread status at a round
64const __CS_type __THREAD_UNUSED = 0x00; //cseq: not used
65const __CS_type __THREAD_RUNNING = 0x01; //cseq: successfully created
66const __CS_type __THREAD_FINISHED = 0x02; //cseq: finished with errors or without errors
67/*
68const __CS_type __THREAD_FINISHED_ERROR = 0x02; //cseq: finished with errors
69const __CS_type __THREAD_FINISHED_NO_ERROR = 0x04; //cseq: finished without errors
70*/
71
72
73__CS_type *__CS_thread_lockedon[__CS_ROUNDS][__CS_THREADS+1]; //cseq: threads waiting for conditional variables
74
75/*
76//cseq: size of dynamically allocated memory blocks, indexed by var ID
77int __CS_size[__CS_ROUNDS][9];
78int __CS_cp___CS_size[__CS_ROUNDS][9];
79*/
80
81/*
82unsigned int __CS_SwitchPoints[__CS_ROUNDS];
83unsigned int __CS_StmtCount;
84unsigned int __CS_SwitchDone;
85*/
86
87//cseq: function declarations
88int nondet_int(){
89 return 0;
90}
91
92void __CS_cs(void)
93{
94 __CS_type k;
95
96 __VERIFIER_assume(__CS_round+k < __CS_ROUNDS); // k==0 --> no switch
97 __CS_round += k;
98 // this is removed when not needed
99
100 // __CS_ret = (nondet_int() && __CS_round == __CS_ROUNDS-1)?1:__CS_ret; // preemption
101 __CS_ret = (nondet_int() && __CS_round == __CS_ROUNDS-1)?__CS_ret_PREEMPTED:__CS_ret;
102}
103/*
104void __CS_cs(void)
105{
106 if (__CS_SwitchDone == __CS_ROUNDS-1) return;
107
108 if (__CS_SwitchPoints[__CS_SwitchDone] == __CS_StmtCount++) {
109 __CS_type k;
110
111 __VERIFIER_assume(__CS_round+k < __CS_ROUNDS); // k==__CS_round --> no switch
112 __CS_round += k;
113 //__VERIFIER_assume(__CS_thread_lockedon[__CS_round][__CS_thread_index] == 0);
114
115 __CS_SwitchDone++;
116 //__CS_StmtCount = 0;
117 }
118}
119*/
120
121int __CS_pthread_mutex_init(__CS_pthread_mutex_t *mutex, void *attr)
122{
123 return 0;
124}
125
126int __CS_pthread_mutex_destroy(__CS_pthread_mutex_t *lock)
127{
128 if (*lock != __CS_thread_index && *lock != 0) {
129 __CS_error = 1;
130 __CS_ret = __CS_ret_ERROR;
131 __CS_error_detail = __ERR_MUTEX_DESTROY;
132 }
133 else *lock = 0;
134
135 return 0;
136}
137
138int __CS_pthread_mutex_lock(__CS_pthread_mutex_t *lock)
139{
140 if (*lock == 0) *lock = (__CS_thread_index+1);
141 else { __CS_ret = __CS_ret_PREEMPTED; return 1; }
142
143 return 0;
144}
145
146int __CS_pthread_mutex_unlock(__CS_pthread_mutex_t *lock)
147{
148 if (*lock != (__CS_thread_index+1)) {
149 __CS_error = 1;
150 __CS_ret = __CS_ret_ERROR;
151 __CS_error_detail = __ERR_UNLOCK_ATTEMPT;
152 return 1;
153 } else *lock = 0;
154
155 return 0;
156}
157
158int __CS_pthread_cond_init(__CS_pthread_cond_t *cond, void *attr)
159{
160 return 0;
161}
162
163int __CS_pthread_cond_signal(__CS_pthread_cond_t *cond)
164{
165 int j;
166
167 for (j=0; j<=__CS_THREADS; j++)
168 if (__CS_thread_lockedon[__CS_round][j] == cond)
169 __CS_thread_lockedon[__CS_round][j] = 0;
170
171 return 0;
172}
173
174int __CS_pthread_cond_broadcast(__CS_pthread_cond_t *cond)
175{
176 int j;
177
178 for (j=0; j<=__CS_THREADS; j++)
179 if (__CS_thread_lockedon[__CS_round][j] == cond)
180 __CS_thread_lockedon[__CS_round][j] = 0;
181
182 return 0;
183}
184
185int __CS_pthread_cond_wait(__CS_pthread_cond_t *cond, __CS_pthread_mutex_t *lock)
186{
187 // __CS_pthread_mutex_unlock(mutex);
188 if (*lock != (__CS_thread_index+1)) {
189 __CS_error = 1;
190 __CS_ret = __CS_ret_ERROR;
191 __CS_error_detail = __ERR_COND_WAIT_MUTEX_NOT_OWNED;
192 return 1;
193 }
194 else *lock = 0;
195
196 __CS_thread_lockedon[__CS_round][__CS_thread_index] = cond;
197 __CS_ret = __CS_ret_PREEMPTED; // force context-switch
198
199 // __CS_pthread_mutex_lock(mutex);
200 if (*lock == 0) *lock = __CS_thread_index+1;
201 else { __CS_ret = __CS_ret_PREEMPTED; return 1; }
202
203 return 0;
204}
205
206void __CS_assert(int expr)
207{
208 if (!expr) {
209 __CS_error = 1;
210 __CS_error_detail = __ERR_ASSERT_FAILURE;
211 __CS_ret = __CS_ret_ERROR;
212 }
213}
214
215void __CS_assume(int expr)
216{
217 if (!expr) __CS_ret = __CS_ret_PREEMPTED;
218}
219
220int __CS_pthread_join(__CS_pthread_t thread, void **value_ptr)
221{
222 // checking index range
223 if (thread != 123 && thread > __CS_THREADS+1)
224 {
225 __CS_error = 1;
226 __CS_error_detail = __ERR_JOIN_FAILED_WRONG_THREAD_ID;
227 __CS_ret = __CS_ret_ERROR;
228 return 0;
229 }
230
231 if ( thread == 123 || __CS_thread_status[__CS_round][thread] == __THREAD_RUNNING )
232 {
233 __CS_ret = __CS_ret_PREEMPTED;
234 return 0;
235 }
236
237 if (__CS_thread_status[__CS_round][thread] == __THREAD_UNUSED)
238 {
239 __CS_error = 1;
240 __CS_error_detail = __ERR_JOIN_FAILED_THREAD_NOT_CREATED;
241 __CS_ret = __CS_ret_ERROR;
242 return 0;
243 }
244
245 /*
246 __VERIFIER_assume( __CS_thread_status[__CS_round][thread] == __THREAD_FINISHED_ERROR ||
247 __CS_thread_status[__CS_round][thread] == __THREAD_FINISHED_NO_ERROR );
248 */
249
250 __VERIFIER_assume( __CS_thread_status[__CS_round][thread] == __THREAD_FINISHED );
251
252 return 0;
253}
254
255int __CS_pthread_create(__CS_pthread_t *id1, void *attr, void *(*t1)(void*), void *arg)
256{
257 /* if (nondet_int()) { *id = -1; return -1; } */
258
259 /*
260 if (__CS_thread_index == __CS_THREADS+1) {
261 __CS_error = 1;
262 __CS_ret = __CS_ret_ERROR;
263 __CS_error_detail = __ERR_MAXTHREADS_REACHED;
264 return 1;
265 }
266 */
267
268 if (__CS_thread_index == __CS_THREADS) {
269 *id1 = 123;
270 return -1;
271 }
272
273 __CS_thread_index++;
274
275 __CS_thread_allocated[__CS_thread_index] = 1;
276 __CS_thread_born_round[__CS_thread_index] = __CS_round;
277 __CS_thread[__CS_thread_index] = t1;
278 __CS_thread_status[__CS_round][__CS_thread_index] = __THREAD_RUNNING;
279
280 *id1 = __CS_thread_index;
281
282 return __CS_thread_index;
283}
284
285/*
286void *__CS_malloc(int varID, int size)
287{
288 __CS_size[__CS_round][varID] = size;
289 return malloc((size_t)size);
290}
291
292void __CS_free(int varID, void *ptr)
293{
294 __CS_size[__CS_round][varID] = 0;
295}
296
297int __CS_memcmp(void *a, void *b, int size)
298{
299 int j;
300
301 for (j=0; j<size; j++)
302 if (*(char *)(a+j) != *(char *)(b+j))
303
304 return 0;
305}
306*/
307//cseq: Sequentialised code starts here.
308int i[__CS_ROUNDS] = {1};
309int j[__CS_ROUNDS] = {1};
310union __CS__u {
311 int i[__CS_ROUNDS];
312 int j[__CS_ROUNDS];
313};
314
315union __CS__u __CS_u;
316
317void *t1(void *arg)
318{
319 int k = 0;
320 __CS_cs(); if (__CS_ret != 0) return 0;
321 for (k = 0; k < 5; k++)
322 {
323 __CS_cs(); if (__CS_ret != 0) return 0;
324 //cseq: Translation for the assignment statement "i[__CS_round] += j[__CS_round]", case 2
325 __CS_u.i[__CS_round] = i[__CS_round];
326 i[__CS_round] += j[__CS_round];
327 if (__CS_ret) i[__CS_round]= __CS_u.i[__CS_round];
328 }
329
330 __CS_cs(); if (__CS_ret != 0) return 0;
331 ;
332 __CS_cs(); if (__CS_ret != 0) return 0;
333}
334
335void *t2(void *arg)
336{
337 int k = 0;
338 __CS_cs(); if (__CS_ret != 0) return 0;
339 for (k = 0; k < 5; k++)
340 {
341 __CS_cs(); if (__CS_ret != 0) return 0;
342 //cseq: Translation for the assignment statement "j[__CS_round] += i[__CS_round]", case 2
343 __CS_u.j[__CS_round] = j[__CS_round];
344 j[__CS_round] += i[__CS_round];
345 if (__CS_ret) j[__CS_round]= __CS_u.j[__CS_round];
346 }
347
348 __CS_cs(); if (__CS_ret != 0) return 0;
349 ;
350 __CS_cs(); if (__CS_ret != 0) return 0;
351}
352
353void *main_thread(void *arg)
354{
355 int __CS_main_arg_argc;
356 char **argv;
357 __CS_pthread_t id1;
358 __CS_pthread_t id2;
359 __CS_cs(); if (__CS_ret != 0) return 0;
360 __CS_pthread_create(&id1, 0, t1, 0);
361 __CS_cs(); if (__CS_ret != 0) return 0;
362 __CS_pthread_create(&id2, 0, t2, 0);
363 __CS_cs(); if (__CS_ret != 0) return 0;
364 if ((i[__CS_round] >= 144) || (j[__CS_round] >= 144))
365 {
366 __CS_cs(); if (__CS_ret != 0) return 0;
367 goto __CS_ERROR;
368 __CS_cs(); if (__CS_ret != 0) return 0;
369 __CS_ERROR: __CS_error = 1; __CS_ret = __CS_ret_ERROR; __CS_error_detail = __ERR_ERROR_LABEL_REACHED; return 0;
370 __CS_cs(); if (__CS_ret != 0) return 0;
371 ;
372
373 __CS_cs(); if (__CS_ret != 0) return 0;
374 }
375 __CS_cs(); if (__CS_ret != 0) return 0;
376 }
377
378int main(int argc, char **argv)
379{
380 //cseq: Copies of global variables
381 __CS_type __CS_cp___CS_thread_status[__CS_ROUNDS][__CS_THREADS+1];
382 __CS_type *__CS_cp___CS_thread_lockedon[__CS_ROUNDS][__CS_THREADS+1];
383 int __CS_cp_i[__CS_ROUNDS];
384 int __CS_cp_j[__CS_ROUNDS];
385
386 //cseq: Copy statements for global variables:
387 //cseq: for each global variable x,
388 //cseq: copy into x[1...___CS_ROUNDS] <--- __CS_cp_x[1..___CS_ROUNDS].
389 //cseq: This is used to fill global variables with non-initialised data.
390 __CS_thread_status[1][0] = __CS_cp___CS_thread_status[1][0]; //cseq: Copy of __CS_thread_status
391 __CS_thread_status[2][0] = __CS_cp___CS_thread_status[2][0];
392 __CS_thread_status[3][0] = __CS_cp___CS_thread_status[3][0];
393 __CS_thread_status[4][0] = __CS_cp___CS_thread_status[4][0];
394 __CS_thread_status[5][0] = __CS_cp___CS_thread_status[5][0];
395 __CS_thread_status[1][1] = __CS_cp___CS_thread_status[1][1];
396 __CS_thread_status[2][1] = __CS_cp___CS_thread_status[2][1];
397 __CS_thread_status[3][1] = __CS_cp___CS_thread_status[3][1];
398 __CS_thread_status[4][1] = __CS_cp___CS_thread_status[4][1];
399 __CS_thread_status[5][1] = __CS_cp___CS_thread_status[5][1];
400 __CS_thread_status[1][2] = __CS_cp___CS_thread_status[1][2];
401 __CS_thread_status[2][2] = __CS_cp___CS_thread_status[2][2];
402 __CS_thread_status[3][2] = __CS_cp___CS_thread_status[3][2];
403 __CS_thread_status[4][2] = __CS_cp___CS_thread_status[4][2];
404 __CS_thread_status[5][2] = __CS_cp___CS_thread_status[5][2];
405 __CS_thread_lockedon[1][0] = __CS_cp___CS_thread_lockedon[1][0]; //cseq: Copy of __CS_thread_lockedon
406 __CS_thread_lockedon[2][0] = __CS_cp___CS_thread_lockedon[2][0];
407 __CS_thread_lockedon[3][0] = __CS_cp___CS_thread_lockedon[3][0];
408 __CS_thread_lockedon[4][0] = __CS_cp___CS_thread_lockedon[4][0];
409 __CS_thread_lockedon[5][0] = __CS_cp___CS_thread_lockedon[5][0];
410 __CS_thread_lockedon[1][1] = __CS_cp___CS_thread_lockedon[1][1];
411 __CS_thread_lockedon[2][1] = __CS_cp___CS_thread_lockedon[2][1];
412 __CS_thread_lockedon[3][1] = __CS_cp___CS_thread_lockedon[3][1];
413 __CS_thread_lockedon[4][1] = __CS_cp___CS_thread_lockedon[4][1];
414 __CS_thread_lockedon[5][1] = __CS_cp___CS_thread_lockedon[5][1];
415 __CS_thread_lockedon[1][2] = __CS_cp___CS_thread_lockedon[1][2];
416 __CS_thread_lockedon[2][2] = __CS_cp___CS_thread_lockedon[2][2];
417 __CS_thread_lockedon[3][2] = __CS_cp___CS_thread_lockedon[3][2];
418 __CS_thread_lockedon[4][2] = __CS_cp___CS_thread_lockedon[4][2];
419 __CS_thread_lockedon[5][2] = __CS_cp___CS_thread_lockedon[5][2];
420 i[1] = __CS_cp_i[1]; //cseq: Copy of i
421 i[2] = __CS_cp_i[2];
422 i[3] = __CS_cp_i[3];
423 i[4] = __CS_cp_i[4];
424 i[5] = __CS_cp_i[5];
425 j[1] = __CS_cp_j[1]; //cseq: Copy of j
426 j[2] = __CS_cp_j[2];
427 j[3] = __CS_cp_j[3];
428 j[4] = __CS_cp_j[4];
429 j[5] = __CS_cp_j[5];
430
431 //cseq: create new thread for the main function
432 __CS_round = 0;
433 __CS_thread_index = 0;
434 __CS_thread_born_round[0] = __CS_round;
435 __CS_thread_status[0][0] = __THREAD_RUNNING;
436 __CS_thread[0] = main_thread;
437 __CS_thread_allocated[0] = 1;
438
439 //cseq: simulation of the threads
440 if (__CS_thread_allocated[0] == 1) {
441 __CS_round = __CS_thread_born_round[0];
442 __CS_ret = 0;
443 __CS_thread[0](0);
444 if (__CS_ret!=__CS_ret_PREEMPTED) __CS_thread_status[__CS_round][0] = __THREAD_FINISHED;
445 }
446
447 if (__CS_thread_allocated[1] == 1) {
448 __CS_round = __CS_thread_born_round[1];
449 __CS_ret = 0;
450 __CS_thread[1](0);
451 if (__CS_ret!=__CS_ret_PREEMPTED) __CS_thread_status[__CS_round][1] = __THREAD_FINISHED;
452 }
453
454 if (__CS_thread_allocated[2] == 1) {
455 __CS_round = __CS_thread_born_round[2];
456 __CS_ret = 0;
457 __CS_thread[2](0);
458 if (__CS_ret!=__CS_ret_PREEMPTED) __CS_thread_status[__CS_round][2] = __THREAD_FINISHED;
459 }
460
461
462 //cseq: Consistency checks for global variables:
463 //cseq: for each global variable x,
464 //cseq: check that x[0...___CS_ROUNDS-1] == __CS_cp_x[1..___CS_ROUNDS].
465 __VERIFIER_assume(__CS_thread_status[0][0] == __CS_cp___CS_thread_status[1][0]); //cseq: Consistency of __CS_thread_status
466 __VERIFIER_assume(__CS_thread_status[1][0] == __CS_cp___CS_thread_status[2][0]);
467 __VERIFIER_assume(__CS_thread_status[2][0] == __CS_cp___CS_thread_status[3][0]);
468 __VERIFIER_assume(__CS_thread_status[3][0] == __CS_cp___CS_thread_status[4][0]);
469 __VERIFIER_assume(__CS_thread_status[4][0] == __CS_cp___CS_thread_status[5][0]);
470 __VERIFIER_assume(__CS_thread_status[0][1] == __CS_cp___CS_thread_status[1][1]);
471 __VERIFIER_assume(__CS_thread_status[1][1] == __CS_cp___CS_thread_status[2][1]);
472 __VERIFIER_assume(__CS_thread_status[2][1] == __CS_cp___CS_thread_status[3][1]);
473 __VERIFIER_assume(__CS_thread_status[3][1] == __CS_cp___CS_thread_status[4][1]);
474 __VERIFIER_assume(__CS_thread_status[4][1] == __CS_cp___CS_thread_status[5][1]);
475 __VERIFIER_assume(__CS_thread_status[0][2] == __CS_cp___CS_thread_status[1][2]);
476 __VERIFIER_assume(__CS_thread_status[1][2] == __CS_cp___CS_thread_status[2][2]);
477 __VERIFIER_assume(__CS_thread_status[2][2] == __CS_cp___CS_thread_status[3][2]);
478 __VERIFIER_assume(__CS_thread_status[3][2] == __CS_cp___CS_thread_status[4][2]);
479 __VERIFIER_assume(__CS_thread_status[4][2] == __CS_cp___CS_thread_status[5][2]);
480 __VERIFIER_assume(__CS_thread_lockedon[0][0] == __CS_cp___CS_thread_lockedon[1][0]); //cseq: Consistency of __CS_thread_lockedon
481 __VERIFIER_assume(__CS_thread_lockedon[1][0] == __CS_cp___CS_thread_lockedon[2][0]);
482 __VERIFIER_assume(__CS_thread_lockedon[2][0] == __CS_cp___CS_thread_lockedon[3][0]);
483 __VERIFIER_assume(__CS_thread_lockedon[3][0] == __CS_cp___CS_thread_lockedon[4][0]);
484 __VERIFIER_assume(__CS_thread_lockedon[4][0] == __CS_cp___CS_thread_lockedon[5][0]);
485 __VERIFIER_assume(__CS_thread_lockedon[0][1] == __CS_cp___CS_thread_lockedon[1][1]);
486 __VERIFIER_assume(__CS_thread_lockedon[1][1] == __CS_cp___CS_thread_lockedon[2][1]);
487 __VERIFIER_assume(__CS_thread_lockedon[2][1] == __CS_cp___CS_thread_lockedon[3][1]);
488 __VERIFIER_assume(__CS_thread_lockedon[3][1] == __CS_cp___CS_thread_lockedon[4][1]);
489 __VERIFIER_assume(__CS_thread_lockedon[4][1] == __CS_cp___CS_thread_lockedon[5][1]);
490 __VERIFIER_assume(__CS_thread_lockedon[0][2] == __CS_cp___CS_thread_lockedon[1][2]);
491 __VERIFIER_assume(__CS_thread_lockedon[1][2] == __CS_cp___CS_thread_lockedon[2][2]);
492 __VERIFIER_assume(__CS_thread_lockedon[2][2] == __CS_cp___CS_thread_lockedon[3][2]);
493 __VERIFIER_assume(__CS_thread_lockedon[3][2] == __CS_cp___CS_thread_lockedon[4][2]);
494 __VERIFIER_assume(__CS_thread_lockedon[4][2] == __CS_cp___CS_thread_lockedon[5][2]);
495 __VERIFIER_assume(i[0] == __CS_cp_i[1]); //cseq: Consistency of i
496 __VERIFIER_assume(i[1] == __CS_cp_i[2]);
497 __VERIFIER_assume(i[2] == __CS_cp_i[3]);
498 __VERIFIER_assume(i[3] == __CS_cp_i[4]);
499 __VERIFIER_assume(i[4] == __CS_cp_i[5]);
500 __VERIFIER_assume(j[0] == __CS_cp_j[1]); //cseq: Consistency of j
501 __VERIFIER_assume(j[1] == __CS_cp_j[2]);
502 __VERIFIER_assume(j[2] == __CS_cp_j[3]);
503 __VERIFIER_assume(j[3] == __CS_cp_j[4]);
504 __VERIFIER_assume(j[4] == __CS_cp_j[5]);
505
506
507 //cseq: Error check
508 __VERIFIER_assert(__CS_error_detail != __ERR_MAXTHREADS_REACHED);
509 __VERIFIER_assert(__CS_error_detail != __ERR_ASSERT_FAILURE);
510 __VERIFIER_assert(__CS_error_detail != __ERR_ERROR_LABEL_REACHED);
511 __VERIFIER_assert(__CS_error_detail != __ERR_UNLOCK_ATTEMPT);
512 __VERIFIER_assert(__CS_error_detail != __ERR_JOIN_FAILED_WRONG_THREAD_ID);
513 __VERIFIER_assert(__CS_error_detail != __ERR_JOIN_FAILED_THREAD_NOT_CREATED);
514 __VERIFIER_assert(__CS_error != 1);
515}
516
517
Note: See TracBrowser for help on using the repository browser.