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

fix(library/vm/vm): handle InvokeJP at pc manipulation methods

Browse source
This commit is contained in:
Leonardo de Moura 2018-11-01 16:01:36 -07:00
parent e11fe27de2
commit adff01bba4
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -577,6 +577,8 @@ unsigned vm_instr::get_num_pcs() const {
return 2;
case opcode::CasesN:
return get_casesn_size();
case opcode::InvokeJP:
return 1;
default:
return 0;
}
@ -590,6 +592,8 @@ unsigned vm_instr::get_pc(unsigned i) const {
return m_pc[i];
case opcode::CasesN:
return get_casesn_pc(i);
case opcode::InvokeJP:
return m_jp_pc;
default:
lean_unreachable();
}
@ -605,6 +609,9 @@ void vm_instr::set_pc(unsigned i, unsigned pc) {
case opcode::CasesN:
set_casesn_pc(i, pc);
break;
case opcode::InvokeJP:
m_jp_pc = pc;
break;
default:
lean_unreachable();
}