Pass type of controlling switch expression into ctx.

The standard requires that the constant expression of a case needs to be
converted to the integer promoted type of the controlling expression
(§6.8.4.2p5).

To enforce this we pass the ineger promoted type of the controlling
expression in ctx  and add a cast of the case expression to this type.

If the controlling expression is not an integer type we already have an
error message and skip adding the cast.
Bug 40122

Author: bschommer

cparser/Elab.ml

@@ -1767,7 +1767,8 @@ type elab_context = {
   ctx_labels: StringSet.t;      (**r all labels defined in the function *)
   ctx_break: bool;              (**r is 'break' allowed? *)
   ctx_continue: bool;           (**r is 'continue' allowed? *)
-  ctx_in_switch: bool;          (**r are 'case' and 'default' allowed? *)
+  ctx_in_switch: typ option;    (**r type of the controlling switch expression
+                                     or [None] outside of switch *)
   ctx_vararg: bool;             (**r is this a vararg function? *)
   ctx_nonstatic_inline: bool    (**r is this a nonstatic inline function? *)
 }
@@ -1777,7 +1778,7 @@ type elab_context = {
 let ctx_constexp = {
   ctx_return_typ = TVoid [];
   ctx_labels = StringSet.empty;
-  ctx_break = false; ctx_continue = false; ctx_in_switch = false;
+  ctx_break = false; ctx_continue = false; ctx_in_switch = None;
   ctx_vararg = false; ctx_nonstatic_inline = false
 }
 
@@ -3063,7 +3064,7 @@ let stmt_labels stmt =
 
 let ctx_loop ctx = { ctx with ctx_break = true; ctx_continue = true }
 
-let ctx_switch ctx = { ctx with ctx_break = true; ctx_in_switch = true }
+let ctx_switch ctx ty = { ctx with ctx_break = true; ctx_in_switch = Some ty }
 
 (* Check the uniqueness of 'case' and 'default' in a 'switch' *)
 
@@ -3125,9 +3126,11 @@ let rec elab_stmt env ctx s =
       { sdesc = Slabeled(Slabel lbl, s1); sloc = elab_loc loc },env
 
   | CASE(a, s1, loc) ->
-      if not ctx.ctx_in_switch then
-        error loc "'case' statement not in switch statement";
       let a',env = elab_expr ctx loc env a in
+      let a' = match ctx.ctx_in_switch with
+        | None -> error loc "'case' statement not in switch statement"; a'
+        | Some ((TInt _) as ty) -> ecast ty a'
+        | _ -> a' in
       let n =
         match Ceval.integer_expr env a' with
         | None ->
@@ -3137,7 +3140,8 @@ let rec elab_stmt env ctx s =
       { sdesc = Slabeled(Scase(a', n), s1); sloc = elab_loc loc },env
 
   | DEFAULT(s1, loc) ->
-      if not ctx.ctx_in_switch then
+      (*- #Link_to E_COMPCERT_TR_Robustness_ELAB_141 *)
+      if ctx.ctx_in_switch = None then
         error loc "'case' statement not in switch statement";
       let s1,env = elab_stmt env ctx s1 in
       { sdesc = Slabeled(Sdefault, s1); sloc = elab_loc loc },env
@@ -3217,7 +3221,7 @@ let rec elab_stmt env ctx s =
       if not (is_integer_type env' a'.etyp) then
         error loc "controlling expression of 'switch' does not have integer type (%a invalid)"
           (print_typ env') a'.etyp;
-      let s1' = elab_stmt_new_scope env' (ctx_switch ctx) s1 in
+      let s1' = elab_stmt_new_scope env' (ctx_switch ctx (unary_conversion env a'.etyp)) s1 in
       check_switch_cases s1';
       { sdesc = Sswitch(a', s1'); sloc = elab_loc loc },env
 
@@ -3326,7 +3330,7 @@ let elab_funbody return_typ vararg nonstatic_inline env b =
       ctx_labels = stmt_labels b;
       ctx_break = false;
       ctx_continue = false;
-      ctx_in_switch = false;
+      ctx_in_switch = None;
       ctx_vararg = vararg;
       ctx_nonstatic_inline = nonstatic_inline } in
   (* The function body appears as a block in the AST but should not create