search

runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
36 stars 23 forks source link

Fix tautological comparison error #1116

Closed Baltoli closed 3 months ago

Baltoli commented 3 months ago

Using -1 as the sentinel "not present" value for these weak symbols of type char is not correct, as the standard makes no guarantee whether char is signed or not; it is therefore possible for an implementation to supply us with a type such that comparing the sentinels with -1 later is tautologically false.

Baltoli commented 3 months ago

cc @0cjs @stevenmeker

0cjs commented 3 months ago

This is a fix for #1115, right?

Baltoli commented 3 months ago

Yep, I believe it morally should be, though I'm still not sure how to reproduce the configuration that causes the error.

0cjs commented 3 months ago

...though I'm still not sure how to reproduce the configuration that causes the error.

Ah, my bad! I should have given you that info in the issue. We reproduced it only on Debian 12 running on aarch64 (a Docker container hosted on an Apple Silicon Mac). This should have been the standard clang package from Debian, as I don't see any way another clang could have snuck in there.

We spent quite some time trying to figure out if we could find a compiler warning flag that would warn on systems with signed ints, but couldn't find anything.