[printer] ensures labels are not put on declarations

Fixes #617

Technically, the C standard distinguishes between declarations and statements,
and only the latter may have labels attached to them. Thus, printing a label
directly over a `Local_init` will result in ill-formed C code. In order to
avoid that, we add a dummy nop (aka `;`) in-between.

A first version was done in !1518, but failed to take into account
`UnspecifiedSequence` whose first element happens to be a `Local_init` 

src/kernel_services/ast_printing/cil_printer.ml

@@ -418,6 +418,13 @@ let extract_acsl_list t =
 let is_cfg_block =
   function Stmt_block _ -> false | Then_with_else | Other | Body -> true
 
+let rec has_unprotected_local_init s =
+  match s.skind with
+  | Instr (Local_init _) -> true
+  | UnspecifiedSequence((s,_,_,_,_) :: _) -> has_unprotected_local_init s
+  | Block { bscoping = false; bstmts = s :: _ } -> has_unprotected_local_init s
+  | _ -> false
+
 class cil_printer () = object (self)
 
   val mutable logic_printer_enabled = true
@@ -1020,9 +1027,8 @@ class cil_printer () = object (self)
 
   method stmt_labels fmt (s:stmt) =
     let suf =
-      match s.skind with
-      | Instr (Local_init _) -> format_of_string ";@]@ "
-      | _ -> format_of_string "@]@ "
+      if has_unprotected_local_init s then format_of_string ";@]@ "
+      else format_of_string "@]@ "
     in
     if s.labels <> [] then
       Pretty_utils.pp_list

tests/syntax/label_decl.i

@@ -2,8 +2,17 @@
 MACRO: TMP @PTEST_DIR@/result/@PTEST_NAME@.i
 OPT: -print -then -print -ocode @TMP@ -then @TMP@ -print -ocode=""
 */
+struct s { int i; };
+
+void s_cp (struct s *p, struct s v) { *p = v; }
+
 void main(void)
 {
   int i = 0;
   label: if (i);
+
+  struct s y;
+
+  if ((i < 0) || (i >= 256))
+    s_cp(&y, (struct s){1});
 }

tests/syntax/oracle/label_decl.res.oracle

 [kernel] Parsing tests/syntax/label_decl.i (no preprocessing)
 /* Generated by Frama-C */
+struct s {
+   int i ;
+};
+void s_cp(struct s *p, struct s v)
+{
+  *p = v;
+  return;
+}
+
 void main(void)
 {
+  struct s y;
   int i = 0;
   label:; int tmp = i;
+  if (i < 0) goto _LOR;
+  else 
+    if (i >= 256) {
+      _LOR:; struct s __constr_expr_0 = {.i = 1};
+      s_cp(& y,__constr_expr_0);
+    }
   return;
 }
 
 
 [kernel] Parsing tests/syntax/result/label_decl.i (no preprocessing)
 /* Generated by Frama-C */
+struct s {
+   int i ;
+};
+void s_cp(struct s *p, struct s v)
+{
+  *p = v;
+  return;
+}
+
 void main(void)
 {
+  struct s y;
   int i = 0;
   label: ;
   int tmp = i;
+  if (i < 0) goto _LOR;
+  else 
+    if (i >= 256) {
+      _LOR: ;
+      struct s __constr_expr_0 = {.i = 1};
+      s_cp(& y,__constr_expr_0);
+    }
   return;
 }