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"
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);