Marek Chalupa

Actually, the only benchmarks from _Memsafety_ that have undefined functions are the ntdrivers one. The rest of the benchmarks are from _SoftwareSystems_ category. For busybox, we already have this issue:...

Here are witnesses for memsafety violation for 181 of these benchmarks that I was able to confirm with CPAchecker: https://www.fi.muni.cz/~xchalup4/sv-comp/1270_witnesses_memsafety/

> If their precise semantics is not important for the safety of the benchmark That is the problem - when we treat the undefined functions as returning non-deterministic value (which...

Ignore was not the right word - we put there some concrete value (like 0). Since the benchmark should not depend on the returned value of undefined function, the value...

I agree that verifiers should be able to handle such function, but we should state it somewhere (or is it somewhere and I missed it?). However, in some benchmarks there...

I don't know if in all these benchmarks modified in #556 the `input_allocate_device` was problematic, but at least in the five mentioned above, it was.

@mutilin : Yes, that is what am I reporting -- an invalid access to memory.

>> That's me making use of undefined behaviour without even resorting to memory errors. > So use this, but do not refer to memory errors! Memory errors are undefined behavior......

> I do not see such requirement in the rules. Yes, my bad, I formulated it incorrectly, what I said holds only for MemSafety category. The rest of the sentence,...

Anyway, I think that the conversation is starting diverging from the original topic, which is that the reported benchmarks contain invalid memory accesses (whatever it means for the unreach-call label).