Tasks with expected undefined behavior and another result in several directories

[PhilippWendler]

The following tasks all have expected undefined behavior (as indicated by false-valid-deref or false-no-overflow), but also a result for some other property:

sv-benchmarks/c/check.py

Lines 93 to 115 in 50702f8

	("busybox-1.22.0/basename_false-unreach-call_true-no-overflow_false-valid-deref.c", "has expected undefined behavior but also a verdict for some other property"),
	("busybox-1.22.0/basename_false-unreach-call_true-no-overflow_false-valid-deref.i", "has expected undefined behavior but also a verdict for some other property"),
	("busybox-1.22.0/head_true-no-overflow_false-valid-deref.c", "has expected undefined behavior but also a verdict for some other property"),
	("busybox-1.22.0/head_true-no-overflow_false-valid-deref.i", "has expected undefined behavior but also a verdict for some other property"),
	("busybox-1.22.0/sleep_true-no-overflow_false-valid-deref.c", "has expected undefined behavior but also a verdict for some other property"),
	("busybox-1.22.0/sleep_true-no-overflow_false-valid-deref.i", "has expected undefined behavior but also a verdict for some other property"),
	("forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.c", "has expected undefined behavior but also a verdict for some other property"),
	("forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i", "has expected undefined behavior but also a verdict for some other property"),
	("forester-heap/sll-01_false-unreach-call_false-valid-deref.c", "has expected undefined behavior but also a verdict for some other property"),
	("forester-heap/sll-01_false-unreach-call_false-valid-deref.i", "has expected undefined behavior but also a verdict for some other property"),
	("forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.c", "has expected undefined behavior but also a verdict for some other property"),
	("forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i", "has expected undefined behavior but also a verdict for some other property"),
	("heap-manipulation/tree_false-unreach-call_false-valid-deref.c", "has expected undefined behavior but also a verdict for some other property"),
	("heap-manipulation/tree_false-unreach-call_false-valid-deref.i", "has expected undefined behavior but also a verdict for some other property"),
	("list-ext-properties/list-ext_false-unreach-call_false-valid-deref.c", "has expected undefined behavior but also a verdict for some other property"),
	("list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i", "has expected undefined behavior but also a verdict for some other property"),
	("list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.c", "has expected undefined behavior but also a verdict for some other property"),
	("list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i", "has expected undefined behavior but also a verdict for some other property"),
	("termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_false-no-overflow.c", "has expected undefined behavior but also a verdict for some other property"),
	("termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_false-no-overflow.c", "has expected undefined behavior but also a verdict for some other property"),
	("termination-crafted/NonTermination3_false-termination_false-valid-deref.c", "has expected undefined behavior but also a verdict for some other property"),
	("termination-numeric/Binomial_true-termination_false-no-overflow.c", "has expected undefined behavior but also a verdict for some other property"),
	("termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c", "has expected undefined behavior but also a verdict for some other property"),

The affected directories are

• busybox-1.22.0
• forester-heap
• heap-manipulation
• list-ext-properties
• termination-crafted-lit
• termination-numeric

Undefined behavior can in theory lead to the violation of any other property, so this makes little sense.

Probably the task should be split into two versions, one identical to the current version but only with the property for undefined behavior, and the other with the undefined behavior fixed.

[PhilippWendler]

Should these tasks simply be renamed to remove the other verdict? Probably it would be better to fix them, but I can't do this.

[PhilippWendler]

@dbeyer What should be do here? Will you contact the authors of these tasks and ask for fixes, or should we remove the label for the other property (the one that does not include undefined behavior)?

@tautschnig has already fixes for the busybox tasks in #513.

[dbeyer]

Can this issue be closed? @tautschnig ?

[tautschnig]

I'm not sure why it's me to comment on this? I have tried to do my share of the work by addressing the issue for those benchmarks that I had originally submitted. It would be nice if the submitters of benchmarks in forester-heap etc. did the same?

[tautschnig]

Also: no, it cannot be closed AFAIK, because the other directories as listed by @PhilippWendler are still affected.

[dbeyer]

Assigned @Heizmann and @danieldietsch for cleaning up the labels for the termination directories.