Michael Tautschnig

This benchmark is almost the same as c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.c, if it weren't for the declaration of "i" as `unsigned`. Both of which exist in verisec (cf. https://github.com/cirosantilli/frama-c/tree/439bddd91e0686429a585ec3ae28200b60a31e8b/tests/verisec/suite/programs/apps/sendmail/CVE-2001-0653/tTflag). As it is, it...

@kfriedberger I'm not as surprised that you are finding counterexamples to be short - the issues will really just be a lack of necessary initialisation, often resulting in an invalid...

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...

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

We could generalise memory leaks to "resource leaks", which is a class of practically relevant problems. (And then, finally, the Infer team might want to join.)

Are we on a path to ending the never-ending category debate?

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?

@mutilin Why can't we use __VERIFIER_nondet_* in place of those functions? We have been fighting over various undefined behaviours in numerous benchmarks, so we should really not have any such...

It might be good to at least capture the assumption "invoking a function where no definition is provided yields a non-deterministic value, but does not cause any other side effects."...

At a much larger scale, Linux distributions have solved these problems properly, so it's not that rocket science would be required. I had myself made attempts in the benchmarking toolkit...