From a083cab5327accfd8bbde7eea02876983361a7f4 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 16 Sep 2019 17:33:14 +0200
Subject: [PATCH] fix(library/compiler/ir_interpreter): fix UB sequencing found
 by GCC

---
 src/library/compiler/ir_interpreter.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp
index dc432956eb..2ba7549589 100644
--- a/src/library/compiler/ir_interpreter.cpp
+++ b/src/library/compiler/ir_interpreter.cpp
@@ -473,7 +473,10 @@ class interpreter {
                         check_system("interpreter");
                         break;
                     }
-                    var(fn_body_vdecl_var(b)) = eval_expr(fn_body_vdecl_expr(b), fn_body_vdecl_type(b));
+                    value v = eval_expr(fn_body_vdecl_expr(b), fn_body_vdecl_type(b));
+                    // NOTE: `var` must be called *after* `eval_expr` because the stack may get resized and invalidate
+                    // the pointer
+                    var(fn_body_vdecl_var(b)) = v;
                     DEBUG_CODE(lean_trace(name({"interpreter", "step"}),
                                           tout() << std::string(m_call_stack.size(), ' ') << "=> x_";
                                           tout() << fn_body_vdecl_var(b).get_small_value() << " = ";