cerc-io/solidity
11
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

Merge pull request #7485 from ethereum/develop

Browse Source 
Merge develop into develop_060
This commit is contained in:
Leonardo
2019-09-26 15:43:12 +02:00
committed by GitHub
parent 9c23f35bec 45583895fc
commit ca714a2d3d
71 changed files with 731 additions and 335 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/analysis/ControlFlowAnalyzer.cpp
+1 -1
View File
@@ -142,7 +142,7 @@ void ControlFlowAnalyzer::checkUninitializedAccess(CFGNode const* _entry, CFGNod
ssl,
string("This variable is of storage pointer type and can be ") +
(variableOccurrence->kind() == VariableOccurrence::Kind::Return ? "returned" : "accessed") +
" without prior assignment."
" without prior assignment, which would lead to undefined behaviour."
);
}
}
libsolidity/formal/SMTEncoder.cpp
+2 -2
View File
@@ -621,8 +621,8 @@ void SMTEncoder::visitFunctionIdentifier(Identifier const& _identifier)
auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type);
if (fType.returnParameterTypes().size() == 1)
{
defineGlobalVariable(fType.richIdentifier(), _identifier);
m_context.createExpression(_identifier, m_context.globalSymbol(fType.richIdentifier()));
defineGlobalVariable(fType.identifier(), _identifier);
m_context.createExpression(_identifier, m_context.globalSymbol(fType.identifier()));
}
}
libsolidity/formal/SMTLib2Interface.cpp
+19 -4
View File
@@ -46,7 +46,7 @@ void SMTLib2Interface::reset()
m_accumulatedOutput.emplace_back();
m_variables.clear();
write("(set-option :produce-models true)");
write("(set-logic QF_UFLIA)");
write("(set-logic ALL)");
}
void SMTLib2Interface::push()
@@ -126,9 +126,24 @@ string SMTLib2Interface::toSExpr(smt::Expression const& _expr)
{
if (_expr.arguments.empty())
return _expr.name;
std::string sexpr = "(" + _expr.name;
for (auto const& arg: _expr.arguments)
sexpr += " " + toSExpr(arg);
std::string sexpr = "(";
if (_expr.name == "const_array")
{
solAssert(_expr.arguments.size() == 2, "");
auto sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments.at(0).sort);
solAssert(sortSort, "");
auto arraySort = dynamic_pointer_cast<ArraySort>(sortSort->inner);
solAssert(arraySort, "");
sexpr += "(as const " + toSmtLibSort(*arraySort) + ") ";
sexpr += toSExpr(_expr.arguments.at(1));
}
else
{
sexpr += _expr.name;
for (auto const& arg: _expr.arguments)
sexpr += " " + toSExpr(arg);
}
sexpr += ")";
return sexpr;
}