[NOT URGENT] mem-cleanup property

[peterschrammel]

There's a new mem-cleanup property (https://sv-comp.sosy-lab.org/2018/rules.php) that needs to be distinguished in the output of the wrapper script: https://github.com/diffblue/cprover-sv-comp/blob/master/tool-wrapper.inc#L33

Example benchmark: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.c

[lucasccordeiro]

@peterschrammel: The description of this property is unclear. What is the difference to memory leak? Is it going to be encoded as an assertion in the program?

If we run CBMC in this example, then we get:

$cbmc merge_sort_false-unreach-call_false-valid-memcleanup.c --unwind 2 --stop-on-fail --memory-leak-check --pointer-check

Violated property:
  file merge_sort_false-unreach-call_false-valid-memcleanup.c line 8 function fail
  assertion
  FALSE

VERIFICATION FAILED

We get a user-specified assertion violation.

[lucasccordeiro]

Here is the discussion of this new property: https://github.com/sosy-lab/sv-benchmarks/issues/471

[lucasccordeiro]

@peterschrammel, @tautschnig, and @marek-trtik: Reading the discussions related to sosy-lab/sv-benchmarks#471, I get the impression that this is not a useful property of the C programming language; this seems to be garbage collection problem. Additionally, I don't think that changing the output of our script is going to solve this issue. I believe this issue requires further implementation in CBMC (or am I wrong?)

[marek-trtik]

I think this property is not used (and perhaps will not be used) in this year competition. There is no .set file for this property. There is only .prp file, but it is not included in any .xml file in https://github.com/sosy-lab/sv-comp Also, I am not aware of any incorrect result from CBMC due to this category.

Therefore I vote for closing this issue.

[lucasccordeiro]

I would also vote to close this issue for now.

[tautschnig]

I'd agree that we should ignore this for SV-COMP'18.