owi icon indicating copy to clipboard operation
owi copied to clipboard

concolic failures

Open zapashcanon opened this issue 1 year ago • 8 comments

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/.

zapashcanon avatar Jun 14 '24 22:06 zapashcanon