source: CIVL/examples/pthread/esbmc/stateful01_false.c@ beab7f2

main test-branch
Last change on this file since beab7f2 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: 788 bytes
Line 
1extern void __VERIFIER_error();
2
3#include <pthread.h>
4
5pthread_mutex_t ma, mb;
6int data1, data2;
7
8void * thread1(void * arg)
9{
10 pthread_mutex_lock(&ma);
11 data1++;
12 pthread_mutex_unlock(&ma);
13
14 pthread_mutex_lock(&ma);
15 data2++;
16 pthread_mutex_unlock(&ma);
17}
18
19
20void * thread2(void * arg)
21{
22 pthread_mutex_lock(&ma);
23 data1+=5;
24 pthread_mutex_unlock(&ma);
25
26 pthread_mutex_lock(&ma);
27 data2-=6;
28 pthread_mutex_unlock(&ma);
29}
30
31
32int main()
33{
34 pthread_t t1, t2;
35
36 pthread_mutex_init(&ma, 0);
37 pthread_mutex_init(&mb, 0);
38
39 data1 = 10;
40 data2 = 10;
41
42 pthread_create(&t1, 0, thread1, 0);
43 pthread_create(&t2, 0, thread2, 0);
44
45 pthread_join(t1, 0);
46 pthread_join(t2, 0);
47
48 if (data1==16 && data2==5)
49 {
50 ERROR: __VERIFIER_error();
51 ;
52 }
53
54 return 0;
55}
56
Note: See TracBrowser for help on using the repository browser.