michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/blast): uninitialized variables

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-18 18:56:19 -08:00
parent fbeee674b3
commit d85e26898e
3 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/blast/choice_point.h
View file

@ -20,6 +20,7 @@ class choice_point_cell {
MK_LEAN_RC(); // Declare m_rc counter MK_LEAN_RC(); // Declare m_rc counter
void dealloc() { delete this; } void dealloc() { delete this; }
public: public:
choice_point_cell():m_rc(0) {}
virtual ~choice_point_cell() {} virtual ~choice_point_cell() {}
/** \brief Update next proof state. This method may /** \brief Update next proof state. This method may
perform destructive updates, choice points are not shared perform destructive updates, choice points are not shared

2
src/library/blast/state.cpp
View file

@ -706,7 +706,7 @@ branch_extension & state::get_extension(unsigned extid) {
lean_assert(extid < get_extension_manager().get_num_extensions()); lean_assert(extid < get_extension_manager().get_num_extensions());
if (!m_branch.m_extensions[extid]) { if (!m_branch.m_extensions[extid]) {
/* lazy initialization */ /* lazy initialization */
branch_extension * ext = get_extension_manager().get_initial(extid)->clone();; branch_extension * ext = get_extension_manager().get_initial(extid)->clone();
ext->inc_ref(); ext->inc_ref();
m_branch.m_extensions[extid] = ext; m_branch.m_extensions[extid] = ext;
lean_assert(ext->get_rc() == 1); lean_assert(ext->get_rc() == 1);

2
src/library/blast/state.h
View file

@ -45,6 +45,7 @@ class proof_step_cell {
MK_LEAN_RC(); // Declare m_rc counter MK_LEAN_RC(); // Declare m_rc counter
void dealloc() { delete this; } void dealloc() { delete this; }
public: public:
proof_step_cell():m_rc(0) {}
virtual ~proof_step_cell() {} virtual ~proof_step_cell() {}
/** \brief When an action updates the main branch of the proof state, /** \brief When an action updates the main branch of the proof state,
it adds a proof_step object to the proof step stack. it adds a proof_step object to the proof step stack.
@ -103,6 +104,7 @@ class branch_extension {
MK_LEAN_RC(); MK_LEAN_RC();
void dealloc() { delete this; } void dealloc() { delete this; }
public: public:
branch_extension():m_rc(0) {}
virtual ~branch_extension() {} virtual ~branch_extension() {}
/** \brief Return a copy of this object */ /** \brief Return a copy of this object */
virtual branch_extension * clone() = 0; virtual branch_extension * clone() = 0;