From 0d64e4bf54395541f410a389be094baf47b7861a Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 18 Feb 2020 08:49:55 +0100
Subject: [PATCH] indentation
---
src/kernel_internals/typing/cabs2cil.ml | 24 +++++++-------
.../ast_printing/cil_printer.ml | 8 ++---
src/kernel_services/ast_printing/printer.ml | 32 +++++++++----------
3 files changed, 32 insertions(+), 32 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 38cee0fc4e5..52d0a5b1ba5 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 3294a415408..14c6d76b211 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 da8ce9ed3e6..b864a20fb0d 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
--
GitLab