Philipp Wendler

What do you mean by "just ignore them"? What is the difference to assuming a nondet return value?

Replacing lots of functions in benchmarks would be a considerable effort when preparing benchmarks. @mutilin and this colleagues would like to have verifiers that they can apply to Linux kernel...

Documenting this is always good. For witness validation, I would not expect many problems. These are `unreach-call` benchmarks, so verifiers should ignore all memsafety problems and just continue (and for...

No, I meant unsigned overflows.

Adding these files to another category is easy, but to remove them from the current category without removing them from the current directory is not so easy. How about creating...

A case of #480.

I agree with @tautschnig. In particular, as far as I understand the C standard, using a char pointer to access individual bytes of some object is legal.

What is the current state of this? @shaobo-he Do you still think that this program has undefined behavior? Can you explain precisely why and where? Otherwise I think this issue...

Do you know a way to determine which files a PR touches? Note that a PR can have an arbitrarily long list of commits.

I think this can be closed.