Added expected verification results for LLBMC benchmark suite

pkgs/llbmc-bench/cprover/expected_results

@@ -0,0 +1,175 @@
+anonymous/bubbleSort:valid
+anonymous/intSqRoot:valid
+anonymous/selectSort:unknown
+anonymous/simpleWhile:valid
+eureka/Prim_4:valid
+eureka/Prim_5:valid
+eureka/Prim_6:valid
+eureka/Prim_7:valid
+eureka/Prim_8:valid
+eureka/array_init:valid
+eureka/array_init_assign:valid
+eureka/bf10:valid
+eureka/bf11:valid
+eureka/bf12:valid
+eureka/bf13:valid
+eureka/bf14:valid
+eureka/bf15:valid
+eureka/bf16:valid
+eureka/bf17:valid
+eureka/bf18:valid
+eureka/bf19:valid
+eureka/bf20:valid
+eureka/bf5:valid
+eureka/bf6:valid
+eureka/bf7:valid
+eureka/bf8:valid
+eureka/bf9:valid
+eureka/bubblesort:invalid
+eureka/bubblesort_inner_loop:invalid
+eureka/complex_guard:valid
+eureka/loop_on_input:invalid
+eureka/sequential_swap:valid
+eureka/simple_array_inversion:valid
+eureka/simple_control_on_input:invalid
+eureka/simple_swap_call:valid
+eureka/wrong_loop:invalid
+necla/ex10:invalid
+necla/ex11:valid
+necla/ex12:invalid
+necla/ex13:invalid
+necla/ex14:valid
+necla/ex15:valid
+necla/ex16:valid
+necla/ex17:valid
+necla/ex18:valid
+necla/ex19:invalid
+necla/ex1:valid
+necla/ex20:invalid
+necla/ex21:valid
+necla/ex22:valid
+necla/ex23:valid
+necla/ex26:invalid
+necla/ex27:invalid
+necla/ex29:valid
+necla/ex2:unknown
+necla/ex30:unknown
+necla/ex31:valid
+necla/ex32:valid
+necla/ex33:unknown
+necla/ex34:valid
+necla/ex36_free:unknown
+necla/ex36_read:unknown
+necla/ex37:valid
+necla/ex3:invalid
+necla/ex40:invalid
+necla/ex43:invalid
+necla/ex46:invalid
+necla/ex47:invalid
+necla/ex49:valid
+necla/ex4:invalid
+necla/ex5:valid
+necla/ex6:valid
+necla/ex7:unknown
+necla/ex8:unknown
+necla/ex9:valid
+necla/inf1:invalid
+necla/inf3:valid
+necla/inf4:invalid
+necla/inf5:invalid
+necla/inf6:valid
+necla/inf8:valid
+queue/queue_1000:unknown
+queue/queue_100:valid
+queue/queue_10:valid
+queue/queue_1:valid
+slayer/ex1:invalid
+slayer/ex2:valid
+slayer/ex3:invalid
+slayer/ex5:valid
+slayer/ex6:invalid
+slayer/ex7:valid
+slayer/ex8:valid
+slayer/ex9:valid
+smack/array1:valid
+smack/array2:valid
+smack/array3:valid
+smack/array4:valid
+smack/array:valid
+smack/array_free1:valid
+smack/array_free2:valid
+smack/array_free:valid
+smack/ase_example:valid
+smack/dsa_test10:valid
+smack/dsa_test11:valid
+smack/dsa_test12:valid
+smack/dsa_test13:valid
+smack/dsa_test14:valid
+smack/dsa_test15:valid
+smack/dsa_test1:valid
+smack/dsa_test2:valid
+smack/dsa_test3:valid
+smack/dsa_test4:valid
+smack/dsa_test5:valid
+smack/dsa_test6:valid
+smack/dsa_test7:valid
+smack/dsa_test8:valid
+smack/dsa_test9:valid
+smack/dsa_test:valid
+smack/simple:valid
+smack/simple_double_free:invalid
+smack/simple_fail:invalid
+smack/simple_pre1:valid
+smack/simple_pre2:valid
+smack/simple_pre3:valid
+smack/simple_pre:valid
+smack/two_arrays1:valid
+smack/two_arrays2:valid
+smack/two_arrays6:valid
+smack/two_arrays:valid
+smack/vmcai_bytes:valid
+smack/vmcai_struct:valid
+snu/bs:valid
+snu/crc:valid
+snu/fibcall:valid
+snu/insertsort:valid
+snu/jfdctint:invalid
+snu/matmul:invalid
+urbiva/bitcount16:invalid
+urbiva/bitcount32:invalid
+urbiva/fermat:invalid
+urbiva/graycode:invalid
+urbiva/magic:invalid
+urbiva/matrixsqrt:invalid
+urbiva/queens:invalid
+urbiva/send-more-money:invalid
+urbiva/sort:invalid
+urbiva/sudoku:invalid
+wcet/adpcm:invalid
+wcet/bs:valid
+wcet/bsort100:valid
+wcet/cnt:invalid
+wcet/compress:invalid
+wcet/cover:valid
+wcet/crc:valid
+wcet/duff:valid
+wcet/edn:invalid
+wcet/expint:valid
+wcet/fac:valid
+wcet/fdct:valid
+wcet/fibcall:valid
+wcet/fir:unknown
+wcet/insertsort:valid
+wcet/janne_complex:valid
+wcet/jfdctint:invalid
+wcet/loop3:valid
+wcet/matmult:unknown
+wcet/minmax:valid
+wcet/ndes:valid
+wcet/ns:valid
+wcet/nsichneu:valid
+wcet/prime:valid
+wcet/recursion:valid
+wcet/select:invalid
+wcet/statemate:valid
+wcet/ud:valid

pkgs/llbmc-bench/cprover/rules

@@ -306,9 +306,12 @@ results.$(CONFIG)/%vr: build/%$(SUFFIX)
 	tool="$(TOOL)" ; if [ "x$$tool" = "x" ] ; then tool="$(basename $(CONFIG))" ; fi ; \
 	timeout="$(TIMEOUT)" ; if [ "x$$timeout" != "x" ] ; then timeout="--timeout $(TIMEOUT)" ; fi ; \
 	maxmem="$(MAXMEM)" ; if [ "x$$maxmem" != "x" ] ; then maxmem="--maxmem $(MAXMEM)" ; fi ; \
+	bm="`echo $@ | sed 's#^results.$(CONFIG)/##' | sed 's/.vr$$//'`" ; \
+	st="`grep "^$$bm:" cprover/expected_results | cut -f2 -d:`" ; \
+	if [ "x$$st" = "x" ] ; then st="unknown" ; fi ; \
 	cd $(dir $@) ; \
 	export GMON_OUT_PREFIX=$(basename $(notdir $@)).gmon.out ; \
-	cpbm run $$timeout $$maxmem --cmd $$tool $(realpath $<) -- $(TOOL_OPTS) | tee $(abspath $@) ; \
+	cpbm run $$timeout $$maxmem --$$st --cmd $$tool $(realpath $<) -- $(TOOL_OPTS) | tee $(abspath $@) ; \
 	exit $${PIPESTATUS[0]}
 	tool="$(TOOL)" ; if [ "x$$tool" = "x" ] ; then tool="$(basename $(CONFIG))" ; fi ; \
 	tdir=$(dir $@) ; tbasename=$(basename $(notdir $@)) ; $(POST_RUN)