diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 38cee0fc4e529c4880eae49095aeeedf11482939..52d0a5b1ba553f3654f2c9b5d653d346b1aa75fd 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -1980,18 +1980,18 @@ struct let n = mkEmptyStmt ~ghost ~valid_sid ~loc () in n, [n,[],[],[],[]] | s -> - let (st,_,_,_,_) = Extlib.last s in - if not ghost && st.ghost then - (* non-ghost label in front of a ghost statement. Keep the - non-ghost status with a Skip. - Note that the reverse case is not possible: - /*@ ghost L1: */ stmt; will be directly translated - by the parser as /*@ ghost L1: ; */ stmt; - *) - begin - let n = mkEmptyStmt ~ghost ~valid_sid ~loc () in - n, s @ [n,[],[],[],[]] - end else st,s + let (st,_,_,_,_) = Extlib.last s in + if not ghost && st.ghost then + (* non-ghost label in front of a ghost statement. Keep the + non-ghost status with a Skip. + Note that the reverse case is not possible: + /*@ ghost L1: */ stmt; will be directly translated + by the parser as /*@ ghost L1: ; */ stmt; + *) + begin + let n = mkEmptyStmt ~ghost ~valid_sid ~loc () in + n, s @ [n,[],[],[],[]] + end else st,s (* s2c must not be used during expression translation, as it does not take care of the effects of the statement. Use i2c instead. diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index 3294a415408d7f9f322b3285be190cd939c2bf89..14c6d76b21154a392682f90354b353e2286e340a 100644 --- a/src/kernel_services/ast_printing/cil_printer.ml +++ b/src/kernel_services/ast_printing/cil_printer.ml @@ -1173,13 +1173,13 @@ class cil_printer () = object (self) (* print the statement. *) if Cil.is_skip s.skind && not s.ghost && s.sattr = [] then begin if verbose || s.labels <> [] then begin - self#stmt_labels fmt s; - fprintf fmt ";" - end + self#stmt_labels fmt s; + fprintf fmt ";" + end end else begin self#in_ghost_if_needed fmt s.ghost ~post_fmt:"%t" (fun () -> - self#stmt_labels fmt s; self#stmtkind s.sattr next fmt s.skind) + self#stmt_labels fmt s; self#stmtkind s.sattr next fmt s.skind) end; pp_close_box fmt () diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml index da8ce9ed3e6621825b1bbad20f29bad894be5ff7..b864a20fb0d0caa8d2ff7588b14d6ad19f63ad58 100644 --- a/src/kernel_services/ast_printing/printer.ml +++ b/src/kernel_services/ast_printing/printer.ml @@ -215,22 +215,22 @@ class printer_with_annot () = object (self) in self#in_ghost_if_needed fmt s.ghost ~post_fmt:"%t" (fun () -> - self#stmt_labels fmt s; - match all_annot with - | [] -> self#stmtkind s.sattr next fmt s.skind; - | [ a ] when Cil.is_skip s.skind && not s.ghost -> - Format.fprintf fmt "@[<hv>@[%t@ %a@;<1 1>%t@]@ %a@]" - self#begin_annotation - self#code_annotation a - self#end_annotation - (self#stmtkind s.sattr next) s.skind; - | _ -> - let loop_annot, stmt_annot = - List.partition Logic_utils.is_loop_annot all_annot - in - self#annotations fmt stmt_annot; - self#loop_annotations fmt loop_annot; - self#stmtkind s.sattr next fmt s.skind) ; + self#stmt_labels fmt s; + match all_annot with + | [] -> self#stmtkind s.sattr next fmt s.skind; + | [ a ] when Cil.is_skip s.skind && not s.ghost -> + Format.fprintf fmt "@[<hv>@[%t@ %a@;<1 1>%t@]@ %a@]" + self#begin_annotation + self#code_annotation a + self#end_annotation + (self#stmtkind s.sattr next) s.skind; + | _ -> + let loop_annot, stmt_annot = + List.partition Logic_utils.is_loop_annot all_annot + in + self#annotations fmt stmt_annot; + self#loop_annotations fmt loop_annot; + self#stmtkind s.sattr next fmt s.skind) ; end else begin