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

fix(library/vm/vm): problems detected when using valgrind

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-03 16:55:01 -07:00
parent 163a650ede
commit b5ca231cdf
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/vm/vm.cpp
View file

@ -317,6 +317,7 @@ vm_instr mk_cases2_instr(unsigned pc1, unsigned pc2) {
vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs) {
lean_assert(num_pc >= 2);
vm_instr r(opcode::CasesN);
r.m_cases_idx = 0; /* not really needed, but it avoids a valgrind warning. */
r.m_npcs = new unsigned[num_pc + 1];
r.m_npcs[0] = num_pc;
for (unsigned i = 0; i < num_pc; i++)
@ -384,7 +385,7 @@ void vm_instr::copy_args(vm_instr const & i) {
case opcode::CasesN:
case opcode::BuiltinCases:
m_npcs = new unsigned[i.m_npcs[0] + 1];
for (unsigned j = 0; j < m_npcs[0] + 1; j++)
for (unsigned j = 0; j < i.m_npcs[0] + 1; j++)
m_npcs[j] = i.m_npcs[j];
m_cases_idx = i.m_cases_idx;
break;