From 24b5580bfa1b1f0300074c4b1b74d344f6d315a7 Mon Sep 17 00:00:00 2001
From: Benjamin Jorge <benjamin.jorge@cea.fr>
Date: Thu, 26 Sep 2024 15:02:02 +0200
Subject: [PATCH] [kernel] fix pretty printing of assigns-from clauses
---
src/kernel_services/ast_printing/cil_printer.ml | 10 ++--------
src/plugins/e-acsl/tests/libc/oracle/gen_str.c | 16 ++++++++--------
.../oracle/issue-1373-ranges.res.oracle | 16 +++++++---------
3 files changed, 17 insertions(+), 25 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 783dad28f08..83029572c91 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3077,18 +3077,12 @@ class cil_printer () = object (self)
method from kw fmt (base,deps) = match deps with
| FromAny -> ()
- | From [] ->
- fprintf fmt "@[<hv 2>@[<h>%a@ %a@]@ @[<h>%a %a@];@]"
- self#pp_acsl_keyword kw
- self#identified_term base
- self#pp_acsl_keyword "\\from"
- self#pp_acsl_keyword "\\nothing"
| From l ->
- fprintf fmt "@[<hv 2>@[%a@ %a@]@ @[<h>%a %a@];@]"
+ fprintf fmt "@[<hv 2>@[<h>%a@ %a@]@ @[<h>%a %a@];@]"
self#pp_acsl_keyword kw
self#identified_term base
self#pp_acsl_keyword "\\from"
- (Pretty_utils.pp_list ~sep:",@ " self#identified_term) l
+ (Pretty_utils.pp_list ~sep:",@ " ~empty:"\\nothing" self#identified_term) l
(* not enclosed in a box *)
method private terminates_decreases ~extra_nl nl fmt (terminates, variant) =
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
index 2c95285a9e9..e41ebd61ec3 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
@@ -65,8 +65,8 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
assigns *(dest +
(strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
\result;
- assigns
- *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
+ assigns *(dest +
+ (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
\from *(src + (0 .. strlen{Old}(src)));
assigns \result \from dest;
*/
@@ -96,8 +96,8 @@ char *__gen_e_acsl_strcat(char * restrict dest, char const * restrict src);
assigns *(dest +
(strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
\result;
- assigns
- *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
+ assigns *(dest +
+ (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
\from *(src + (0 .. strlen{Old}(src) - 1));
assigns \result \from dest;
@@ -143,8 +143,8 @@ char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
assigns *(dest +
(strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
\result;
- assigns
- *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
+ assigns *(dest +
+ (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
\from *(src + (0 .. strlen{Old}(src) - 1));
assigns \result \from dest;
@@ -273,8 +273,8 @@ char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
assigns *(dest +
(strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
\result;
- assigns
- *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
+ assigns *(dest +
+ (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
\from *(src + (0 .. strlen{Old}(src)));
assigns \result \from dest;
*/
diff --git a/tests/pretty_printing/oracle/issue-1373-ranges.res.oracle b/tests/pretty_printing/oracle/issue-1373-ranges.res.oracle
index b5403f21838..2e4801305e5 100644
--- a/tests/pretty_printing/oracle/issue-1373-ranges.res.oracle
+++ b/tests/pretty_printing/oracle/issue-1373-ranges.res.oracle
@@ -8,10 +8,9 @@ int const bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb = 3;
/*@ assigns x->bar[name_range1:
(aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb)];
- assigns
- x->bar[name_range1:
- (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
- bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb)]
+ assigns x->bar[name_range1:
+ (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
+ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb)]
\from x->bar[aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb];
*/
@@ -29,7 +28,7 @@ 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: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.
+ def'n of func main at issue-1373-ranges.i:16 (sum 2855) conflicts with the one at ocode_issue-1373-ranges.c:18 (sum 4629); keeping the one at ocode_issue-1373-ranges.c:18.
/* Generated by Frama-C */
struct foo {
char bar[4] ;
@@ -39,10 +38,9 @@ int const bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb = 3;
/*@ assigns x->bar[name_range1:
(aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb)];
- assigns
- x->bar[name_range1:
- (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
- bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb)]
+ assigns x->bar[name_range1:
+ (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
+ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb)]
\from x->bar[aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ..
bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb];
*/
--
GitLab