Skip to content

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Sep 8, 2025

This fixes a regression from #193 after which Goblint started erroring on 32-bit SV-COMP tasks with

[Error][Unsound] Machine definition not available for selected architecture

The problem is that _Float16 is available on 64-bit, but not 32-bit, so separate headers are needed. Otherwise the compilation of 32-bit machdep generation fails.

The headers should've been separate from the beginning. It's surprising that nothing broke before.

@sim642 sim642 added this to the 2.0.8 milestone Sep 8, 2025
@sim642 sim642 added the bug label Sep 8, 2025
@sim642
Copy link
Member Author

sim642 commented Sep 8, 2025

Ugh, it now correctly creates both machdeps again on my machine where I also have 32-bit available, but fails when one doesn't.

@sim642 sim642 merged commit e5b6287 into develop Sep 8, 2025
28 checks passed
@sim642 sim642 deleted the machdep-header branch September 8, 2025 09:56
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 9, 2025
CHANGES:

* Fix 32bit `Machdep` generation on 64bit host (goblint/cil#195).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant