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

[SMTChecker] Fix typo in the code (satisifable->satisfiable)

Browse Source
This commit is contained in:
Leonardo Alt 2017-12-18 17:31:27 +01:00
parent 55752db956
commit b588134840
2 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsolidity/formal/SMTChecker.cpp
View File

@ -560,7 +560,7 @@ void SMTChecker::checkCondition(
} }
smt::CheckResult result; smt::CheckResult result;
vector<string> values; vector<string> values;
tie(result, values) = checkSatisifableAndGenerateModel(expressionsToEvaluate); tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate);
string conditionalComment; string conditionalComment;
if (m_conditionalExecutionHappened) if (m_conditionalExecutionHappened)
@ -607,12 +607,12 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
m_interface->push(); m_interface->push();
addPathConjoinedExpression(expr(_condition)); addPathConjoinedExpression(expr(_condition));
auto positiveResult = checkSatisifable(); auto positiveResult = checkSatisfiable();
m_interface->pop(); m_interface->pop();
m_interface->push(); m_interface->push();
addPathConjoinedExpression(!expr(_condition)); addPathConjoinedExpression(!expr(_condition));
auto negatedResult = checkSatisifable(); auto negatedResult = checkSatisfiable();
m_interface->pop(); m_interface->pop();
if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR) if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
@ -642,7 +642,7 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
} }
pair<smt::CheckResult, vector<string>> pair<smt::CheckResult, vector<string>>
SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate) SMTChecker::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
{ {
smt::CheckResult result; smt::CheckResult result;
vector<string> values; vector<string> values;
@ -672,9 +672,9 @@ SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _exp
return make_pair(result, values); return make_pair(result, values);
} }
smt::CheckResult SMTChecker::checkSatisifable() smt::CheckResult SMTChecker::checkSatisfiable()
{ {
return checkSatisifableAndGenerateModel({}).first; return checkSatisfiableAndGenerateModel({}).first;
} }
void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)

4
libsolidity/formal/SMTChecker.h
View File

@ -100,9 +100,9 @@ private:
std::pair<smt::CheckResult, std::vector<std::string>> std::pair<smt::CheckResult, std::vector<std::string>>
checkSatisifableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate); checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
smt::CheckResult checkSatisifable(); smt::CheckResult checkSatisfiable();
void initializeLocalVariables(FunctionDefinition const& _function); void initializeLocalVariables(FunctionDefinition const& _function);
void resetVariables(std::vector<Declaration const*> _variables); void resetVariables(std::vector<Declaration const*> _variables);