From b41206413fe870f8e6a5d39938a35216a793422a Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 17 Feb 2020 18:38:40 +0100
Subject: [PATCH] [printer] pretty-prints ghost labels as ghost.
---
.../ast_printing/cil_printer.ml | 9 ++-
src/kernel_services/ast_printing/printer.ml | 56 ++++++++++---------
tests/cil/oracle/ghost_cfg.0.res.oracle | 4 +-
tests/spec/oracle/at.res.oracle | 2 +-
4 files changed, 40 insertions(+), 31 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 5aa6db6a1c5..3294a415408 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1170,13 +1170,16 @@ class cil_printer () = object (self)
method annotated_stmt (next: stmt) fmt (s: stmt) =
pp_open_hvbox fmt 0;
- self#stmt_labels fmt s;
(* print the statement. *)
if Cil.is_skip s.skind && not s.ghost && s.sattr = [] then begin
- if verbose || s.labels <> [] then fprintf fmt ";"
+ if verbose || s.labels <> [] then begin
+ self#stmt_labels fmt s;
+ fprintf fmt ";"
+ end
end else begin
self#in_ghost_if_needed fmt s.ghost ~post_fmt:"%t"
- (fun () -> self#stmtkind s.sattr next fmt s.skind)
+ (fun () ->
+ 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 5d89b10f83d..da8ce9ed3e6 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -196,7 +196,6 @@ class printer_with_annot () = object (self)
loc.Lexing.pos_lnum); *)
Format.pp_open_hvbox fmt 0;
(* print the labels *)
- self#stmt_labels fmt s;
if Kernel.PrintComments.get () then begin
let comments = Globals.get_comments_stmt s in
if comments <> [] then
@@ -207,30 +206,37 @@ class printer_with_annot () = object (self)
if verbose || Kernel.is_debug_key_enabled Kernel.dkey_print_sid then
Format.fprintf fmt "@[/* sid:%d */@]@\n" s.sid ;
(* print the annotations *)
- if logic_printer_enabled then begin
- let all_annot =
- List.sort
- Cil_datatype.Code_annotation.compare
- (Annotations.code_annot s)
- in
- self#in_ghost_if_needed fmt s.ghost ~post_fmt:"%t"
- (fun () -> 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
- self#stmtkind s.sattr next fmt s.skind;
+ if logic_printer_enabled then
+ begin
+ let all_annot =
+ List.sort
+ Cil_datatype.Code_annotation.compare
+ (Annotations.code_annot s)
+ 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) ;
+ end
+ else
+ begin
+ self#stmt_labels fmt s;
+ self#stmtkind s.sattr next fmt s.skind;
+ end;
Format.pp_close_box fmt ()
method! stmtkind sattr (next: stmt) fmt skind =
diff --git a/tests/cil/oracle/ghost_cfg.0.res.oracle b/tests/cil/oracle/ghost_cfg.0.res.oracle
index e1befb2ba50..c4bf9a5dc2d 100644
--- a/tests/cil/oracle/ghost_cfg.0.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.0.res.oracle
@@ -12,7 +12,7 @@
i ++;
[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:60: Warning:
Ghost code breaks CFG starting at:
- case 1: /*@ ghost g = 3; */
+ /*@ ghost case 1: g = 3; */
[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:79: Warning:
Ghost code breaks CFG starting at:
/*@ ghost goto X; */
@@ -21,7 +21,7 @@
/*@ ghost goto X; */
[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:100: Warning:
Ghost code breaks CFG starting at:
- case 1: /*@ ghost x ++; */
+ /*@ ghost case 1: x ++; */
[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:108: Warning:
Ghost code breaks CFG starting at:
/*@ ghost __retres = 1; */
diff --git a/tests/spec/oracle/at.res.oracle b/tests/spec/oracle/at.res.oracle
index 8194269ad90..afc2f1b8b5b 100644
--- a/tests/spec/oracle/at.res.oracle
+++ b/tests/spec/oracle/at.res.oracle
@@ -28,7 +28,7 @@ int f(int y)
{
x += y;
L1: x ++;
- L2: /*@ ghost ; */
+ /*@ ghost L2: ; */
x ++;
/*@ assert \at(x,L1) ≡ \at(x,Pre) + y; */ ;
/*@ assert \at(x,L2) ≡ (1 + \at(x,Pre)) + y; */ ;
--
GitLab