max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/compiler/ir_interpreter): fix UB sequencing found by GCC

Browse source
This commit is contained in:
Sebastian Ullrich 2019-09-16 17:33:14 +02:00
parent 75e5f5bfd8
commit a083cab532
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/compiler/ir_interpreter.cpp
View file

@ -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() << " = ";