End-to-End Translation Validation is the problem of verifying the executable code generated by a compiler against the corresponding input source code for a single compilation. This becomes particularly hard in the presence of dynamically allocated local memory: in the context of a C procedure, local memory may be allocated due to constant-length local arrays, address-taken local variables, address-taken formal parameters, variable-length local arrays, procedure-call arguments (including variadic arguments), and the alloca() operator. We provide an execution model and an associated algorithm to soundly convert this complex verification task into first-order logic queries that an off-the-shelf SMT solver can handle efficiently. In our experiments, we perform blackbox translation validation of C programs, involving these local memory allocation constructs, against their corresponding assembly implementations generated by an optimizing compiler. We demonstrate that our algorithm can automatically search for an equivalence proof for procedure pairs containing dynamic local memory (de)allocations with 100+ source lines of code and 200+ assembly instructions, in the presence of complex loop and vectorizing transformations, within a resource budget of eight CPU-hours.