Skip to content
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

Allow C macros in CN specs #76

Open
thatplguy opened this issue May 8, 2024 · 1 comment
Open

Allow C macros in CN specs #76

thatplguy opened this issue May 8, 2024 · 1 comment
Labels
CN Issues related to the CN tool

Comments

@thatplguy
Copy link
Collaborator

The C preprocessor doesn't expand macros in comments, which means CN specs (in comments) can't use C macros. It would be nice to make this possible, although there are challenges; see rems-project/cerberus#230 (comment).

@thatplguy thatplguy added the CN Issues related to the CN tool label May 8, 2024
@peterohanley
Copy link
Collaborator

This would also help with macros that replace a symbol, like here: https://github.com/GaloisInc/VERSE-OpenSUT/blob/8e0db300668301b92578f19f559ce09eae714426/components/mission_protection_system/src/variants/instrumentation_handwritten_C.c#L4

We need to refer to it here: https://github.com/GaloisInc/VERSE-OpenSUT/blob/8e0db300668301b92578f19f559ce09eae714426/components/mission_protection_system/src/include/instrumentation.h#L114 but we can't because we can't access the name. Frama-C doesn't mention the name for specs on declarations so it doesn't have this problem.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CN Issues related to the CN tool
Projects
None yet
Development

No branches or pull requests

2 participants