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.

Author: tautschnig

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())

src/goto-programs/builtin_functions.cpp

@@ -1389,6 +1389,38 @@ void goto_convertt::do_function_call_symbol(
 
     copy(function_call, FUNCTION_CALL, dest);
   }
+  else if(identifier == "alloca" || identifier == "__builtin_alloca")
+  {
+    if(lhs.is_nil())
+    {
+      // this will trigger a recursive call
+      side_effect_expr_function_callt call{
+        function, arguments, function.type(), function.source_location()};
+      make_temp_symbol(call, "alloca", dest, mode);
+    }
+    else
+    {
+      code_function_callt function_call(lhs, function, arguments);
+      function_call.add_source_location() = function.source_location();
+      copy(function_call, FUNCTION_CALL, dest);
+
+      exprt new_lhs = lhs;
+      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(), function.source_location()},
+        std::move(alloca_result),
+        dead_object_sym};
+      code_assignt assign{std::move(dead_object_sym), std::move(rhs)};
+      assign.add_source_location() = function.source_location();
+      targets.destructor_stack.add(assign);
+    }
+  }
   else
   {
     do_function_call_symbol(*symbol);