Potential issue with munmap model in busy box

[zvonimir]

Here is the current model:

int munmap(void *addr, size_t length)
{
  if(__VERIFIER_nondet_int())
    return -1;
  (void)length;
  free(addr);
  return 0;
}

It might nondeterministally not free memory, which causes memory leaks in at least cat_true-no-overflow_true-valid-memsafety.i. Now, if the model is correct, than cat_true-no-overflow_true-valid-memsafety.i should be relabeled since it contains a memory leak.

[zvonimir]

What do you think @tautschnig?

[tautschnig]

You are of course right that this approach has introduced possible memory leaks. Would you suggest to make the munmap model less general, or should we rather relabel the benchmark?

[zvonimir]

Given that the deadline has passed, I am of the opinion that all benchmarks with open issues should be moved into the todo folder and discussed after the competition. Otherwise, after reading the specification for munmap, your model makes sense to me, and I think that this benchmarks should be relabeled.

[ondrik]

Hi @zvonimir , could you please identify all falsely labeled benchmarks due to the munmap model in /c/busybox-1.22.0-todo so that they can be returned to the competition?