Earlier, more comprehensive check for constant initializers (#88)

This commit checks *during elaboration* that initializers for global
variables or local static variables are compile-time constants.

Before this commit, some non-constant initializers were detected
later in the C2C pass, but others were eliminated by the Cleanup
pass before being checked, and yet others could cause the Rename pass
to abort.

To determine which variables are constant l-values, we leverage
the recent addition of the Storage_auto storage class and base
the determination on the storage class of the identifier:
'auto' or 'register' is not constant, the others are constant.

1 files changed, 6 insertions, 3 deletions

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 55764c3c..dddbd03b 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2236,9 +2236,6 @@ let enter_decdefs local loc env sto dl =
       fatal_error loc "'%s' has incomplete type" s;
     (* process the initializer *)
     let (ty', init') = elab_initializer loc env1 s ty init in
-    (* if (sto = Storage_static || not local) then
-     *   (\* Check for constant initializer for static and global variables *\)
-     *   is_constant_init env loc init'; *)
     (* update environment with refined type *)
     let env2 = Env.add_ident env1 id sto' ty' in
     (* check for incomplete type *)
@@ -2252,6 +2249,12 @@ let enter_decdefs local loc env sto dl =
     else begin
       (* Global definition *)
       emit_elab ~linkage env2 loc (Gdecl(sto', id, ty', init'));
+      (* Make sure the initializer is constant. *)
+      begin match init' with
+      | Some i when not (Ceval.is_constant_init env2 i) ->
+          error loc "initializer is not a compile-time constant"
+      | _ -> ()
+      end;
       (decls, env2)
     end in
   let (decls, env') = List.fold_left enter_decdef ([], env) dl in