From 64d8732dda6f02c83efda7e3e1d4a8f8e905c21d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 9 Dec 2025 11:35:13 +0000
Subject: [PATCH] Fix builtin function return hidden flag inconsistency

Function returns for built-in functions now correctly match their
function call hidden flag. This is done by symex storing the combined
hidden flag in call frame.

Co-authored-by: Kiro autonomous agent

Fixes: #5207
---
 regression/cbmc/builtin-function-hidden-flag/test.c    |  8 ++++++++
 regression/cbmc/builtin-function-hidden-flag/test.desc | 10 ++++++++++
 .../cbmc/builtin-function-hidden-flag/test_xml.desc    | 10 ++++++++++
 src/goto-symex/symex_function_call.cpp                 |  2 +-
 4 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/builtin-function-hidden-flag/test.c
 create mode 100644 regression/cbmc/builtin-function-hidden-flag/test.desc
 create mode 100644 regression/cbmc/builtin-function-hidden-flag/test_xml.desc

diff --git a/regression/cbmc/builtin-function-hidden-flag/test.c b/regression/cbmc/builtin-function-hidden-flag/test.c
new file mode 100644
index 00000000000..a2b2318d9b3
--- /dev/null
+++ b/regression/cbmc/builtin-function-hidden-flag/test.c
@@ -0,0 +1,8 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  char *x = malloc(1);
+  assert(0);
+}
diff --git a/regression/cbmc/builtin-function-hidden-flag/test.desc b/regression/cbmc/builtin-function-hidden-flag/test.desc
new file mode 100644
index 00000000000..68ce3d985e2
--- /dev/null
+++ b/regression/cbmc/builtin-function-hidden-flag/test.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+--json-ui
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+"function": \{[^}]*"displayName": "malloc",[^}]*"sourceLocation": \{[^}]*\}[^}]*\}[^}]*"hidden": false[^}]*"sourceLocation": \{[^}]*\}[^}]*"stepType": "function-call"
+"function": \{[^}]*"displayName": "malloc",[^}]*"sourceLocation": \{[^}]*\}[^}]*\}[^}]*"hidden": false[^}]*"sourceLocation": \{[^}]*\}[^}]*"stepType": "function-return"
+--
+^warning: ignoring
diff --git a/regression/cbmc/builtin-function-hidden-flag/test_xml.desc b/regression/cbmc/builtin-function-hidden-flag/test_xml.desc
new file mode 100644
index 00000000000..600860a49ec
--- /dev/null
+++ b/regression/cbmc/builtin-function-hidden-flag/test_xml.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+--xml-ui
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+<function_call hidden="false" step_nr="\d+" thread="0">\n\s*<function display_name="malloc" identifier="malloc"
+<function_return hidden="false" step_nr="\d+" thread="0">\n\s*<function display_name="malloc" identifier="malloc"
+--
+^warning: ignoring
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index db4bfa133bc..492fb1f7413 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -344,7 +344,7 @@ void goto_symext::symex_function_call_post_clean(
   frame.call_lhs = cleaned_lhs;
   frame.end_of_function = --goto_function.body.instructions.end();
   frame.function_identifier=identifier;
-  frame.hidden_function = goto_function.is_hidden();
+  frame.hidden_function = hidden;
 
   // set up the 'return value symbol' when needed
   if(frame.call_lhs.is_not_nil())