From c6fcb0254f3a9e4de2bd24f0e01f7e98dcf61890 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 19 Feb 2024 15:07:00 +0000 Subject: [PATCH] Deprecate namespacet::follow Follows struct and union tags, but does not follow enum tags. This is not obvious from its documentation, and led to surprising behaviour as seen (and fixed) in https://github.com/diffblue/cbmc/pull/8203. Using suitable variants of `follow_tag` is safer. --- src/util/namespace.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/util/namespace.h b/src/util/namespace.h index 34cf6a2d964..8328e1b815c 100644 --- a/src/util/namespace.h +++ b/src/util/namespace.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_NAMESPACE_H #define CPROVER_UTIL_NAMESPACE_H +#include "deprecate.h" #include "invariant.h" #include "irep.h" @@ -58,6 +59,7 @@ class namespace_baset virtual ~namespace_baset(); void follow_macros(exprt &) const; + DEPRECATED(SINCE(2024, 2, 19, "use follow_tag(...) instead")) const typet &follow(const typet &) const; // These produce union_typet, struct_typet, c_enum_typet or