CIVL=civl
VERIFY=${CIVL} verify -enablePrintf=false
CLOC=cloc --csv --quiet

all: bug4 queue_ok_longest_true-unreach-call read_write_lock_false-unreach-call sync01_true-unreach-call 03_incdec_true-unreach-call

bug4: bug4.c
	@lessecho "NAME: bug4.c"
	@lessecho "CITE: \\cite{LLNL:Pthreads:URL}"	
	@lessecho "TYPE: $$\\text{P}$$"
	@lessecho "SCALE: {\\texttt{NT=3}}"
	@$(CLOC) bug4.c
	${VERIFY} bug4.c

queue_ok_longest_true-unreach-call: queue_ok_longest_true-unreach-call.c
	@lessecho "NAME: queue{\U}ok{\U}longest{\U}...c"
	@lessecho "CITE: \\cite{svcomp:2015} "	
	@lessecho "TYPE: $$\\text{P}$$"
	@lessecho "SCALE: {\\texttt{SIZE=800}}"
	@$(CLOC) queue_ok_longest_true-unreach-call.c
	${VERIFY} -svcomp -inputSIZE=800 -inputEMPTY=-1 -inputFULL=-2 queue_ok_longest_true-unreach-call.c

read_write_lock_false-unreach-call: read_write_lock_false-unreach-call.c
	@lessecho "NAME: read{\U}write{\U}lock{\U}...c"
	@lessecho "CITE: \\cite{svcomp:2015} "	
	@lessecho "TYPE: $$\\text{P}$$"
	@lessecho "SCALE: {\\texttt{NT=4}}"
	@$(CLOC) read_write_lock_false-unreach-call.c
	${VERIFY} -svcomp read_write_lock_false-unreach-call.c

sync01_true-unreach-call: sync01_true-unreach-call.c
	@lessecho "NAME: sync01{\U}true...c"
	@lessecho "CITE: \\cite{svcomp:2015} "	
	@lessecho "TYPE: $$\\text{P}$$"
	@lessecho "SCALE: {\\texttt{NT=2}}"
	@$(CLOC) sync01_true-unreach-call.c
	${VERIFY} -svcomp sync01_true-unreach-call.c

03_incdec_true-unreach-call: 03_incdec_true-unreach-call.c
	@lessecho "NAME: 03{\U}incdec{\U}true...c"
	@lessecho "CITE: \\cite{svcomp:2015} "	
	@lessecho "TYPE: $$\\text{P}$$"
	@lessecho "SCALE: {\\texttt{NT=3}}"
	@$(CLOC) 03_incdec_true-unreach-call.c
	${VERIFY} -svcomp -procBound=3 03_incdec_true-unreach-call.c	

clean: 
	rm -f -r CIVLREP
	rm -f *~
