diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 186378fef09557dd2143da21ed5e62fcb70a6ecc..e1642d5c48bad2da4a98d431f042f9581e4c7d31 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 4d5ac4535168bb6f0b25f30b22412d0c028fc525..49074590ec4ff2071112e1ba7cdd78a2ff5f864e 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 f8121ed36ebd8d25b30cf878152eb8e39f44eccf..132d1bef54df6c456d61b9acf25df882c73a6d48 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