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

Merge pull request #3344 from leonardoalt/smt_checker

Browse Source 
[SMTChecker] Fix typo in the code (satisifable->satisfiable)
This commit is contained in:
chriseth 2017-12-18 17:49:41 +01:00 committed by GitHub
commit b3fb73f53f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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;
vector<string> values;
tie(result, values) = checkSatisifableAndGenerateModel(expressionsToEvaluate);
tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate);
string conditionalComment;
if (m_conditionalExecutionHappened)
@ -607,12 +607,12 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
m_interface->push();
addPathConjoinedExpression(expr(_condition));
auto positiveResult = checkSatisifable();
auto positiveResult = checkSatisfiable();
m_interface->pop();
m_interface->push();
addPathConjoinedExpression(!expr(_condition));
auto negatedResult = checkSatisifable();
auto negatedResult = checkSatisfiable();
m_interface->pop();
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>>
SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
SMTChecker::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
{
smt::CheckResult result;
vector<string> values;
@ -672,9 +672,9 @@ SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _exp
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)

4
libsolidity/formal/SMTChecker.h
View File

@ -100,9 +100,9 @@ private:
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 resetVariables(std::vector<Declaration const*> _variables);