Ticket #7: model.c

File model.c, 883 bytes (added by Vladimír Štill, 13 months ago)

a modified version of pthread-ext/09_fmaxsym_true-unreach-call.c (for bug 3)

Line 
1extern void __VERIFIER_assume(int);
2extern void __VERIFIER_error() __attribute__ ((__noreturn__));
3extern int __VERIFIER_nondet_int();
4
5#include <pthread.h>
6
7volatile int max = 0x80000000, m = 0;
8void __VERIFIER_atomic_acquire()
9{
10 __VERIFIER_assume(!!(m==0));
11 m = 1;
12}
13void __VERIFIER_atomic_release()
14{
15 __VERIFIER_assume(!!(m==1));
16 m = 0;
17}
18int storage[2*3];
19inline void findMax(int offset)
20{
21 int i;
22 int e;
23 for(i = offset; i < offset+2; i++) {
24  e = storage[i];
25  __VERIFIER_atomic_acquire();
26  {
27   if(e > max) {
28    max = e;
29   }
30  }
31  __VERIFIER_atomic_release();
32  { if(!(e <= max)) { ERROR: __VERIFIER_error();(void)0; } };
33 }
34}
35void* thr1(void* arg) {
36  int offset=__VERIFIER_nondet_int();
37 __VERIFIER_assume(!!(offset % 2 == 0 && offset >= 0 && offset < 2*3));
38 findMax(offset);
39  return 0;
40}
41int main(){
42  pthread_t t;
43 while(1) { pthread_create(&t, 0, thr1, 0); }
44}