sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
184 stars 169 forks source link

Do not perform pointer comparison over distinct objects #1284

Closed tautschnig closed 3 years ago

tautschnig commented 3 years ago

Comparing pointers pointing to distinct objects is undefined behaviour. Instead, perform the comparison over integers, which is implementation-defined behaviour.

This fix also contributes to addressing #1266, but several more tasks have this problem. Thus I instead opted to fix it for all of them.

versokova commented 3 years ago

Why not uintptr_t? Probably it will be typedef to unsigned long, but it looks cleaner.

dbeyer commented 3 years ago

I propose to implement the suggested improvement in a new PR, such that we can immediately merge and progress.