diff --git a/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.c b/c/ldv-linux-4.2-rc1/todo/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.c similarity index 99% rename from c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.c rename to c/ldv-linux-4.2-rc1/todo/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.c index e1e993b03fa..7a4b69a8dc1 100644 --- a/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.c +++ b/c/ldv-linux-4.2-rc1/todo/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.c @@ -1,3 +1,5 @@ +// lacks proper initialization (see https://github.com/sosy-lab/sv-benchmarks/issues/1207) + extern void abort(void); #include void reach_error() { assert(0); } diff --git a/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.i b/c/ldv-linux-4.2-rc1/todo/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.i similarity index 100% rename from c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.i rename to c/ldv-linux-4.2-rc1/todo/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.i diff --git a/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.yml b/c/ldv-linux-4.2-rc1/todo/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.yml similarity index 72% rename from c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.yml rename to c/ldv-linux-4.2-rc1/todo/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.yml index f6595258801..48014eb1da3 100644 --- a/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.yml +++ b/c/ldv-linux-4.2-rc1/todo/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.yml @@ -5,7 +5,7 @@ input_files: 'linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-e properties: - property_file: ../properties/unreach-call.prp - expected_verdict: false + expected_verdict: false # currently true, lacks proper initialization (see https://github.com/sosy-lab/sv-benchmarks/issues/1207) options: language: C