exp05_conjunct sizes

Experiment: budget=100, timeout=30 running this with batch-size values 1 2 4 ... 32. with random5.txt Expected number of runs in each db: 5 * 100 * 8 = 4000. Strangely, there are only 1604 runs in each, which is really weird.

batch-size	unsound	incomplete	unsound-cbmc-klee	unsound-cmbc-klee-smack
1	81	0	0	0
2	90	0	0	0
4	93	0	0	0
8	93	0	0	0
16	97	0	0	0
32	95	0	0	0

Also, all the unsound cases are due to klee.

So, there must be something wrong here.

There’s a problem with c/locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c, apparently there are only 2 runs on one instrumentation of that file.

I found another reason why vdiff crashes. The glue code for Klee calls clang-3.8 through callCommand which throws an IOException if the called process returns an error code. Apparently the instrumented files from that test case are not type-checking.

Commit 9953d9b74caa8be91c8dfc9f41ec50a1ffba8095 adds an exception handler.

The reason why that file is not accepted is that it uses goto ERROR. The label ERROR is undefined because the instrumentation removes the ERROR label.

TODO: Also replace all goto ERROR statements with an empty statement.