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

Provide version information in in preprocessor #282

Closed
nemequ opened this issue Mar 23, 2019 · 2 comments
Closed

Provide version information in in preprocessor #282

nemequ opened this issue Mar 23, 2019 · 2 comments

Comments

@nemequ
Copy link

nemequ commented Mar 23, 2019

I'd like to add support for CompCert to Hedley, but AFAICT there is no way to tell from the preprocessor which version of CompCert is in use, so there is no way to tell when certain features can be enabled.

For example, it looks like noinline was added with version 3.2, so if I'd like to be able to do something like

#if defined(__COMPCERT__) && (__COMPCERT__ >= 30200)
#  define HEDLEY_NO_INLINE __attribute((noinline))
#else
#  define HEDLEY_NO_INLINE
#endif

It looks like this would basically just require something like

diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 88b47854..30d78592 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -19,7 +19,7 @@ open Driveraux
 
 let predefined_macros =
   [
-    "-D__COMPCERT__";
+    "-D__COMPCERT__=30500";
     "-U__STDC_IEC_559_COMPLEX__";
     "-D__STDC_NO_ATOMICS__";
     "-D__STDC_NO_COMPLEX__";

But obviously the version number shouldn't be hard-coded, and I'm not sure where to get it.

@xavierleroy
Copy link
Contributor

I agree this would be nice. Thanks for the suggestion, I'll look into it.

xavierleroy added a commit that referenced this issue Mar 25, 2019
As suggested in #282, it can be useful to #ifdef code depending on
specific versions of CompCert.

Assuming a version number of the form MM.mm or MM.mm.pp
the following macros are predefined:

__COMPCERT_MAJOR__=MM       (the major version number)
__COMPCERT_MAJOR__=mm       (the minor version number)
__COMPCERT_PATCHLEVEL__=pp  (the patchlevel, or 0 if none)
__COMPCERT_VERSION__=MMmmpp (two decimal digits each, e.g. 30500 for version 3.5)
@xavierleroy
Copy link
Contributor

A proposed implementation: #284.

tbrk pushed a commit to inria-parkas/CompCert that referenced this issue May 21, 2019
As suggested in AbsInt#282, it can be useful to #ifdef code depending on
specific versions of CompCert.

Assuming a version number of the form MM.mm ,
the following macros are predefined:

__COMPCERT_MAJOR__=MM       (the major version number)
__COMPCERT_MINOR__=mm       (the minor version number)
__COMPCERT_VERSION__=MMmm (two decimal digits for the minor, e.g. 305 for version 3.5)

We also define __COMPCERT_BUILDNR__ if the build number is not empty in file ./VERSION.

Closes: AbsInt#282
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants