You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Running cbmc --big-endian regression/cbmc-shadow-memory/float1/main.c yields VERIFICATION FAILED (and so do several other tests in the cbmc-shadow-memory suite). As far as I can tell, the problem is that compute_max_over_bytes uses byte extract with a value type that isn't even a full byte (it might just be 7 bits). This code should either extract bits (with suitable offset), or extract full bytes and then apply a mask (adjusted for endianness).
CBMC version: cbmc-5.95.1 or later
Operating system: Any big-endian platform, or running cbmc with --big-endian
Exact command line resulting in the issue: See above
What behaviour did you expect: Verification results are independent of endianness.
What happened instead: See above
The text was updated successfully, but these errors were encountered:
Running
cbmc --big-endian regression/cbmc-shadow-memory/float1/main.c
yieldsVERIFICATION FAILED
(and so do several other tests in thecbmc-shadow-memory
suite). As far as I can tell, the problem is thatcompute_max_over_bytes
uses byte extract with a value type that isn't even a full byte (it might just be 7 bits). This code should either extract bits (with suitable offset), or extract full bytes and then apply a mask (adjusted for endianness).CBMC version: cbmc-5.95.1 or later
Operating system: Any big-endian platform, or running
cbmc
with--big-endian
Exact command line resulting in the issue: See above
What behaviour did you expect: Verification results are independent of endianness.
What happened instead: See above
The text was updated successfully, but these errors were encountered: