From 6976b676eab3196f5f47765b3300a96905939c3b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 29 May 2019 12:07:19 +0100 Subject: [PATCH] Out-of-line prop_conv_solvert::decision_procedure_text to work around g++-5 bug As elaborated in the comment in prop_conv_solver.cpp, under some configurations g++-5 would miscompile the inline version. --- src/solvers/prop/prop_conv_solver.cpp | 10 ++++++++++ src/solvers/prop/prop_conv_solver.h | 5 +---- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index 68cfdb1e903..0a9d3406c15 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -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"; +} diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h index 0bb5dfe6adf..8bd6a728aaa 100644 --- a/src/solvers/prop/prop_conv_solver.h +++ b/src/solvers/prop/prop_conv_solver.h @@ -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