owi
owi copied to clipboard
concolic failures
From the report generated:
run 1151: testcomp/sv-benchmarks/c/seq-pthread/cs_stateful-1.i
run 1150: testcomp/sv-benchmarks/c/seq-pthread/cs_stack-2.i
run 1149: testcomp/sv-benchmarks/c/seq-pthread/cs_read_write_lock-2.i
run 1148: testcomp/sv-benchmarks/c/seq-pthread/cs_queue-2.i
run 1147: testcomp/sv-benchmarks/c/seq-pthread/cs_fib_longer-2.i
run 1146: testcomp/sv-benchmarks/c/seq-pthread/cs_fib-2.i
run 853: testcomp/sv-benchmarks/c/ntdrivers/parport.i.cil-1.c
run 852: testcomp/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c
run 851: testcomp/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c
run 850: testcomp/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c
run 849: testcomp/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c
run 116: testcomp/sv-benchmarks/c/eca-rers2012/Problem18_label00.c
run 115: testcomp/sv-benchmarks/c/eca-rers2012/Problem16_label00.c
run 114: testcomp/sv-benchmarks/c/eca-rers2012/Problem15_label00.c
run 113: testcomp/sv-benchmarks/c/eca-rers2012/Problem12_label00.c
run 112: testcomp/sv-benchmarks/c/eca-rers2012/Problem11_label00.c
run 111: testcomp/sv-benchmarks/c/eca-rers2012/Problem06_label00.c
run 110: testcomp/sv-benchmarks/c/eca-rers2012/Problem05_label00.c
run 107: testcomp/sv-benchmarks/c/busybox-1.22.0/test-1.i
run 106: testcomp/sv-benchmarks/c/busybox-1.22.0/printf-3.i
run 105: testcomp/sv-benchmarks/c/busybox-1.22.0/od-4.i
run 104: testcomp/sv-benchmarks/c/busybox-1.22.0/ls-incomplete-2.i
I had a quick look at the output:
- 104, 849, 850, 851, 852, 853, 1146, 1147, 1148, 1149, 1150, 1151 (error 125)
owi: internal error, uncaught exception: Failure("TODO"), I guess something is missing in the concolic monad ; - 105 (error 26) seems to be the same as #272 ;
- 106, 107 (error 125)
owi: internal error, uncaught exception: Failure("alloc: cannot allocate base pointer [...]here we should probably abort as it's done in the symbolic monad instead of failing... ; - 110, 111, 112, 113, 114, 115, 116 (error 43)
unknown import "summaries" "exit"(maybe we should add a an interface of expected imported functions to make sure we have all of them in both symbolic and concolic mode).
FYI the full results are on the server in owi/bench/results-testcomp-owi_w24_O3_concolic-2024-06-14_15h54m53s/.