From ac4373cce47479dc97ec0021e9932bebb3a30cb6 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 26 Mar 2020 14:40:54 +0100
Subject: [PATCH] [printer] special treatment for __fc_sig_* following their
new declaration
---
src/kernel_services/ast_printing/cil_printer.ml | 7 +++++++
tests/value/oracle/invalid_pointer.0.res.oracle | 2 +-
tests/value/oracle/invalid_pointer.1.res.oracle | 2 +-
3 files changed, 9 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 186378fef09..e1642d5c48b 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -54,6 +54,10 @@ module Extensions = struct
end
let set_extension_handler = Extensions.set_handler
+(* for specific builtin functions that act as placeholder for C macros.
+ For each name f below, pretty-printer will replace f and &f with the
+ corresponding name. Be sure to keep the list in sync with share/libc.
+*)
let rename_builtins = Datatype.String.Hashtbl.create 17
let () =
@@ -781,6 +785,9 @@ class cil_printer () = object (self)
Neither cookie nor keyword for you. *)
| AlignOf t -> fprintf fmt "__alignof__(%a)" (self#typ None) t
| AlignOfE e -> fprintf fmt "__alignof__(%a)" self#exp_non_decay e
+ | AddrOf ((Var v, NoOffset))
+ when Datatype.String.Hashtbl.mem rename_builtins v.vname ->
+ self#varinfo fmt v
| AddrOf lv -> fprintf fmt "& %a" (self#lval_prec Precedence.addrOfLevel) lv
| StartOf(lv) ->
if state.print_cil_as_is || non_decay then
diff --git a/tests/value/oracle/invalid_pointer.0.res.oracle b/tests/value/oracle/invalid_pointer.0.res.oracle
index 4d5ac453516..49074590ec4 100644
--- a/tests/value/oracle/invalid_pointer.0.res.oracle
+++ b/tests/value/oracle/invalid_pointer.0.res.oracle
@@ -420,4 +420,4 @@
[inout] Out (internal) for function main:
Frama_C_entropy_source
[inout] Inputs for function main:
- Frama_C_entropy_source; SIG_DFL; SIG_IGN; SIG_ERR; undet
+ Frama_C_entropy_source; undet
diff --git a/tests/value/oracle/invalid_pointer.1.res.oracle b/tests/value/oracle/invalid_pointer.1.res.oracle
index f8121ed36eb..132d1bef54d 100644
--- a/tests/value/oracle/invalid_pointer.1.res.oracle
+++ b/tests/value/oracle/invalid_pointer.1.res.oracle
@@ -348,4 +348,4 @@
[inout] Out (internal) for function main:
Frama_C_entropy_source
[inout] Inputs for function main:
- Frama_C_entropy_source; SIG_DFL; SIG_IGN; SIG_ERR; undet
+ Frama_C_entropy_source; undet
--
GitLab