-
Notifications
You must be signed in to change notification settings - Fork 226
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Bit-field initialization via interpreter still has problems #499
Comments
You're right, there has been a regression since #22. Recently, a formal semantics was added for bit fields, and most of the compilation of bit field accesses was moved from the unverified part of CompCert (written in OCaml) to the formally-verified part (written and proved in Coq). That's a good thing, as it improves confidence in the compilation of bit fields, and also enables full conformance with the bit field layout specified in the ELF ABIs. However, in the formally-verified part of CompCert, there are no initializers like |
When I use
ccomp -interp
, i encounter a UB problem about bitfield. I also notice #22, it should be fixed, but not.$ccomp --version The CompCert C verified compiler, version 3.11
The text was updated successfully, but these errors were encountered: