Detect use of alloca-allocated object after leaving its scope

alloca-allocated objects need no longer be usable outside their scope.
Detect such use by non-deterministically setting __CPROVER_dead_object
to return_value___builtin_alloca.

This fixes the verification result for SV-COMP's
memsafety-ext3/getNumbers1-1.c.

Author: tautschnig

regression/cbmc-library/alloca-02/main.c

@@ -0,0 +1,19 @@
+#include <stdlib.h>
+
+#ifdef _WIN32
+void *alloca(size_t alloca_size);
+#endif
+
+int *foo()
+{
+  int *foo_ptr = alloca(sizeof(int));
+  return foo_ptr;
+}
+
+int main()
+{
+  int *from_foo = foo();
+  *from_foo = 42; // access to object that has gone out of scope
+
+  return 0;
+}

regression/cbmc-library/alloca-02/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+dereference failure: dead object in \*from_foo: FAILURE$
+^\*\* 1 of 6 failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -2110,6 +2110,28 @@ void goto_checkt::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())