From 398b8187e09d31bdc7224a098126057bf1514944 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 25 Apr 2019 16:26:56 +0200
Subject: [PATCH] [printer] fixes pretty-printing of unions
---
src/kernel_services/ast_printing/cil_printer.ml | 8 ++++++--
tests/libc/oracle/fc_libc.1.res.oracle | 4 ++--
2 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 897febf6911..453741922dd 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -386,6 +386,11 @@ let remove_no_op_coerce t =
| TLogic_coerce (ty,t) when Cil.no_op_coerce ty t -> t
| _ -> t
+let rec is_singleton t =
+ match t.term_node with
+ | TLogic_coerce(Ltype ({ lt_name = "set"},_), t') -> is_singleton t'
+ | _ -> not (Logic_const.is_set_type t.term_type)
+
(* when pretty-printing relation chains, a < b && b' < c, it can happen that
b has a coercion and b' hasn't or vice-versa (bc c is an integer and a and
b are ints for instance). We nevertheless want to
@@ -2340,8 +2345,7 @@ class cil_printer () = object (self)
| Ttype ty ->
fprintf fmt "%a(%a)" self#pp_acsl_keyword "\\type" (self#typ None) ty
| Tunion l
- when ((List.for_all (fun t -> not(Logic_const.is_set_type t.term_type)) l)
- && (not state.print_cil_as_is)) ->
+ when (List.for_all is_singleton l) && (not state.print_cil_as_is) ->
fprintf fmt "{%a}" (Pretty_utils.pp_list ~sep:",@ " self#term) l
| Tunion locs ->
fprintf fmt "@[<hov 2>%a(@,%a)@]"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 4202b6e1aa9..1aff0685633 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -6893,7 +6893,7 @@ char *__fc_p_basename = __fc_basename;
null_or_valid_string_path: path ≡ \null ∨ valid_read_string(path);
ensures
result_points_to_internal_storage_or_path:
- \subset(\result, \union(__fc_p_basename, \old(path)));
+ \subset(\result, {__fc_p_basename, \old(path)});
assigns *(path + (0 ..)), __fc_basename[0 ..], \result;
assigns *(path + (0 ..)) \from *(path + (0 ..)), __fc_basename[0 ..];
assigns __fc_basename[0 ..] \from *(path + (0 ..)), __fc_basename[0 ..];
@@ -6908,7 +6908,7 @@ char *__fc_p_dirname = __fc_dirname;
null_or_valid_string_path: path ≡ \null ∨ valid_read_string(path);
ensures
result_points_to_internal_storage_or_path:
- \subset(\result, \union(__fc_p_dirname, \old(path)));
+ \subset(\result, {__fc_p_dirname, \old(path)});
assigns *(path + (0 ..)), __fc_dirname[0 ..], \result;
assigns *(path + (0 ..)) \from *(path + (0 ..)), __fc_dirname[0 ..];
assigns __fc_dirname[0 ..] \from *(path + (0 ..)), __fc_dirname[0 ..];
--
GitLab