diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 64bcad8cbaec0a7b35377f266cbcb557edc158fb..b0b3d4041b92d074c9ff3986214f04f9fb1fb291 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -454,6 +454,12 @@ let rec has_unprotected_local_init s =
| Block { bscoping = false; bstmts = s :: _ } -> has_unprotected_local_init s
| _ -> false
+(** Annotation context in which the Printer is *)
+type annot_ctxt =
+ | Not_in_annot (** not in annotation *)
+ | In_simple_annot (** in /*@ ... */ annotation *)
+ | In_nested_annot (** in /@ ... @/ annotation *)
+
class cil_printer () = object (self)
val mutable logic_printer_enabled = true
@@ -462,13 +468,51 @@ class cil_printer () = object (self)
method pp_keyword fmt s = pp_print_string fmt s
method pp_acsl_keyword = self#pp_keyword
+
+ val mutable annot_ctxt = Not_in_annot
+
method pp_open_annotation ?(block=true) ?(pre=format_of_string "/*@@") fmt =
+ let pre = match annot_ctxt with
+ | Not_in_annot -> annot_ctxt <- In_simple_annot ; pre
+ | In_simple_annot -> annot_ctxt <- In_nested_annot ; format_of_string "/@@"
+ | _ -> assert false (* cannot enter an annotation in a internal annotation *)
+ in
(if block then Pretty_utils.pp_open_block else Format.fprintf)
fmt "%(%)" pre
method pp_close_annotation ?(block=true) ?(suf=format_of_string "*/") fmt =
+ let suf = match annot_ctxt with
+ | In_nested_annot -> annot_ctxt <- In_simple_annot ; format_of_string "@@/"
+ | In_simple_annot -> annot_ctxt <- Not_in_annot ; suf
+ | _ -> assert false (* we should not have to close an annotation that is not open *)
+ in
(if block then Pretty_utils.pp_close_block else Format.fprintf)
fmt "%(%)" suf
+ val mutable verbose = false
+ (* Do not add a value that depends on a
+ non-constant variable of the kernel here (e.g. [Kernel.Debug.get ()]). Due
+ to the way the pretty-printing class is instantiated, this value would be
+ evaluated too soon. Override the [reset] method instead. *)
+
+ (* indicates whether we are printing ghost elements *)
+ val mutable is_ghost = false
+ method private display_comment () = not is_ghost || verbose
+
+ method private in_ghost_if_needed fmt ghost_flag ~post_fmt ?block do_it =
+ let display_ghost = ghost_flag && not is_ghost in
+ if display_ghost then begin
+ is_ghost <- true ;
+ Format.fprintf fmt "%t %a@ "
+ (fun fmt -> self#pp_open_annotation ?block fmt)
+ self#pp_acsl_keyword "ghost"
+ end ;
+ do_it () ;
+ if display_ghost then begin
+ is_ghost <- false;
+ Format.fprintf fmt post_fmt
+ (fun fmt -> self#pp_close_annotation ?block fmt)
+ end
+
method without_annot:
'a. (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit =
fun f fmt x ->
@@ -487,12 +531,6 @@ class cil_printer () = object (self)
let finally () = force_brace <- tmp in
Extlib.try_finally ~finally f fmt x;
- val mutable verbose = false
- (* Do not add a value that depends on a
- non-constant variable of the kernel here (e.g. [Kernel.Debug.get ()]). Due
- to the way the pretty-printing class is instantiated, this value would be
- evaluated too soon. Override the [reset] method instead. *)
-
val current_stmt = Stack.create ()
val mutable current_function = None
@@ -1094,10 +1132,6 @@ class cil_printer () = object (self)
method fundec fmt fd = fprintf fmt "%a" self#varinfo fd.svar
- (* number of opened ghost code *)
- val mutable is_ghost = false
- method private display_comment () = not is_ghost || verbose
-
method annotated_stmt (next: stmt) fmt (s: stmt) =
pp_open_hvbox fmt 0;
self#stmt_labels fmt s;
@@ -1105,18 +1139,8 @@ class cil_printer () = object (self)
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
- let display_ghost = s.ghost && not was_ghost in
- if display_ghost then begin
- is_ghost <- true;
- Format.fprintf fmt "%t %a "
- (fun fmt -> self#pp_open_annotation fmt) self#pp_acsl_keyword "ghost"
- end;
- self#stmtkind s.sattr next fmt s.skind ;
- if display_ghost then begin
- is_ghost <- false;
- self#pp_close_annotation fmt
- end
+ self#in_ghost_if_needed fmt s.ghost ~post_fmt:"%t"
+ (fun () -> self#stmtkind s.sattr next fmt s.skind)
end;
pp_close_box fmt ()
@@ -1190,18 +1214,10 @@ class cil_printer () = object (self)
| _ -> false
method private vdecl_complete fmt v =
- let display_ghost = v.vghost && not is_ghost in
- Format.fprintf fmt "@[<hov 0>%t%a;%t@]"
- (if display_ghost then (fun fmt ->
- Format.fprintf fmt "%t %a@ "
- (fun fmt -> self#pp_open_annotation ~block:false fmt)
- self#pp_acsl_keyword "ghost")
- else ignore)
- self#vdecl v
- (if display_ghost
- then (fun fmt -> Format.fprintf fmt "@ %t"
- (fun fmt -> self#pp_close_annotation ~block:false fmt))
- else ignore)
+ Format.fprintf fmt "@[<hov 0>" ;
+ self#in_ghost_if_needed fmt v.vghost ~post_fmt:"@ %t" ~block:false
+ (fun () -> Format.fprintf fmt "%a;" self#vdecl v) ;
+ Format.fprintf fmt "@]"
(* no box around the block *)
method private unboxed_block
@@ -1541,22 +1557,24 @@ class cil_printer () = object (self)
match g with
| GFun (fundec, l) ->
self#in_current_function fundec.svar;
- (* If the function has attributes then print a prototype because
- * GCC cannot accept function attributes in a definition *)
- let oldattr = fundec.svar.vattr in
- let oldattr = List.filter keep_attr oldattr in
- (* Always print the file name before function declarations *)
- (* Prototype first *)
- if oldattr <> [] then
- (self#line_directive fmt l;
- fprintf fmt "%a@\n"
- self#vdecl_complete fundec.svar);
- (* Temporarily remove the function attributes *)
- fundec.svar.vattr <- [];
- (* Body now *)
- self#line_directive ~forcefile:true fmt l;
- self#fundecl fmt fundec;
- fundec.svar.vattr <- oldattr;
+ self#in_ghost_if_needed fmt fundec.svar.vghost ~post_fmt:"%t@\n"
+ (fun () ->
+ (* If the function has attributes then print a prototype because
+ * GCC cannot accept function attributes in a definition *)
+ let oldattr = fundec.svar.vattr in
+ let oldattr = List.filter keep_attr oldattr in
+ (* Always print the file name before function declarations *)
+ (* Prototype first *)
+ if oldattr <> [] then
+ (self#line_directive fmt l;
+ fprintf fmt "%a@\n"
+ self#vdecl_complete fundec.svar);
+ (* Temporarily remove the function attributes *)
+ fundec.svar.vattr <- [];
+ (* Body now *)
+ self#line_directive ~forcefile:true fmt l;
+ self#fundecl fmt fundec;
+ fundec.svar.vattr <- oldattr) ;
fprintf fmt "@\n";
self#out_current_function
@@ -1610,21 +1628,16 @@ class cil_printer () = object (self)
| GVar (vi, io, l) ->
self#line_directive ~forcefile:true fmt l;
Format.fprintf fmt "@[<hov 2>";
- if vi.vghost then
- Format.fprintf fmt "%t %a@ "
- (fun fmt -> self#pp_open_annotation ~block:false fmt)
- self#pp_acsl_keyword "ghost";
- self#vdecl fmt vi;
- (match io.init with
- | None -> ()
- | Some i ->
- fprintf fmt " =@ ";
- self#init fmt i;
- );
- fprintf fmt ";";
- if vi.vghost then
- Format.fprintf fmt "@ %t"
- (fun fmt -> self#pp_close_annotation ~block:false fmt);
+ self#in_ghost_if_needed fmt vi.vghost ~post_fmt:"@ %t" ~block:false
+ (fun () ->
+ self#vdecl fmt vi;
+ (match io.init with
+ | None -> ()
+ | Some i ->
+ fprintf fmt " =@ ";
+ self#init fmt i;
+ );
+ fprintf fmt ";") ;
fprintf fmt "@]@\n";
(* print global variable 'extern' declarations *)
@@ -1724,26 +1737,13 @@ class cil_printer () = object (self)
method private fundecl fmt f =
(* declaration. *)
- let was_ghost = is_ghost in
- let entering_ghost = f.svar.vghost && not was_ghost in
- fprintf fmt "@[%t%a@\n@[<v 2>"
- (if entering_ghost then (fun fmt ->
- Format.fprintf fmt "%t %a@ "
- (fun fmt -> self#pp_open_annotation ~block:false fmt)
- self#pp_acsl_keyword "ghost")
- else ignore)
- self#vdecl f.svar;
- (* We take care of locals in blocks. *)
- (*List.iter (fprintf fmt "@\n%a;" self#vdecl) f.slocals ;*)
- (* body. *)
- if entering_ghost then is_ghost <- true;
- self#unboxed_block Body fmt f.sbody;
- if entering_ghost then is_ghost <- false;
- fprintf fmt "@]%t@]@."
- (if entering_ghost
- then (fun fmt -> Format.fprintf fmt "@ %t"
- (fun fmt -> self#pp_close_annotation ~block:false fmt))
- else ignore)
+ fprintf fmt "@[";
+ self#in_ghost_if_needed fmt f.svar.vghost ~post_fmt:"@ %t" ~block:false
+ (fun () ->
+ fprintf fmt "%a@\n@[<v 2>" self#vdecl f.svar;
+ self#unboxed_block Body fmt f.sbody;
+ fprintf fmt "@]") ;
+ fprintf fmt "@]@."
(***** PRINTING DECLARATIONS and TYPES ****)
diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index 294c40cd7425dcd9e8965befa437e02683c97a2e..5d89b10f83d796dcc7b8409fbad5bbe8fd1008c2 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -167,12 +167,10 @@ class printer_with_annot () = object (self)
super#global fmt glob
method private begin_annotation fmt =
- let pre = if is_ghost then Some ("@@/": Pretty_utils.sformat) else None in
- self#pp_open_annotation ~block:false ?pre fmt
+ self#pp_open_annotation ~block:false fmt
method private end_annotation fmt =
- let suf = if is_ghost then Some ("@@/": Pretty_utils.sformat) else None in
- self#pp_close_annotation ~block:false ?suf fmt
+ self#pp_close_annotation ~block:false fmt
method private loop_annotations fmt annots =
if annots <> [] then
@@ -215,35 +213,22 @@ class printer_with_annot () = object (self)
Cil_datatype.Code_annotation.compare
(Annotations.code_annot s)
in
- let pGhost fmt s =
- let was_ghost = is_ghost in
- if not was_ghost && s.ghost then begin
- Format.fprintf fmt "%t %a "
- (fun fmt -> self#pp_open_annotation ~pre:"@[/*@@" fmt)
- self#pp_acsl_keyword "ghost";
- is_ghost <- true
- end;
- 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;
- end
- in
- (match all_annot with
- | [] -> pGhost fmt s
- | [ a ] when Cil.is_skip s.skind && not s.ghost ->
- Format.fprintf fmt "@[<hv>@[%t@ %a@;<1 1>%t@]@ %a@]"
- (fun fmt -> self#pp_open_annotation ~block:false fmt)
- self#code_annotation a
- (fun fmt -> self#pp_close_annotation ~block:false fmt)
- (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;
- pGhost fmt s)
+ 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;
Format.pp_close_box fmt ()
diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli
index 78de7bf360627e7a59de0c7a2c9d6143ee61b95c..a09665c4365ec4cbafc36db2060b72f955acb93d 100644
--- a/src/kernel_services/ast_printing/printer_api.mli
+++ b/src/kernel_services/ast_printing/printer_api.mli
@@ -78,6 +78,22 @@ class type extensible_printer_type = object
method private has_annot: bool
(** [true] if [current_stmt] has some annotations attached to it. *)
+ method private in_ghost_if_needed:
+ Format.formatter ->
+ bool ->
+ post_fmt:(((Format.formatter -> unit) -> unit, Format.formatter, unit) format) ->
+ ?block:bool ->
+ (unit -> unit)
+ -> unit
+ (** Open a ghost context if the the first [bool] is true and we are not
+ already in a ghost context. [post_fmt] is a format like ["%t"] and is used
+ to define the format at the end of the ghost context. [block] indicates
+ whether we should open a C block or not (defaults to [true]). The last
+ parameter is the function to be applied in the ghost context (generally
+ some AST element).
+
+ @since 19.0-Potassium+dev *)
+
method private current_stmt: stmt option
(** @return the [stmt] being printed *)
diff --git a/tests/pretty_printing/annotations.i b/tests/pretty_printing/annotations.i
new file mode 100644
index 0000000000000000000000000000000000000000..1d80a03ba031afea73f4f4f1b3e9d306078df4e5
--- /dev/null
+++ b/tests/pretty_printing/annotations.i
@@ -0,0 +1,113 @@
+/*@ axiomatic A {
+ predicate P(integer x) reads \nothing ;
+ }
+*/
+
+//@ ghost int global_decl ;
+//@ ghost int global_def = 42 ;
+
+/*@
+ requires P(x) && x > 0 ;
+ ensures P(x) ;
+*/
+void function_no_ghost(int x) {
+ int y = 0;
+
+ /*@ loop invariant 0 <= y <= x ;
+ loop assigns y ;
+ loop variant x - y ; */
+ while (y < x) {
+ /*@ assert y < x ; */
+ y++;
+ /*@ assert y <= x ; */
+ }
+
+ //@ assert y == x ;
+
+ /*@ requires y == x ;
+ assigns y ;
+ ensures y != x ;
+ */ {
+ y -- ;
+ y *= 2 ;
+ }
+
+ //@ requires y >= 0 ;
+ y /= y ;
+}
+
+/*@
+ requires P(x) && x > 0 ;
+ ensures P(x) ;
+*/
+void function_with_ghost(int x) {
+ //@ ghost int y = 0;
+
+ /*@ ghost
+ /@ loop invariant 0 <= y <= x ;
+ loop assigns y ;
+ loop variant x - y ; @/
+ while (y < x) {
+ /@ assert y < x ; @/
+ y++;
+ /@ assert y <= x ; @/
+ }
+ */
+
+ //@ assert y == x ;
+
+ /*@ ghost
+ /@ requires y == x ;
+ assigns y ;
+ ensures y != x ;
+ @/ {
+ y -- ;
+ y *= 2 ;
+ }
+ */
+
+ /*@ ghost
+ //@ requires y >= 0 ;
+ y /= y ;
+ */
+}
+
+/* @ ghost TODO: reactivate this test when ghost-functions are supported
+ /@
+ requires P(x) && x > 0 ;
+ ensures P(x) ;
+ @/
+ void ghost_function(int x) {
+ int y = 0;
+
+ /@ loop invariant 0 <= y <= x ;
+ loop assigns y ;
+ loop variant x - y ; @/
+ while (y < x) {
+ /@ assert y < x ; @/
+ y++;
+ /@ assert y <= x ; @/
+ }
+
+ /@ assert y == x ; @/
+
+ /@ requires y == x ;
+ assigns y ;
+ ensures y != x ;
+ @/ {
+ y -- ;
+ y *= 2 ;
+ }
+
+ //@ requires y >= 0 ;
+ y /= y ;
+}
+*/
+
+/* @ ghost TODO: reactivate this test when ghost-functions are supported
+ void function_declaration(int variable) ;
+*/
+
+void reference_function(void){
+ // @ ghost function_declaration(42) ;
+}
diff --git a/tests/pretty_printing/oracle/annotations.res.oracle b/tests/pretty_printing/oracle/annotations.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e0259ac8679d28eb2dc45f1e187766a9979c90c7
--- /dev/null
+++ b/tests/pretty_printing/oracle/annotations.res.oracle
@@ -0,0 +1,155 @@
+[kernel] Parsing tests/pretty_printing/annotations.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ axiomatic A {
+ predicate P(ℤ x)
+ reads \nothing;
+
+ }
+ */
+/*@ ghost int global_decl; */
+/*@ ghost int global_def = 42; */
+/*@ requires P(x) ∧ x > 0;
+ ensures P(\old(x)); */
+void function_no_ghost(int x)
+{
+ int y = 0;
+ /*@ loop invariant 0 ≤ y ≤ x;
+ loop assigns y;
+ loop variant x - y; */
+ while (y < x) {
+ /*@ assert y < x; */ ;
+ y ++;
+ /*@ assert y ≤ x; */ ;
+ }
+ /*@ assert y ≡ x; */ ;
+ /*@ requires y ≡ x;
+ ensures y ≢ x;
+ assigns y; */
+ {
+ y --;
+ y *= 2;
+ }
+ /*@ requires y ≥ 0; */
+ y /= y;
+ return;
+}
+
+/*@ requires P(x) ∧ x > 0;
+ ensures P(\old(x)); */
+void function_with_ghost(int x)
+{
+ /*@ ghost int y = 0; */
+ /*@ ghost
+ /@ loop invariant 0 ≤ y ≤ x;
+ loop assigns y;
+ loop variant x - y; @/
+ while (y < x) {
+ /@ assert y < x; @/
+ ;
+ y ++;
+ /@ assert y ≤ x; @/
+ ;
+ }
+ */
+ /*@ assert y ≡ x; */ ;
+ /*@ ghost
+ /@ requires y ≡ x;
+ ensures y ≢ x;
+ assigns y; @/
+ {
+ y --;
+ y *= 2;
+ }
+ */
+ /*@ ghost /@ requires y ≥ 0; @/
+ y /= y; */
+ return;
+}
+
+void reference_function(void)
+{
+ return;
+}
+
+
+[kernel] Parsing tests/pretty_printing/result/annotations.c (with preprocessing)
+[kernel] Parsing tests/pretty_printing/annotations.i (no preprocessing)
+[kernel] tests/pretty_printing/annotations.i:13: Warning:
+ def'n of func function_no_ghost at tests/pretty_printing/annotations.i:13 (sum 9297192) conflicts with the one at tests/pretty_printing/result/annotations.c:12 (sum 14988159); keeping the one at tests/pretty_printing/result/annotations.c:12.
+[kernel] tests/pretty_printing/annotations.i:43: Warning:
+ def'n of func function_with_ghost at tests/pretty_printing/annotations.i:43 (sum 9297192) conflicts with the one at tests/pretty_printing/result/annotations.c:38 (sum 14988159); keeping the one at tests/pretty_printing/result/annotations.c:38.
+[kernel] tests/pretty_printing/annotations.i:111: Warning:
+ dropping duplicate def'n of func reference_function at tests/pretty_printing/annotations.i:111 in favor of that at tests/pretty_printing/result/annotations.c:68
+/* Generated by Frama-C */
+/*@ axiomatic A {
+ predicate P(ℤ x)
+ reads \nothing;
+
+ }
+ */
+/*@ ghost int global_decl; */
+/*@ ghost int global_def = 42; */
+/*@ requires P(x) ∧ x > 0;
+ ensures P(\old(x)); */
+void function_no_ghost(int x)
+{
+ int y = 0;
+ /*@ loop invariant 0 ≤ y ≤ x;
+ loop assigns y;
+ loop variant x - y; */
+ while (y < x) {
+ /*@ assert y < x; */ ;
+ y ++;
+ /*@ assert y ≤ x; */ ;
+ }
+ /*@ assert y ≡ x; */ ;
+ /*@ requires y ≡ x;
+ ensures y ≢ x;
+ assigns y; */
+ {
+ y --;
+ y *= 2;
+ }
+ /*@ requires y ≥ 0; */
+ y /= y;
+ return;
+}
+
+/*@ requires P(x) ∧ x > 0;
+ ensures P(\old(x)); */
+void function_with_ghost(int x)
+{
+ /*@ ghost int y = 0; */
+ /*@ ghost
+ /@ loop invariant 0 ≤ y ≤ x;
+ loop assigns y;
+ loop variant x - y; @/
+ while (y < x) {
+ /@ assert y < x; @/
+ ;
+ y ++;
+ /@ assert y ≤ x; @/
+ ;
+ }
+ */
+ /*@ assert y ≡ x; */ ;
+ /*@ ghost
+ /@ requires y ≡ x;
+ ensures y ≢ x;
+ assigns y; @/
+ {
+ y --;
+ y *= 2;
+ }
+ */
+ /*@ ghost /@ requires y ≥ 0; @/
+ y /= y; */
+ return;
+}
+
+void reference_function(void)
+{
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/ghost_multiline_annot.0.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.0.res.oracle
index a1b72856b21cf5e086a4bc325f794e87dcaf34cd..c8071303034a8e9a29cd54bb895f61696618c9ae 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.0.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.0.res.oracle
@@ -3,12 +3,14 @@
int main(int c)
{
int __retres;
- /*@ requires c ≥ 0; */
- /*@ ghost int x = c; */
- /*@ loop invariant x ≥ 0;
- loop assigns x;
- loop variant x; */
- /*@ ghost while (x > 0) x --; */
+ /*@ ghost /@ requires c ≥ 0; @/
+ int x = c; */
+ /*@ ghost
+ /@ loop invariant x ≥ 0;
+ loop assigns x;
+ loop variant x; @/
+ while (x > 0) x --;
+ */
__retres = 0;
return __retres;
}
diff --git a/tests/syntax/oracle/ghost_multiline_annot.6.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.6.res.oracle
index 2a924d8ae0eb5823a84bdd5b62cc660f80758220..a7859b320dda126c06a33ce03c652e7f6000b888 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.6.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.6.res.oracle
@@ -4,9 +4,10 @@ int main(void)
{
int __retres;
/*@ ghost int x = 10; */
- /*@ loop invariant x ≥ 0;
- loop variant x; */
- /*@ ghost while (x > 0) x --; */
+ /*@ ghost /@ loop invariant x ≥ 0;
+ loop variant x; @/
+ while (x > 0) x --;
+ */
__retres = 0;
return __retres;
}
diff --git a/tests/syntax/oracle/ghost_multiline_annot.7.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.7.res.oracle
index 2019d87badcbe58ff2104e81b12fbf70dae540c7..6ee6fd7133f935cf8d4e05201fd1e2d8abba1d69 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.7.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.7.res.oracle
@@ -3,12 +3,14 @@
int main(int c)
{
int __retres;
- /*@ requires c ≥ 0; */
- /*@ ghost int x = c; */
- /*@ loop invariant x ≥ 0;
- loop invariant x ≡ x;
- loop variant x; */
- /*@ ghost while (x > 0) x --; */
+ /*@ ghost /@ requires c ≥ 0; @/
+ int x = c; */
+ /*@ ghost
+ /@ loop invariant x ≥ 0;
+ loop invariant x ≡ x;
+ loop variant x; @/
+ while (x > 0) x --;
+ */
__retres = 0;
return __retres;
}
diff --git a/tests/syntax/oracle/ghost_multiline_annot.8.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.8.res.oracle
index 2019d87badcbe58ff2104e81b12fbf70dae540c7..6ee6fd7133f935cf8d4e05201fd1e2d8abba1d69 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.8.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.8.res.oracle
@@ -3,12 +3,14 @@
int main(int c)
{
int __retres;
- /*@ requires c ≥ 0; */
- /*@ ghost int x = c; */
- /*@ loop invariant x ≥ 0;
- loop invariant x ≡ x;
- loop variant x; */
- /*@ ghost while (x > 0) x --; */
+ /*@ ghost /@ requires c ≥ 0; @/
+ int x = c; */
+ /*@ ghost
+ /@ loop invariant x ≥ 0;
+ loop invariant x ≡ x;
+ loop variant x; @/
+ while (x > 0) x --;
+ */
__retres = 0;
return __retres;
}