diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index 783dad28f08bafc654b9b847330959e21c3eb1a1..83029572c913384b6d9f5e446b72c497bccf2f9d 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 2c95285a9e9a2b94308334229801130e12d514ce..e41ebd61ec3c6acf70f8a66e6dde2be3f68edbfb 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 b5403f2183884c6101e576123335f5f26b329855..2e4801305e563ff079e93b5bf73bd3b3e31a5341 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]; */