Record value of constant expression in C.Scase constructor

The Elab pass checks that the argument of 'case' is a compile-time constant
expression.  This commit records the value of this expression in the
C.Scase AST generated by Elab, so that it can be used for further
diagnostics, i.e. checking (in Elab) for duplicate cases.

Note that C2C ignores the recorded value and recomputes the value of
the expression using Ceval.integer_expr.  This is intentional:
Ceval.integer_expr is more trustworthy, as it is formally verified
against the CompCert C semantics.

1 files changed, 5 insertions, 5 deletions

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 0194a893..b8a4ebf6 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2585,13 +2585,13 @@ let rec elab_stmt env ctx s =
       if not ctx.ctx_in_switch then
         error loc "'case' statement not in switch statement";
       let a',env = elab_expr ctx.ctx_vararg loc env a in
-      begin match Ceval.integer_expr env a' with
+      let n =
+        match Ceval.integer_expr env a' with
         | None ->
-            error loc "expression of 'case' label is not an integer constant expression"
-        | Some n -> ()
-      end;
+            error loc "expression of 'case' label is not an integer constant expression"; 0L
+        | Some n -> n in
       let s1,env = elab_stmt env ctx s1 in
-      { sdesc = Slabeled(Scase a', s1); sloc = elab_loc loc },env
+      { sdesc = Slabeled(Scase(a', n), s1); sloc = elab_loc loc },env
 
   | DEFAULT(s1, loc) ->
       if not ctx.ctx_in_switch then