Define macros with CompCert's version number (#284)

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 ,
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: #282 

1 files changed, 24 insertions, 2 deletions

diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 88b47854..929d9fd7 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -11,21 +11,43 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+open Printf
 open Clflags
 open Commandline
 open Driveraux
 
 (* Common frontend functions between clightgen and ccomp *)
 
+(* Split the version number into major.minor *)
+
+let re_version = Str.regexp {|\([0-9]+\)\.\([0-9]+\)|}
+
+let (v_major, v_minor) =
+  let get n = int_of_string (Str.matched_group n Version.version) in
+  assert (Str.string_match re_version Version.version 0);
+  (get 1, get 2)
+
+let v_number =
+  assert (v_minor < 100);
+  100 * v_major + v_minor
+
+(* Predefined macros: version numbers, C11 features *)
+
 let predefined_macros =
-  [
+  let macros = [  
     "-D__COMPCERT__";
+    sprintf "-D__COMPCERT_MAJOR__=%d" v_major;    
+    sprintf "-D__COMPCERT_MINOR__=%d" v_minor;    
+    sprintf "-D__COMPCERT_VERSION__=%d" v_number;    
     "-U__STDC_IEC_559_COMPLEX__";
     "-D__STDC_NO_ATOMICS__";
     "-D__STDC_NO_COMPLEX__";
     "-D__STDC_NO_THREADS__";
     "-D__STDC_NO_VLA__"
-  ]
+  ] in
+  if Version.buildnr = ""
+  then macros
+  else sprintf "-D__COMPCERT_BUILDNR__=%s" Version.buildnr :: macros
 
 (* From C to preprocessed C *)