diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index 794e1cc8d4f85f7a6557b614e080cd2671c60663..a5248ccff9865ba8282c2cdf631cb647ea4cb2e1 100644 --- a/src/kernel_services/ast_printing/cil_printer.ml +++ b/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 diff --git a/tests/syntax/label_decl.i b/tests/syntax/label_decl.i index a35c2dce800cb8ef3092a8db696593030a73d7ee..f47ca2a64a658bbc9161ae8faf0e7a852c480b19 100644 --- a/tests/syntax/label_decl.i +++ b/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}); } diff --git a/tests/syntax/oracle/label_decl.res.oracle b/tests/syntax/oracle/label_decl.res.oracle index 9335e7b2570c68494425717b7728a75295e10aeb..00c3bd3ef4dde9fec38209c01b097120091b110b 100644 --- a/tests/syntax/oracle/label_decl.res.oracle +++ b/tests/syntax/oracle/label_decl.res.oracle @@ -1,20 +1,53 @@ [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; }