From 28c4f7bf9db8d0a1a823096d2a76a23f16131b32 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 22 Mar 2022 21:59:47 +0000
Subject: [PATCH 1/2] Fix cbmc-library CMake test configuration

The multi-argument specification is to be used with add_test_pl_profile,
not add_test_pl_tests. Also, remove the spurious first argument that
resulted in 0 tests being found.
---
 regression/cbmc-library/CMakeLists.txt | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/regression/cbmc-library/CMakeLists.txt b/regression/cbmc-library/CMakeLists.txt
index 9728b73e7aa..38b16fd56ab 100644
--- a/regression/cbmc-library/CMakeLists.txt
+++ b/regression/cbmc-library/CMakeLists.txt
@@ -3,8 +3,7 @@ add_test_pl_tests(
     "$<TARGET_FILE:cbmc>"
 )
 else()
-add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>"
+add_test_pl_profile(
     "cbmc-library"
     "$<TARGET_FILE:cbmc>"
     "-C;-X;unix"

From da65bceb7ed4e372f7d1ba5caaf53b8a1e658eaf Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 21 Mar 2022 21:35:24 +0000
Subject: [PATCH 2/2] Lift alloca's deallocation behaviour out of goto_check_ct

alloca always results in deallocation taking place, and not just when
pointer checks are enabled.
---
 regression/cbmc-library/alloca-01/main.c |  1 +
 src/ansi-c/goto_check_c.cpp              | 22 -------------
 src/goto-programs/builtin_functions.cpp  | 40 ++++++++++++++++++++++++
 3 files changed, 41 insertions(+), 22 deletions(-)

diff --git a/regression/cbmc-library/alloca-01/main.c b/regression/cbmc-library/alloca-01/main.c
index 014bf955d14..c8610c6a56b 100644
--- a/regression/cbmc-library/alloca-01/main.c
+++ b/regression/cbmc-library/alloca-01/main.c
@@ -9,4 +9,5 @@ int main()
   int *p = alloca(sizeof(int));
   *p = 42;
   free(p);
+  (void)alloca(sizeof(int)); // useless, but result still needs to be released
 }
diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp
index 28242fd658d..ebec548c21f 100644
--- a/src/ansi-c/goto_check_c.cpp
+++ b/src/ansi-c/goto_check_c.cpp
@@ -2188,28 +2188,6 @@ void goto_check_ct::goto_check(
               std::move(lhs), std::move(rhs), i.source_location()));
           t->code_nonconst().add_source_location() = i.source_location();
         }
-
-        if(
-          variable.type().id() == ID_pointer &&
-          function_identifier != "alloca" &&
-          (ns.lookup(variable.get_identifier()).base_name ==
-             "return_value___builtin_alloca" ||
-           ns.lookup(variable.get_identifier()).base_name ==
-             "return_value_alloca"))
-        {
-          // mark pointer to alloca result as dead
-          exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
-          exprt alloca_result =
-            typecast_exprt::conditional_cast(variable, lhs.type());
-          if_exprt rhs(
-            side_effect_expr_nondett(bool_typet(), i.source_location()),
-            std::move(alloca_result),
-            lhs);
-          goto_programt::targett t =
-            new_code.add(goto_programt::make_assignment(
-              std::move(lhs), std::move(rhs), i.source_location()));
-          t->code_nonconst().add_source_location() = i.source_location();
-        }
       }
     }
     else if(i.is_end_function())
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index a154338c099..6847ab93345 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -1389,6 +1389,46 @@ void goto_convertt::do_function_call_symbol(
 
     copy(function_call, FUNCTION_CALL, dest);
   }
+  else if(
+    (identifier == "alloca" || identifier == "__builtin_alloca") &&
+    function.source_location().get_function() != "alloca")
+  {
+    const source_locationt &source_location = function.source_location();
+    exprt new_lhs = lhs;
+
+    if(lhs.is_nil())
+    {
+      new_lhs = new_tmp_symbol(
+                  to_code_type(function.type()).return_type(),
+                  "alloca",
+                  dest,
+                  source_location,
+                  mode)
+                  .symbol_expr();
+    }
+
+    code_function_callt function_call(new_lhs, function, arguments);
+    function_call.add_source_location() = source_location;
+    copy(function_call, FUNCTION_CALL, dest);
+
+    // create a backup copy to ensure that no assignments to the pointer affect
+    // the destructor code that will execute eventually
+    if(!lhs.is_nil())
+      make_temp_symbol(new_lhs, "alloca", dest, mode);
+
+    // mark pointer to alloca result as dead
+    symbol_exprt dead_object_sym =
+      ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+    exprt alloca_result =
+      typecast_exprt::conditional_cast(new_lhs, dead_object_sym.type());
+    if_exprt rhs{
+      side_effect_expr_nondett{bool_typet(), source_location},
+      std::move(alloca_result),
+      dead_object_sym};
+    code_assignt assign{
+      std::move(dead_object_sym), std::move(rhs), source_location};
+    targets.destructor_stack.add(assign);
+  }
   else
   {
     do_function_call_symbol(*symbol);