diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 48b894205eecc0bf98e06c87e05c3a1cc0c6913a..42b88e95e867c4fef0baf76a19e551bce5c492e5 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2100,82 +2100,89 @@ struct
Cil_printer.pp_stmt s l;
with Found -> ()
- class cleanUnspecified = object(self)
- inherit nopCilVisitor
- val unspecified_stack = Stack.create ()
-
- val mutable replace_table = []
-
- (* we start in a deterministic block. *)
- initializer Stack.push false unspecified_stack
-
- method private push: 'a.bool->'a->'a visitAction =
- fun flag x ->
- Stack.push flag unspecified_stack;
- ChangeDoChildrenPost
- (x,fun x -> ignore(Stack.pop unspecified_stack); x)
-
-
- method! vblock b =
- b.bstmts <-
- List.rev
- (List.fold_left(
- fun res s ->
- match s.skind with
- | Block b when
- (not (Stack.top unspecified_stack)) &&
- b.battrs = [] && b.blocals = [] &&
- s.labels = []
- -> List.rev_append b.bstmts res
- | _ -> s ::res)
- [] b.bstmts);
- DoChildren
-
- method! vstmt s =
- let ghost = s.ghost in
- let change_label_stmt s s' =
- List.iter
- (function
- | Label (x,_,_) -> H.replace labelStmt x s'
- | Case _ | Default _ -> replace_table <- (s, s') :: replace_table
- ) s.labels;
- s'.labels <- s.labels @ s'.labels
- in
- match s.skind with
- | UnspecifiedSequence [s',_,_,_,_] ->
- change_label_stmt s s';
- ChangeDoChildrenPost(s', fun x -> x)
- | UnspecifiedSequence [] ->
- let s' = mkEmptyStmt ~ghost ~valid_sid ~loc:(cabslu "_useq") () in
- change_label_stmt s s';
- ChangeTo s';
- | UnspecifiedSequence _ -> self#push true s
- | Block { battrs = []; blocals = []; bstmts = [s']} ->
- change_label_stmt s s';
- ChangeDoChildrenPost (s', fun x -> x)
- | Block _ | If _ | Loop _
- | TryFinally _ | TryExcept _ | Throw _ | TryCatch _ ->
- self#push false s
- | Switch _ ->
- let change_cases stmt =
- match stmt.skind with
- | Switch(e,body,cases,loc) ->
- let newcases =
- List.map
- (fun s ->
- try List.assq s replace_table
- with Not_found -> s)
- cases
- in
- stmt.skind <- Switch(e,body,newcases,loc);
- ignore (Stack.pop unspecified_stack);
- stmt
- | _ -> assert false
- in Stack.push false unspecified_stack;
- ChangeDoChildrenPost(s,change_cases)
- | Instr _ | Return _ | Goto _ | Break _
- | Continue _ -> DoChildren
- end
+ class cleanUnspecified =
+ let is_annot_next_stmt = function
+ | [] -> false
+ | { skind = Instr (Code_annot (c,_)) } :: _ ->
+ Logic_utils.is_annot_next_stmt c
+ | _ -> false
+ in
+ object(self)
+ inherit nopCilVisitor
+ val unspecified_stack = Stack.create ()
+
+ val mutable replace_table = []
+
+ (* we start in a deterministic block. *)
+ initializer Stack.push false unspecified_stack
+
+ method private push: 'a.bool->'a->'a visitAction =
+ fun flag x ->
+ Stack.push flag unspecified_stack;
+ ChangeDoChildrenPost
+ (x,fun x -> ignore(Stack.pop unspecified_stack); x)
+
+
+ method! vblock b =
+ b.bstmts <-
+ List.rev
+ (List.fold_left(
+ fun res s ->
+ match s.skind with
+ | Block b when
+ (not (Stack.top unspecified_stack)) &&
+ b.battrs = [] && b.blocals = [] &&
+ s.labels = [] && not (is_annot_next_stmt res)
+ -> List.rev_append b.bstmts res
+ | _ -> s ::res)
+ [] b.bstmts);
+ DoChildren
+
+ method! vstmt s =
+ let ghost = s.ghost in
+ let change_label_stmt s s' =
+ List.iter
+ (function
+ | Label (x,_,_) -> H.replace labelStmt x s'
+ | Case _ | Default _ -> replace_table <- (s, s') :: replace_table
+ ) s.labels;
+ s'.labels <- s.labels @ s'.labels
+ in
+ match s.skind with
+ | UnspecifiedSequence [s',_,_,_,_] ->
+ change_label_stmt s s';
+ ChangeDoChildrenPost(s', fun x -> x)
+ | UnspecifiedSequence [] ->
+ let s' = mkEmptyStmt ~ghost ~valid_sid ~loc:(cabslu "_useq") () in
+ change_label_stmt s s';
+ ChangeTo s';
+ | UnspecifiedSequence _ -> self#push true s
+ | Block { battrs = []; blocals = []; bstmts = [s']} ->
+ change_label_stmt s s';
+ ChangeDoChildrenPost (s', fun x -> x)
+ | Block _ | If _ | Loop _
+ | TryFinally _ | TryExcept _ | Throw _ | TryCatch _ ->
+ self#push false s
+ | Switch _ ->
+ let change_cases stmt =
+ match stmt.skind with
+ | Switch(e,body,cases,loc) ->
+ let newcases =
+ List.map
+ (fun s ->
+ try List.assq s replace_table
+ with Not_found -> s)
+ cases
+ in
+ stmt.skind <- Switch(e,body,newcases,loc);
+ ignore (Stack.pop unspecified_stack);
+ stmt
+ | _ -> assert false
+ in Stack.push false unspecified_stack;
+ ChangeDoChildrenPost(s,change_cases)
+ | Instr _ | Return _ | Goto _ | Break _
+ | Continue _ -> DoChildren
+ end
let mkFunctionBody ~ghost (c: chunk) : block =
if c.cases <> [] then
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index f1b5ab00c66af69aa7d722dccca1787ab8e07fed..2b8c620ea6b01e18ec5c712bce14e2b39c4ee70f 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1180,6 +1180,9 @@ class cil_printer () = object (self)
method annotated_stmt (next: stmt) fmt (s: stmt) =
pp_open_hvbox fmt 0;
+ if Kernel.is_debug_key_enabled Kernel.dkey_print_sid then begin
+ Format.fprintf fmt "/* sid:%d */@\n" s.sid;
+ end;
(* print the statement. *)
if Cil.is_skip s.skind && not s.ghost && s.sattr = [] then begin
if verbose || s.labels <> [] then begin
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 49e7e958ce5a96351fbfc9e40334e2f6a7d70fdd..a1635dcd9dfa7ffa5f361137529f12c97e9eabb2 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -730,28 +730,6 @@ let synchronize_source_annot has_new_stmt kf =
| Some block, Some stmt_father when block == stmt_father -> true
| _, _ -> false
in
- let is_annot_next annot =
- match annot.annot_content with
- | AStmtSpec _ | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt)
- -> true
- | AExtended(_,is_loop,{ext_name}) ->
- let warn_not_a_code_annot () =
- Kernel.(
- warning ~wkey:wkey_acsl_extension
- "%s is not a code annotation extension" name)
- in
- (match Logic_env.extension_category ext_name with
- | exception Not_found -> warn_not_a_code_annot () ; false
- | Ext_code_annot (Ext_here | Ext_next_loop)-> false
- | Ext_code_annot Ext_next_stmt-> true
- | Ext_code_annot Ext_next_both-> not is_loop
- | Ext_contract | Ext_global -> warn_not_a_code_annot () ; false)
- | AAssert _ | AInvariant _ | AVariant _
- | AAssigns _ | AAllocation _
- | APragma (Slice_pragma (SPctrl | SPexpr _))
- | APragma (Impact_pragma (IPexpr _))
- | APragma (Loop_pragma _) -> false
- in
let synchronize_user_annot a = add_annotation kf st a in
let synchronize_previous_user_annots () =
if !user_annots_for_next_stmt <> [] then begin
@@ -759,7 +737,7 @@ let synchronize_source_annot has_new_stmt kf =
let my_annots = !user_annots_for_next_stmt in
let post_action st =
let treat_annot (has_annot,st) (st_ann, annot) =
- if is_annot_next annot then begin
+ if Logic_utils.is_annot_next_stmt annot then begin
if has_annot || st.labels <> [] || st_ann.labels <> []
then begin
st_ann.skind <- (Block (Cil.mkBlockNonScoping [st]));
@@ -822,7 +800,7 @@ let synchronize_source_annot has_new_stmt kf =
(* Code annotation isn't considered as a real stmt.
So, previous annotations should be relative to the next stmt.
Only this [annot] may be synchronised to that stmt *)
- if is_annot_next annot then
+ if Logic_utils.is_annot_next_stmt annot then
(* Annotation relative to the effect of next statement *)
add_user_annot_for_next_stmt st annot
else
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index bbc4329de6ad25ea69a96dc56cc6e162e7178296..41237fee5871725c0547b3203b220c9d155189ef 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -573,6 +573,27 @@ let is_trivially_true p =
Ptrue -> true
| _ -> false
+let is_annot_next_stmt c =
+ match c.annot_content with
+ | AStmtSpec _ | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt) -> true
+ | AExtended(_,is_loop,{ext_name}) ->
+ let warn_not_a_code_annot () =
+ Kernel.(
+ warning ~wkey:wkey_acsl_extension
+ "%s is not a code annotation extension" ext_name)
+ in
+ (match Logic_env.extension_category ext_name with
+ | exception Not_found -> warn_not_a_code_annot () ; false
+ | Ext_code_annot (Ext_here | Ext_next_loop)-> false
+ | Ext_code_annot Ext_next_stmt-> true
+ | Ext_code_annot Ext_next_both-> not is_loop
+ | Ext_contract | Ext_global -> warn_not_a_code_annot () ; false)
+ | AAssert _ | AInvariant _ | AVariant _
+ | AAssigns _ | AAllocation _
+ | APragma (Slice_pragma (SPctrl | SPexpr _))
+ | APragma (Impact_pragma (IPexpr _))
+ | APragma (Loop_pragma _) -> false
+
let rec add_attribute_glob_annot a g =
match g with
| Dfun_or_pred ({ l_var_info },_) | Dinvariant({ l_var_info }, _)
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index c19683aac4bb6be426d7fe3beea43e068a201b81..b3a51cdf016276f06e81b7305fa266f6e1598e06 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -250,6 +250,15 @@ val is_trivially_true: predicate -> bool
@since Nitrogen-20111001 *)
val is_trivially_false: predicate -> bool
+(** {2 Code annotations} *)
+
+(** Does the annotation apply to the next statement (e.g. a statement
+ contract). Also false for loop-related annotations.
+
+ @since Frama-C+dev
+*)
+val is_annot_next_stmt: code_annotation -> bool
+
(** {2 Global annotations} *)
(** add an attribute to a global annotation
diff --git a/tests/spec/oracle/stmt_contract.res.oracle b/tests/spec/oracle/stmt_contract.res.oracle
index c60dcabab0aa59db45c8a43697c0d0aead29f3cd..f8723d8fb48dadda23c29a64c262bb2c9915ada3 100644
--- a/tests/spec/oracle/stmt_contract.res.oracle
+++ b/tests/spec/oracle/stmt_contract.res.oracle
@@ -38,6 +38,8 @@ int main(int c)
/*@ requires before_label: \true; */
label: /*@ requires after_label: \true; */
y = 8;
+ /*@ ensures x ≡ 0 ∨ x ≡ 7; */
+ if (c >= 3) x = 0; else x = 7;
/*@ requires x ≡ 7; */
/*@ ensures x ≡ 7; */
{
diff --git a/tests/spec/stmt_contract.i b/tests/spec/stmt_contract.i
index ccac6381fcc02c19553470c0a2f3fafa1d5e2116..80e9690322af910e19338869db6b290668f14b7b 100644
--- a/tests/spec/stmt_contract.i
+++ b/tests/spec/stmt_contract.i
@@ -32,6 +32,9 @@ int main(int c) {
//@ requires after_label: \true;
y=8;
+ /*@ ensures x == 0 || x == 7; */
+ x = (c >= 3) ? 0 : 7;
+
/*@ requires x == 7; */
/*@ ensures x == 7; */
return 0;