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 #7058 from ethereum/smt_reset_context

Browse Source 
[SMTChecker] Clear encoding context before engine starts
This commit is contained in:
chriseth 2019-07-08 12:36:50 +02:00 committed by GitHub
commit 25928767b7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 18 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/BMC.cpp
View File

@ -49,6 +49,8 @@ void BMC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner
m_scanner = _scanner;
m_context.clear();
_source.accept(*this);
solAssert(m_interface->solvers() > 0, "");

6
libsolidity/formal/EncodingContext.cpp
View File

@ -44,6 +44,12 @@ void EncodingContext::reset()
m_assertions.clear();
}
void EncodingContext::clear()
{
m_variables.clear();
reset();
}
/// Variables.
shared_ptr<SymbolicVariable> EncodingContext::variable(solidity::VariableDeclaration const& _varDecl)

7
libsolidity/formal/EncodingContext.h
View File

@ -38,8 +38,13 @@ class EncodingContext
public:
EncodingContext(std::shared_ptr<SolverInterface> _solver);
/// Resets the entire context.
/// Resets the entire context except for symbolic variables which stay
/// alive because of state variables and inlined function calls.
/// To be used in the beginning of a root function visit.
void reset();
/// Clears the entire context, erasing everything.
/// To be used before a model checking engine starts.
void clear();
/// Forwards variable creation to the solver.
Expression newVariable(std::string _name, SortPointer _sort)

6
test/libsolidity/smtCheckerTestsJSON/multi.json
View File

@ -3,9 +3,9 @@
{
"smtlib2responses":
{
"0x68fa399769cf119cbe46d5ae578164d39ea67e06eee08eeb37042d08a13a0cd8": "unsat\n",
"0xd78cd71ff120c5b5ecc5020146952f62de0506c4baef7ba499239a2ce2b14343": "sat\n((|EVALEXPR_0| 0))\n",
"0xf74672131cc6b7b3d6b82ed2fa0da2b75d01c9bc32f15d2f77e8e39e174f5a37": "sat\n((|EVALEXPR_0| 1))\n"
"0x6e5cf865938b82f1627009d26ecb4c59e9b8c05cc1024ccf548b9b94c1c73e56": "unsat\n",
"0x890d45bd5b96d51c4d11683bcf3b7547cea993b3e15961c216a0a782d5d3ccb2": "sat\n((|EVALEXPR_0| 0))\n",
"0xa649be28767cedec4a7b7f5591e3fb237447405a823dbd861869eb35d91bebce": "sat\n((|EVALEXPR_0| 1))\n"
}
}
}

2
test/libsolidity/smtCheckerTestsJSON/simple.json
View File

@ -3,7 +3,7 @@
{
"smtlib2responses":
{
"0x9e377366ae857502a72974bd4e563258a29fa84dd4358cc053057544409da0ea": "sat\n((|EVALEXPR_0| 0))\n"
"0xcae00c08b91a968103a89431c473645366101a2b037d72aa10fbe3099ccd6931": "sat\n((|EVALEXPR_0| 0))\n"
}
}
}