Explicit null-pointer access in memsafety-ext/tree_dsw_true-valid-memsafety.c

[sosy-lab]

Explicit null-pointer access in memsafety-ext/tree_dsw_true-valid-memsafety.c

[mchalupa]

IMO this is OK as long as the (pred != root) condition is unsatisfiable, that is, if that statement can not be executed. If it is the case, then there's no undefined null-pointer access, right?

[tautschnig]

@leostrakosch Do you have a counterexample that would cause pred != root? If so, the benchmark should be renamed to false-valid-memsafety. If there is no such counterexample, the issue should be closed.

[PhilippWendler]

I think this was submitted by @ondrik, maybe he knows something?

[martinhruska]

This is the @ondrik 's way how to express "assertion(pred == root)". Since the assertion should hold the NULL dereference will actually never happen.

[PhilippWendler]

Thanks for the explanation. Another false positive of https://runtimeverification.com/blog/?p=200