From 0541b4f945a310cb22fd47935a969d7f0bf02c2f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 3 Jan 2019 10:02:16 +0100
Subject: [PATCH] [kernel] keep Skip stmt that have an sattr
---
src/kernel_internals/typing/cabs2cil.ml | 2 +-
src/kernel_services/ast_printing/cil_printer.ml | 4 ++--
src/kernel_services/ast_queries/file.ml | 2 +-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 8cf1b5e6913..0bdc611ed92 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1424,7 +1424,7 @@ struct
let empty_stmts l =
let rec is_empty_stmt s =
match s.skind with
- | Instr (Skip _) -> s.labels = []
+ | Instr (Skip _) -> s.labels = [] && s.sattr = []
| Block b -> b.battrs = [] && List.for_all is_empty_stmt b.bstmts
| UnspecifiedSequence seq ->
List.for_all is_empty_stmt (List.map (fun (x,_,_,_,_) -> x) seq)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 26dea67a97c..1da7b9aa53f 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -495,7 +495,7 @@ class cil_printer () = object (self)
method private current_stmt =
try Some (Stack.top current_stmt) with Stack.Empty -> None
- method private may_be_skipped s = s.labels = []
+ method private may_be_skipped s = s.labels = [] && s.sattr = []
method location fmt loc =
Format.fprintf fmt "%a" Filepath.pp_pos (fst loc)
@@ -1058,7 +1058,7 @@ class cil_printer () = object (self)
pp_open_hvbox fmt 0;
self#stmt_labels fmt s;
(* print the statement. *)
- if Cil.is_skip s.skind && not s.ghost then begin
+ if Cil.is_skip s.skind && not s.ghost && s.sattr = [] then begin
if verbose || s.labels <> [] then fprintf fmt ";"
end else begin
let was_ghost = is_ghost in
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 8b0f5b522b1..0d0b2949cf0 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -918,7 +918,7 @@ let cleanup file =
method! vstmt_aux st =
self#remove_lexical_annotations st;
let loc = Stmt.loc st in
- if Annotations.has_code_annot st || st.labels <> [] then
+ if Annotations.has_code_annot st || st.labels <> [] || st.sattr <> [] then
keep_stmt <- Stmt.Set.add st keep_stmt;
match st.skind with
| Block b ->
--
GitLab