cerc-io/solidity
16
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 generation of smtlib scripts

Browse Source 
When both CHC and BMC engines are used, the type of state variable
changes when trusted mode for external calls is used. This is because in
CHC engine, trusted mode means we pack more information into the
symbolic state. In BMC this type is always simple.

However, if BMC is run after CHC, in the current code state variables
are reset (and their declaration dumped into SMT-LIB script) before BMC
resets the type of the state variable.

The proposed solution is to simply reset the variable type before the
first variable of this type is created.
This commit is contained in:
Martin Blicha 2023-06-30 15:02:06 +02:00
parent 30cd1a0fb4
commit 3599c8c6b9
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/BMC.cpp
View File

@ -81,13 +81,13 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
SMTEncoder::resetSourceAnalysis(); SMTEncoder::resetSourceAnalysis();
state().prepareForSourceUnit(_source, false);
m_solvedTargets = std::move(_solvedTargets); m_solvedTargets = std::move(_solvedTargets);
m_context.setSolver(m_interface.get()); m_context.setSolver(m_interface.get());
m_context.reset(); m_context.reset();
m_context.setAssertionAccumulation(true); m_context.setAssertionAccumulation(true);
m_variableUsage.setFunctionInlining(shouldInlineFunctionCall); m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
createFreeConstants(sourceDependencies(_source)); createFreeConstants(sourceDependencies(_source));
state().prepareForSourceUnit(_source, false);
m_unprovedAmt = 0; m_unprovedAmt = 0;
_source.accept(*this); _source.accept(*this);