From 3175ea9030337c039196ebf4c9c4849db386959b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 25 Feb 2020 11:35:54 +0100
Subject: [PATCH] [printer] also protect empty ghost blocks inside non-ghost
environment
---
src/kernel_services/ast_printing/cil_printer.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index b4550d92a6c..80735f7ab24 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1215,6 +1215,8 @@ class cil_printer () = object (self)
gives us at least a correct, compilable, C code.
*)
| _::_::_,[],[],_ -> is_cfg_block ctxt
+ | [s],[],[], (Then_with_else | Other)
+ when (not is_ghost) && s.ghost -> true
| [ { skind = Block b } as s' ], [], [], Stmt_block s ->
(b.bscoping ||
(not (Cil.has_extern_local_init b) && self#stmt_has_annot s))
@@ -1225,8 +1227,6 @@ class cil_printer () = object (self)
| [ { skind = Block b } ], [], [], _ -> self#require_braces ctxt b
| [ { skind = UnspecifiedSequence s } ], [], [], _ ->
self#require_braces ctxt (Cil.block_from_unspecified_sequence s)
- | [s],[],[], (Then_with_else | Other)
- when (not is_ghost) && s.ghost -> true
| [_],[],[], Then_with_else -> self#block_has_dangling_else blk
| [ _ ], [], [], _ -> false
| [],[],[],_ -> false)
--
GitLab