cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

cex2dot debug

Browse Source
This commit is contained in:
Leonardo Alt 2020-07-17 12:26:55 +02:00
parent 5bb4e73693
commit d5f00842d9
2 changed files with 20 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
libsolidity/formal/CHC.cpp
View File

@ -1471,6 +1471,22 @@ string CHC::formatFunctionCallCounterexample(vector<VariableDeclaration const*>
return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")"; return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")";
} }
string CHC::cex2dot(smtutil::CHCSolverInterface::CexGraph const& _cex)
{
string dot = "digraph {\n";
auto pred = [&](CHCSolverInterface::CexNode const& _node) {
return "\"" + _node.first + "(" + boost::algorithm::join(_node.second, ", ") + ")\"";
};
for (auto const& [u, vs]: _cex.edges)
for (auto v: vs)
dot += pred(_cex.nodes.at(v)) + " -> " + pred(_cex.nodes.at(u)) + "\n";
dot += "}";
return dot;
}
string CHC::uniquePrefix() string CHC::uniquePrefix()
{ {
return to_string(m_blockCounter++); return to_string(m_blockCounter++);

4
libsolidity/formal/CHC.h
View File

@ -223,6 +223,10 @@ private:
/// with the concrete values for value type parameters and /// with the concrete values for value type parameters and
/// the parameter name for reference types. /// the parameter name for reference types.
std::string formatFunctionCallCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const& _function, std::vector<std::string> const& _summaryValues); std::string formatFunctionCallCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const& _function, std::vector<std::string> const& _summaryValues);
/// @returns a DAG in the dot format.
/// Used for debugging purposes.
std::string cex2dot(smtutil::CHCSolverInterface::CexGraph const& _graph);
//@} //@}
/// Misc. /// Misc.