diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index dfb0da0f6aefeae4232807624a2523d3bcdf7545..36f2ac6ea004346ac37243309697462cfb26d2c9 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2437,7 +2437,7 @@ class cil_printer () = object (self)
begin match t.term_name with
| [] -> self#term_node fmt t
| _ :: _ ->
- fprintf fmt "(@[%a:@ %a@])"
+ fprintf fmt "(@[<2>%a:@ %a@])"
(Pretty_utils.pp_list ~sep:":@ " self#name) t.term_name
self#term_node t
end;
@@ -2519,10 +2519,11 @@ class cil_printer () = object (self)
self#tand_list l
method private range fmt (low, high) =
+ let pp_opt = Pretty_utils.pp_opt ~pre:"" ~suf:"" in
fprintf fmt "@[%a..%a@]"
- (Pretty_utils.pp_opt
+ (pp_opt
(fun fmt v -> Format.fprintf fmt "%a " (self#term_prec Precedence.upperLevel) v)) low
- (Pretty_utils.pp_opt
+ (pp_opt
(fun fmt v -> Format.fprintf fmt "@ %a" (self#term_prec Precedence.upperLevel) v)) high;
method term_node fmt t =
@@ -2709,7 +2710,7 @@ class cil_printer () = object (self)
match term_name with
| [] -> self#range fmt (low, high)
| _ :: _ ->
- fprintf fmt "@[%a:@ (%a)@]"
+ fprintf fmt "@[<2>%a:@ (%a)@]"
(Pretty_utils.pp_list ~sep:":@ " self#name) term_name
self#range (low, high)
in
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
index 222b73c887b5894b5baca53f33eb78a6bea39295..fdcbf846d8ca558a43f2473c229991bd095d249f 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -16647,7 +16647,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) +\n strlen{Old}(src))) in function strcat."
+ "text": "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) + strlen{Old}(src))) in function strcat."
},
"locations": [
{
@@ -19566,7 +19566,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) +\n strlen{Old}(src))) in function strncat."
+ "text": "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) + strlen{Old}(src))) in function strncat."
},
"locations": [
{
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
index 65daf9d5b7433eff95d480d35ff225b157fbf4e0..49eef37ea69e3e7f40f200e22276de5ad597a508 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
@@ -3316,7 +3316,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) +\n strlen{Old}(src))) in function strcat."
+ "text": "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) + strlen{Old}(src))) in function strcat."
},
"locations": [
{
@@ -6001,7 +6001,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) +\n strlen{Old}(src))) in function strncat."
+ "text": "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) + strlen{Old}(src))) in function strncat."
},
"locations": [
{
diff --git a/tests/pretty_printing/issue-1373-ranges.i b/tests/pretty_printing/issue-1373-ranges.i
index 8e7323f7dc8fbd7de95d8c00cea470fe8ebba7d7..5968215077321150c9835ff8665d85275097d12e 100644
--- a/tests/pretty_printing/issue-1373-ranges.i
+++ b/tests/pretty_printing/issue-1373-ranges.i
@@ -4,7 +4,13 @@
struct foo { char bar[4]; };
-/*@ assigns x->bar[name_range1:(0..3)] \from x->bar[0..3]; */
+// Long names to check Format indentation
+int const aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa = 0;
+int const bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb = 3;
+
+/*@ assigns x->bar[name_range1:(aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa..bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb)]
+ \from x->bar[aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa..bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb];
+*/
int f(struct foo* x);
void main() {
diff --git a/tests/pretty_printing/oracle/issue-1373-ranges.res.oracle b/tests/pretty_printing/oracle/issue-1373-ranges.res.oracle
index 117e8217380d4f3a8310fa5e709646b472260774..b5403f2183884c6101e576123335f5f26b329855 100644
--- a/tests/pretty_printing/oracle/issue-1373-ranges.res.oracle
+++ b/tests/pretty_printing/oracle/issue-1373-ranges.res.oracle
@@ -3,8 +3,17 @@
struct foo {
char bar[4] ;
};
-/*@ assigns x->bar[name_range1: (0 .. 3)];
- assigns x->bar[name_range1: (0 .. 3)] \from x->bar[0 .. 3];
+int const aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa = 0;
+int const bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb = 3;
+/*@ assigns x->bar[name_range1:
+ (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
+ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb)];
+ assigns
+ x->bar[name_range1:
+ (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
+ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb)]
+ \from x->bar[aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
+ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb];
*/
int f(struct foo *x);
@@ -19,14 +28,23 @@ void main(void)
[kernel] Parsing ocode_issue-1373-ranges.c (with preprocessing)
[kernel] Parsing issue-1373-ranges.i (no preprocessing)
-[kernel] issue-1373-ranges.i:10: Warning:
- def'n of func main at issue-1373-ranges.i:10 (sum 2855) conflicts with the one at ocode_issue-1373-ranges.c:10 (sum 4629); keeping the one at ocode_issue-1373-ranges.c:10.
+[kernel] issue-1373-ranges.i:16: Warning:
+ def'n of func main at issue-1373-ranges.i:16 (sum 2855) conflicts with the one at ocode_issue-1373-ranges.c:19 (sum 4629); keeping the one at ocode_issue-1373-ranges.c:19.
/* Generated by Frama-C */
struct foo {
char bar[4] ;
};
-/*@ assigns x->bar[name_range1: (0 .. 3)];
- assigns x->bar[name_range1: (0 .. 3)] \from x->bar[0 .. 3];
+int const aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa = 0;
+int const bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb = 3;
+/*@ assigns x->bar[name_range1:
+ (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
+ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb)];
+ assigns
+ x->bar[name_range1:
+ (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
+ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb)]
+ \from x->bar[aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
+ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb];
*/
int f(struct foo *x);