Skip to content

Out-of-line prop_conv_solvert::decision_procedure_text to work around g++-5 bug #4723

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 30, 2019
Merged

Out-of-line prop_conv_solvert::decision_procedure_text to work around g++-5 bug #4723

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions src/solvers/prop/prop_conv_solver.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -574,3 +574,13 @@ void prop_conv_solvert::pop()

prop.set_assumptions(assumption_stack);
}

// This method out-of-line because gcc-5.5.0-12ubuntu1 20171010 miscompiles it
// when inline (in certain build configurations, notably -O2 -g0) by producing
// a non-virtual thunk with c++03 ABI but a function body with c++11 ABI, the
// mismatch leading to a missing vtable entry and consequent null-pointer deref
// whenever this function is called.
std::string prop_conv_solvert::decision_procedure_text() const
{
return "propositional reduction";
}
5 changes: 1 addition & 4 deletions src/solvers/prop/prop_conv_solver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,10 +39,7 @@ class prop_conv_solvert : public conflict_providert,
// overloading from decision_proceduret
decision_proceduret::resultt dec_solve() override;
void print_assignment(std::ostream &out) const override;
std::string decision_procedure_text() const override
{
return "propositional reduction";
}
std::string decision_procedure_text() const override;
exprt get(const exprt &expr) const override;

tvt l_get(literalt a) const override
Expand Down