./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i


--------------------------------------------------------------------------------


Deagle version 2.1 64-bit x86_64 linux
which contains:
CBMC version 5.67.0 (SVCOMP2023_221122-2-g2121ef1a2) 64-bit x86_64 linux
Parsing /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i
Converting
Type-checking scull
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_mutex_destroy> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_destroy"
old definition in module scull file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i line 514
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_destroy> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-pthread_mutex_init> line 27: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_init"
old definition in module scull file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i line 511
signed int (pthread_mutex_t *, const pthread_mutexattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_init> line 27
signed int (pthread_mutex_t *mutex, const pthread_mutexattr_t *mutexattr)
file <builtin-library-pthread_mutex_lock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_lock"
old definition in module scull file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i line 518
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_lock> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-pthread_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module scull file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i line 405
signed int (pthread_t *, const pthread_attr_t *, void * (*)(void *), void *)
new definition in module <built-in-library> file <builtin-library-pthread_create> line 20
signed int (pthread_t *thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
file <builtin-library-pthread_mutex_unlock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_unlock"
old definition in module scull file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i line 523
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_unlock> line 17
signed int (pthread_mutex_t *mutex)
Removal of function pointers and virtual functions
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 3 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:889:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:906:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:907:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:741:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:697:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:916:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:917:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:741:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:701:3)
[Warning][Deadcode] Function "reach_error" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:12:1)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:68:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:73:1)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:78:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:83:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:88:1)
[Warning][Deadcode] Function "__get_user" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:703:1)
[Warning][Deadcode] Function "__put_user" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:707:1)
[Warning][Deadcode] Function "scull_ioctl" will never be called: 51LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:809:1)
[Warning][Deadcode] Function "scull_llseek" will never be called: 15LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:866:1)
[Warning][Race] Memory location dev_data@scull.i:713:5 (race with conf. 110):
  read with {lock:lock, thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:765:3)
  read with {lock:lock, thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:931:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:796:3)
  write with {thread:([loader@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:724:3)
  write with {lock:lock, thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:724:3)
  write with {lock:lock, thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:931:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:724:3)
[Warning][Race] Memory location dev_quantum@scull.i:714:5 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:748:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:931:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:781:3)
  write with {thread:([loader@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:722:3)
  write with {lock:lock, thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:722:3)
  write with {lock:lock, thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:931:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:722:3)
[Warning][Race] Memory location dev_size@scull.i:716:5 (race with conf. 110):
  read with {lock:lock, thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:755:3)
  read with {lock:lock, thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:757:3)
  read with {lock:lock, thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:758:5)
  read with {lock:lock, thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:931:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:802:3)
  write with {thread:([loader@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:721:3)
  write with {lock:lock, thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:721:3)
  write with {lock:lock, thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:931:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:721:3)
  write with {lock:lock, thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:931:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:803:5)
[Warning][Race] Memory location dev_qset@scull.i:715:5 (race with conf. 110):
  read with {thread:([loader@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:720:3)
  read with {lock:lock, thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:720:3)
  read with {lock:lock, thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:931:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:720:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:748:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:931:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:781:3)
  write with {thread:([loader@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:723:3)
  write with {lock:lock, thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:723:3)
  write with {lock:lock, thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:931:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:723:3)

Summary for all memory locations:
	safe:            4
	vulnerable:      0
	unsafe:          4
	-------------------
	total:           8
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Handling datarace, passing the problem to goblint first
getcwd: /mnt/goblint-svcomp/benchexec/tools-pldi/deagle
/mnt/goblint-svcomp/benchexec/tools-pldi/deagle/goblint/goblint /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 720 721 722 723 724 725 748 749 755 756 757 758 759 765 766 781 782 796 797 802 803 804 889 890 906 907 916 917 
The number of races before goblint filter: 166
The number of races after goblint filter: 49
Race categories: 26
	724(1) - 724(1) dev_data:
		dev_data#2 dev_data#3
		dev_data#2 dev_data#7
		dev_data#3 dev_data#7
	724(1) - 765(1) dev_data:
		dev_data#2 dev_data#4
		dev_data#2 dev_data#5
		dev_data#2 dev_data#6
	724(1) - 796(1) dev_data:
		dev_data#2 dev_data#8
		dev_data#2 dev_data#9
		dev_data#3 dev_data#8
		dev_data#3 dev_data#9
	765(1) - 724(1) dev_data:
		dev_data#4 dev_data#7
		dev_data#5 dev_data#7
		dev_data#6 dev_data#7
	720(1) - 723(1) dev_qset:
		dev_qset#2 dev_qset#5
		dev_qset#2 dev_qset#8
		dev_qset#4 dev_qset#8
	723(1) - 720(1) dev_qset:
		dev_qset#3 dev_qset#4
		dev_qset#3 dev_qset#7
		dev_qset#5 dev_qset#7
	723(1) - 723(1) dev_qset:
		dev_qset#3 dev_qset#5
		dev_qset#3 dev_qset#8
		dev_qset#5 dev_qset#8
	723(1) - 748(1) dev_qset:
		dev_qset#3 dev_qset#6
	723(1) - 781(1) dev_qset:
		dev_qset#3 dev_qset#9
		dev_qset#5 dev_qset#9
	748(1) - 723(1) dev_qset:
		dev_qset#6 dev_qset#8
	722(1) - 722(1) dev_quantum:
		dev_quantum#2 dev_quantum#3
		dev_quantum#2 dev_quantum#5
		dev_quantum#3 dev_quantum#5
	722(1) - 748(1) dev_quantum:
		dev_quantum#2 dev_quantum#4
	722(1) - 781(1) dev_quantum:
		dev_quantum#2 dev_quantum#6
		dev_quantum#3 dev_quantum#6
	748(1) - 722(1) dev_quantum:
		dev_quantum#4 dev_quantum#5
	721(1) - 721(1) dev_size:
		dev_size#2 dev_size#3
		dev_size#2 dev_size#7
		dev_size#3 dev_size#7
	721(1) - 755(1) dev_size:
		dev_size#2 dev_size#4
	721(1) - 757(1) dev_size:
		dev_size#2 dev_size#5
	721(1) - 758(1) dev_size:
		dev_size#2 dev_size#6
	721(1) - 802(1) dev_size:
		dev_size#2 dev_size#8
		dev_size#3 dev_size#8
	721(1) - 803(1) dev_size:
		dev_size#2 dev_size#9
		dev_size#3 dev_size#9
	755(1) - 721(1) dev_size:
		dev_size#4 dev_size#7
	755(1) - 803(1) dev_size:
		dev_size#4 dev_size#9
	757(1) - 721(1) dev_size:
		dev_size#5 dev_size#7
	757(1) - 803(1) dev_size:
		dev_size#5 dev_size#9
	758(1) - 721(1) dev_size:
		dev_size#6 dev_size#7
	758(1) - 803(1) dev_size:
		dev_size#6 dev_size#9
Runtime Symex: 0.801787s
Adding SC constraints
Shared __CPROVER_threads_exited: 6R/4W
Shared __CPROVER_next_thread_id: 5R/4W
Shared i: 6R/1W
Shared lock: 9R/11W
Shared scull_quantum: 3R/1W
Shared scull_qset: 3R/1W
Shared dev_data: 5R/4W
Shared dev_quantum: 2R/4W
Shared dev_qset: 5R/4W
Shared dev_size: 4R/5W
Shared __X__: 4R/5W
Shared main::1::t1!0@1: 2R/2W
Shared main::1::t2!0@1: 2R/2W
Shared main::1::t3!0@1: 2R/2W
size of program expression: 1076 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.00686281s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0168683s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.00221237s
Solving with Deagle's Closure solver
26934 variables, 100290 clauses
ClosureSolver finishes with 34 conflicts, 6110 decisions, and 55532 propagations. 194 theory propagations and 11 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0111357s
Runtime decision procedure: 0.0421681s
Running propositional reduction
Solving with Deagle's Closure solver
26934 variables, 96031 clauses
ClosureSolver finishes with 34 conflicts, 10091 decisions, and 80276 propagations. 194 theory propagations and 11 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00234167s
Runtime decision procedure: 0.00238521s
Running propositional reduction
Solving with Deagle's Closure solver
26934 variables, 96032 clauses
ClosureSolver finishes with 34 conflicts, 13997 decisions, and 105020 propagations. 194 theory propagations and 11 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00238184s
Runtime decision procedure: 0.00240445s
Running propositional reduction
Solving with Deagle's Closure solver
26934 variables, 96033 clauses
ClosureSolver finishes with 104 conflicts, 22218 decisions, and 416221 propagations. 299 theory propagations and 13 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0224205s
Runtime decision procedure: 0.0224537s
Running propositional reduction
Solving with Deagle's Closure solver
26934 variables, 96034 clauses
ClosureSolver finishes with 105 conflicts, 25991 decisions, and 452919 propagations. 314 theory propagations and 13 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00443834s
Runtime decision procedure: 0.00446422s
Running propositional reduction
Solving with Deagle's Closure solver
26934 variables, 94756 clauses
ClosureSolver finishes with 105 conflicts, 29470 decisions, and 477555 propagations. 327 theory propagations and 13 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00303848s
Runtime decision procedure: 0.00306126s
Running propositional reduction
Solving with Deagle's Closure solver
26934 variables, 94757 clauses
ClosureSolver finishes with 135 conflicts, 31290 decisions, and 508064 propagations. 483 theory propagations and 16 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.00420895s
Runtime decision procedure: 0.00422244s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i function main
[nodatarace.assertion.0] line 931 No data races on variable dev_data between line 724 and line 724: FAILURE
[nodatarace.assertion.1] line 931 No data races on variable dev_data between line 724 and line 765: FAILURE
[nodatarace.assertion.2] line 931 No data races on variable dev_data between line 724 and line 796: FAILURE
[nodatarace.assertion.3] line 931 No data races on variable dev_data between line 765 and line 724: SUCCESS
[nodatarace.assertion.4] line 931 No data races on variable dev_qset between line 720 and line 723: FAILURE
[nodatarace.assertion.5] line 931 No data races on variable dev_qset between line 723 and line 720: FAILURE
[nodatarace.assertion.6] line 931 No data races on variable dev_qset between line 723 and line 723: FAILURE
[nodatarace.assertion.7] line 931 No data races on variable dev_qset between line 723 and line 748: FAILURE
[nodatarace.assertion.8] line 931 No data races on variable dev_qset between line 723 and line 781: FAILURE
[nodatarace.assertion.9] line 931 No data races on variable dev_qset between line 748 and line 723: FAILURE
[nodatarace.assertion.10] line 931 No data races on variable dev_quantum between line 722 and line 722: FAILURE
[nodatarace.assertion.11] line 931 No data races on variable dev_quantum between line 722 and line 748: FAILURE
[nodatarace.assertion.12] line 931 No data races on variable dev_quantum between line 722 and line 781: FAILURE
[nodatarace.assertion.13] line 931 No data races on variable dev_quantum between line 748 and line 722: FAILURE
[nodatarace.assertion.14] line 931 No data races on variable dev_size between line 721 and line 721: FAILURE
[nodatarace.assertion.15] line 931 No data races on variable dev_size between line 721 and line 755: FAILURE
[nodatarace.assertion.16] line 931 No data races on variable dev_size between line 721 and line 757: FAILURE
[nodatarace.assertion.17] line 931 No data races on variable dev_size between line 721 and line 758: FAILURE
[nodatarace.assertion.18] line 931 No data races on variable dev_size between line 721 and line 802: FAILURE
[nodatarace.assertion.19] line 931 No data races on variable dev_size between line 721 and line 803: FAILURE
[nodatarace.assertion.20] line 931 No data races on variable dev_size between line 755 and line 721: SUCCESS
[nodatarace.assertion.21] line 931 No data races on variable dev_size between line 755 and line 803: SUCCESS
[nodatarace.assertion.22] line 931 No data races on variable dev_size between line 757 and line 721: SUCCESS
[nodatarace.assertion.23] line 931 No data races on variable dev_size between line 757 and line 803: SUCCESS
[nodatarace.assertion.24] line 931 No data races on variable dev_size between line 758 and line 721: SUCCESS
[nodatarace.assertion.25] line 931 No data races on variable dev_size between line 758 and line 803: SUCCESS

** 19 of 26 failed (7 iterations)
VERIFICATION FAILED
