diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b83030c8f8a27ffce8d6b5d6bdf72ad0eacd044f..0bdc611ed92bee320148dfab22327c22d55d1de1 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)
@@ -1865,10 +1865,10 @@ struct
let canDrop (c: chunk) =
List.for_all (fun (s,_,_,_,_) -> canDropStatement s) c.stmts
- let loopChunk ~ghost a (body: chunk) : chunk =
+ let loopChunk ~ghost ~sattr a (body: chunk) : chunk =
(* Make the statement *)
let loop =
- mkStmt ~ghost ~valid_sid
+ mkStmt ~ghost ~valid_sid ~sattr
(Loop (a,c2block ~ghost body, CurrentLoc.get (), None, None))
in
{ stmts = [ loop,[],[],[],[] ];
@@ -9485,7 +9485,7 @@ and doStatement local_env (s : A.statement) : chunk =
let break_cond = breakChunk ~ghost loc' in
exitLoop ();
CurrentLoc.set loc';
- loopChunk ~ghost a
+ loopChunk ~ghost ~sattr:[Attr("while",[])] a
((doCondition local_env false e skipChunk break_cond)
@@ (s', ghost))
@@ -9520,7 +9520,7 @@ and doStatement local_env (s : A.statement) : chunk =
false e skipChunk (breakChunk ~ghost loc'))
in
exitLoop ();
- loopChunk ~ghost a (s' @@ (s'', ghost))
+ loopChunk ~ghost ~sattr:[Attr("dowhile",[])] a (s' @@ (s'', ghost))
| A.FOR(a,fc1,e2,e3,s,loc) -> begin
let loc' = convLoc loc in
@@ -9545,10 +9545,10 @@ and doStatement local_env (s : A.statement) : chunk =
let res =
match e2.expr_node with
| A.NOTHING -> (* This means true *)
- se1 @@ (loopChunk ~ghost a (s' @@ (s'', ghost)), ghost)
+ se1 @@ (loopChunk ~sattr:[Attr("for",[])] ~ghost a (s' @@ (s'', ghost)), ghost)
| _ ->
se1 @@
- (loopChunk ~ghost a
+ (loopChunk ~sattr:[Attr("for",[])] ~ghost a
(((doCondition
local_env false e2 skipChunk break_cond)
@@ (s', ghost)) @@ (s'', ghost)), ghost)
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index 4ed4a1c7ea381ebe0b282db96d256de616148d30..a14e8c949d178ccb6ae85753051397b002291ff6 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -322,7 +322,8 @@ let copy_block kf switch_label_action break_continue_must_change bl =
succs = [];
preds = [];
skind = stmt.skind;
- ghost = stmt.ghost}
+ ghost = stmt.ghost;
+ sattr = []}
in
let labelled_stmt_tbl =
if stmt.labels = [] then
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 6aea5a03a1390e04aba9a8614cc008473c8c3c28..d9acbb6b3b8891732a8607cce573208df9d8b005 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1062,7 +1062,11 @@ and stmt = {
mutable preds: stmt list;
(** The inverse of the succs function. *)
- mutable ghost : bool
+ mutable ghost : bool;
+
+ mutable sattr : attributes
+ (** Statement attributes.
+ @since Frama-C+dev *)
}
(** Labels *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index b4c6b964b73062e25b193a279e2a4d32c9f2e4c5..1da7b9aa53ffc9d030056d865ebbe672fce02f9c 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
@@ -1068,7 +1068,7 @@ class cil_printer () = object (self)
Format.fprintf fmt "%t %a "
(fun fmt -> self#pp_open_annotation fmt) self#pp_acsl_keyword "ghost"
end;
- self#stmtkind next fmt s.skind ;
+ self#stmtkind s.sattr next fmt s.skind ;
if display_ghost then begin
is_ghost <- false;
self#pp_close_annotation fmt
@@ -1234,7 +1234,7 @@ class cil_printer () = object (self)
fprintf fmt "@[@<0>\n@<0>%s@<0> @<0>%d@<0> @<0>%s@]@\n"
directive (fst l).Filepath.pos_lnum filename
- method stmtkind (next: stmt) fmt = function
+ method stmtkind sattr (next: stmt) fmt = function
| UnspecifiedSequence seq ->
let ctxt =
match self#current_stmt with None -> Other | Some s -> Stmt_block s
@@ -1374,6 +1374,11 @@ class cil_printer () = object (self)
Pretty_utils.pp_list ~sep:"@\n" self#code_annotation fmt a;
Format.fprintf fmt "@ %t" (fun fmt -> self#pp_close_annotation fmt);
end;
+ let pp_sattr fmt =
+ if sattr <> [] && Kernel.is_debug_key_enabled Kernel.dkey_print_attrs
+ then Format.fprintf fmt "@[/*%a */ @]" self#attributes sattr
+ else Format.ifprintf fmt ""
+ in
((* Maybe the first thing is a conditional. Turn it into a WHILE *)
try
let rec skipEmpty = function
@@ -1409,15 +1414,17 @@ class cil_printer () = object (self)
[{ skind=Block b} as s ] when self#may_be_skipped s -> b
| _ -> { b with bstmts = bodystmts }
in
- Format.fprintf fmt "%a@[<v 2>%a (%a) %a@]"
+ Format.fprintf fmt "%a@[<v 2>%a (%a) %t%a@]"
(fun fmt -> self#line_directive fmt) l
self#pp_keyword "while"
self#exp term
+ pp_sattr
(self#unboxed_block Other) b;
with Not_found ->
- Format.fprintf fmt "%a@[<v 2>%a (1) %a@]"
+ Format.fprintf fmt "%a@[<v 2>%a (1) %t%a@]"
(fun fmt -> self#line_directive fmt) l
self#pp_keyword "while"
+ pp_sattr
(self#unboxed_block Other) b);
Format.pp_close_box fmt ()
diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index 61f6615b15fa27c804ac4048523ac2f2834ff36f..b6ced2eb01a5166366c46d2026e418b1c6779152 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -244,7 +244,7 @@ class printer_with_annot () = object (self)
self#pp_acsl_keyword "ghost";
is_ghost <- true
end;
- self#stmtkind next fmt s.skind;
+ self#stmtkind s.sattr next fmt s.skind;
if not was_ghost && s.ghost then begin
self#pp_close_annotation ~suf:"@,*/@]" fmt;
is_ghost <- false;
@@ -257,7 +257,7 @@ class printer_with_annot () = object (self)
(fun fmt -> self#pp_open_annotation ~block:false fmt)
self#code_annotation a
(fun fmt -> self#pp_close_annotation ~block:false fmt)
- (self#stmtkind next) s.skind;
+ (self#stmtkind s.sattr next) s.skind;
| _ ->
let loop_annot, stmt_annot =
List.partition Logic_utils.is_loop_annot all_annot
@@ -266,11 +266,11 @@ class printer_with_annot () = object (self)
self#loop_annotations fmt loop_annot;
pGhost fmt s)
end else
- self#stmtkind next fmt s.skind;
+ self#stmtkind s.sattr next fmt s.skind;
Format.pp_close_box fmt ()
- method! stmtkind (next: stmt) fmt skind =
- super#stmtkind next fmt
+ method! stmtkind sattr (next: stmt) fmt skind =
+ super#stmtkind sattr next fmt
begin
match skind with
| Goto({ contents = { skind = (Return _) as return }},_)
diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli
index 493de08bad1d547358b357dd0086f1c03e00f76c..15bfee3925cc10931886343dd1a88b79320cf67a 100644
--- a/src/kernel_services/ast_printing/printer_api.mli
+++ b/src/kernel_services/ast_printing/printer_api.mli
@@ -190,7 +190,7 @@ class type extensible_printer_type = object
last {!Cil_types.stmt} argument. The initial {!Cil_types.stmt} argument
records the statement which follows the one being printed. *)
- method stmtkind: stmt -> Format.formatter -> stmtkind -> unit
+ method stmtkind: attributes -> stmt -> Format.formatter -> stmtkind -> unit
(** Print a statement kind. The code to be printed is given in the
{!Cil_types.stmtkind} argument. The initial {!Cil_types.stmt} argument
records the statement which follows the one being printed;
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 9493c45605a07006f03f9a29264b86f09364cfcf..86eb84205298d80638abceaf63fc096dda62aa85 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -265,7 +265,7 @@ let mkBlock (slst: stmt list) : block =
let mkBlockNonScoping l = let b = mkBlock l in b.bscoping <- false; b
-let mkStmt ?(ghost=false) ?(valid_sid=false) (sk: stmtkind) : stmt =
+let mkStmt ?(ghost=false) ?(valid_sid=false) ?(sattr=[]) (sk: stmtkind) : stmt =
{ skind = sk;
labels = [];
(* It is better to create statements with a valid sid, so that they can
@@ -274,7 +274,8 @@ let mkStmt ?(ghost=false) ?(valid_sid=false) (sk: stmtkind) : stmt =
(e.g. slicing). *)
sid = if valid_sid then Sid.next () else -1;
succs = []; preds = [];
- ghost = ghost}
+ ghost = ghost;
+ sattr = sattr;}
let stmt_of_instr_list ?(loc=Location.unknown) = function
| [] -> Instr (Skip loc)
@@ -4212,7 +4213,7 @@ let parseIntExp ~loc repr =
let mkStmtCfg ~before ~(new_stmtkind:stmtkind) ~(ref_stmt:stmt) : stmt =
let new_ = { skind = new_stmtkind;
labels = [];
- sid = -1; succs = []; preds = []; ghost = false }
+ sid = -1; succs = []; preds = []; ghost = false; sattr = [] }
in
new_.sid <- Sid.next ();
if before then begin
@@ -4263,10 +4264,11 @@ let parseIntExp ~loc repr =
old_preds;
n
- let mkEmptyStmt ?ghost ?valid_sid ?(loc=Location.unknown) () =
- mkStmt ?ghost ?valid_sid (Instr (Skip loc))
+ let mkEmptyStmt ?ghost ?valid_sid ?sattr ?(loc=Location.unknown) () =
+ mkStmt ?ghost ?valid_sid ?sattr (Instr (Skip loc))
- let mkStmtOneInstr ?ghost ?valid_sid i = mkStmt ?ghost ?valid_sid (Instr i)
+ let mkStmtOneInstr ?ghost ?valid_sid ?sattr i =
+ mkStmt ?ghost ?valid_sid ?sattr (Instr i)
let dummyInstr = Asm([], ["dummy statement!!"], None, Location.unknown)
let dummyStmt = mkStmt (Instr dummyInstr)
@@ -4310,9 +4312,9 @@ let parseIntExp ~loc repr =
let mkString ~loc s = new_exp ~loc (Const(CStr s))
- let mkWhile ~(guard:exp) ~(body: stmt list) : stmt list =
+ let mkLoop ?(sattr = [Attr("while", [])]) ~(guard:exp) ~(body: stmt list) : stmt list =
(* Do it like this so that the pretty printer recognizes it *)
- [ mkStmt ~valid_sid:true
+ [ mkStmt ~valid_sid:true ~sattr
(Loop ([],
mkBlock
(mkStmt ~valid_sid:true
@@ -4324,7 +4326,7 @@ let parseIntExp ~loc repr =
let mkFor ~(start: stmt list) ~(guard: exp) ~(next: stmt list)
~(body: stmt list) : stmt list =
(start @
- (mkWhile guard (body @ next)))
+ (mkLoop ~sattr:[Attr("For",[])] ~guard ~body:(body @ next)))
let mkForIncr ~(iter : varinfo) ~(first: exp) ~(stopat: exp) ~(incr: exp)
~(body: stmt list) : stmt list =
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index ec5424a8b4737a8b5d4f2fa0542525ebfb922b8d..799986722ec0afbc0e43e5acc5cffcd8fb59c5a0 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1025,7 +1025,8 @@ val appears_in_expr: varinfo -> exp -> bool
if [valid_sid] is false (the default),
or to a valid sid if [valid_sid] is true,
and [labels], [succs] and [preds] to the empty list *)
-val mkStmt: ?ghost:bool -> ?valid_sid:bool -> stmtkind -> stmt
+val mkStmt: ?ghost:bool -> ?valid_sid:bool -> ?sattr:attributes -> stmtkind ->
+ stmt
(* make the [new_stmtkind] changing the CFG relatively to [ref_stmt] *)
val mkStmtCfg: before:bool -> new_stmtkind:stmtkind -> ref_stmt:stmt -> stmt
@@ -1048,7 +1049,8 @@ val mkStmtCfgBlock: stmt list -> stmt
(** Construct a statement consisting of just one instruction
See {!Cil.mkStmt} for the signification of the optional args.
*)
-val mkStmtOneInstr: ?ghost:bool -> ?valid_sid:bool -> instr -> stmt
+val mkStmtOneInstr: ?ghost:bool -> ?valid_sid:bool -> ?sattr:attributes ->
+ instr -> stmt
(** Try to compress statements so as to get maximal basic blocks.
* use this instead of List.@ because you get fewer basic blocks *)
@@ -1057,7 +1059,8 @@ val mkStmtOneInstr: ?ghost:bool -> ?valid_sid:bool -> instr -> stmt
(** Returns an empty statement (of kind [Instr]). See [mkStmt] for [ghost] and
[valid_sid] arguments.
@modify Neon-20130301 adds the [valid_sid] optional argument. *)
-val mkEmptyStmt: ?ghost:bool -> ?valid_sid:bool -> ?loc:location -> unit -> stmt
+val mkEmptyStmt: ?ghost:bool -> ?valid_sid:bool -> ?sattr:attributes ->
+ ?loc:location -> unit -> stmt
(** A instr to serve as a placeholder *)
val dummyInstr: instr
@@ -1089,8 +1092,10 @@ val mkPureExpr:
?ghost:bool -> ?valid_sid:bool -> fundec:fundec ->
?loc:location -> exp -> stmt
-(** Make a while loop. Can contain Break or Continue *)
-val mkWhile: guard:exp -> body:stmt list -> stmt list
+(** Make a loop. Can contain Break or Continue.
+ The kind of loop (While, For, DoWhile) is given by [sattr];
+ it is a While loop if unspecified. *)
+val mkLoop: ?sattr:attributes -> guard:exp -> body:stmt list -> stmt list
(** Make a for loop for(i=start; i<past; i += incr) \{ ... \}. The body
can contain Break but not Continue. Can be used with i a pointer
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 11ee585d0ccc150d1b3c9305f0fec6314753e2ec..4603eeb11fa5b9f38eee5d96a67ca73ace3757de 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -271,7 +271,8 @@ module Stmt_Id = struct
sid = -1;
succs = [];
preds = [];
- ghost = false } ]
+ ghost = false;
+ sattr = [] } ]
let compare t1 t2 = Datatype.Int.compare t1.sid t2.sid
let hash t1 = t1.sid
let equal t1 t2 = t1.sid = t2.sid
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 8b0f5b522b18bb4dae2d71f3433482d83c7f35d0..0d0b2949cf04b95003c0fd38891e45d4e700d069 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 ->
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index 4b3263d04dec3295a5047a62bc3ab4a6e7f57c5a..9bd7e7586f61a621f3bf1316e0e1b99fa52dc7f4 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -641,11 +641,11 @@ module TagPrinterClassDeferred (X: Printer.PrinterClass) = struct
Format.fprintf fmt "@{<%s>%a@}"
(Tag.create (PIP ip)) (super#allocation ~isloop) a;
- method! stmtkind next fmt sk =
+ method! stmtkind sattr next fmt sk =
(* Special tag denoting the start of the statement, WITHOUT any ACSL
assertion/statement contract, etc. *)
let s = Extlib.the self#current_stmt in
- Format.fprintf fmt "@{<gui:stmt_start%d>%a@}" s.sid (super#stmtkind next) sk
+ Format.fprintf fmt "@{<gui:stmt_start%d>%a@}" s.sid (super#stmtkind sattr next) sk
initializer force_brace <- true
diff --git a/src/plugins/slicing/printSlice.ml b/src/plugins/slicing/printSlice.ml
index 1f0109af6dd177363c41988512b1aa0221f8e92a..37e5f8a1c6704e77656fca762cf1ad60d1ae412d 100644
--- a/src/plugins/slicing/printSlice.ml
+++ b/src/plugins/slicing/printSlice.ml
@@ -75,7 +75,7 @@ class printerClass optional_ff = object(self)
str_m
super#vdecl var
- method! stmtkind next fmt kind =
+ method! stmtkind sattr next fmt kind =
let stmt_info fmt stmt = match opt_ff with
| None -> Format.fprintf fmt "@[/* %d */@]" stmt.Cil_types.sid
| Some ff ->
@@ -94,7 +94,7 @@ class printerClass optional_ff = object(self)
try
Format.fprintf fmt "@[<v>%a@ %a@]"
stmt_info s
- (fun fmt -> super#stmtkind next fmt) kind
+ (fun fmt -> super#stmtkind sattr next fmt) kind
with Not_found ->
(* some sub statements may be visible *)
let sub_stmts = find_sub_stmts s in