-
Notifications
You must be signed in to change notification settings - Fork 232
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
comments in assembly code cause assembler errors in some versions of MacOS on x86-64 #399
Comments
Thanks for the info. It is strange (bordering on "it is a bug") that clang would preprocess a I couldn't find any documentation on how clang treats assembly source files, however. Do you have any pointers you could share? At any rate, I'm fine with changing the comment syntax on x86_64-macos, but perhaps not (yet) on x86_64-linux. The reason being that one of the two program annotation mechanisms of CompCert produce comments in assembly files that users are supposed to extract with their own tools, so the less we change the syntax of comments the less we break these hypothetical tools. |
Tentative fix in a0ad5ff . Holler if it doesn't work. |
For reference:
If one tries to compile the file:
One gets:
Also reported by another user with configuration:
|
A simple compile of a
|
Some versions of MacOS install a
gcc
command that is actually aliased toclang
. Some versions of that command run the C preprocessor on.s
files, whereasgcc
runs it only on.S
files. This causes some mysterious errors when assembling these files when CompCert prints comment lines, which start with#
, when these lines are identified as C preprocessor directives, which happens for instance if the comment line is of the form# if (blabla)
.Fix: use
##
as comment prefix.The text was updated successfully, but these errors were encountered: