Move ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb…

…-core--dvb-core.ko-entry_point.cil.out to TODO directory (issue sosy-lab#1207) Currently expected verdict would be true because the benchmark lacks proper initialization.
sim642 · Nov 17, 2020 · 4b2af53 · 4b2af53
1 parent 2e5e802
commit 4b2af53
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 1 deletion.
diff --git a/...b-core--dvb-core.ko-entry_point.cil.out.c → ...b-core--dvb-core.ko-entry_point.cil.out.c b/...b-core--dvb-core.ko-entry_point.cil.out.c → ...b-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 <assert.h>
 void reach_error() { assert(0); }

diff --git a/...b-core--dvb-core.ko-entry_point.cil.out.i → ...b-core--dvb-core.ko-entry_point.cil.out.i b/...b-core--dvb-core.ko-entry_point.cil.out.i → ...b-core--dvb-core.ko-entry_point.cil.out.i
diff --git a/...core--dvb-core.ko-entry_point.cil.out.yml → ...core--dvb-core.ko-entry_point.cil.out.yml b/...core--dvb-core.ko-entry_point.cil.out.yml → ...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