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 #11906 from ethereum/smt_fix_bmc

Browse Source 
[SMTChecker] Fix BMCs constraints on internal functions
This commit is contained in:
Alex Beregszaszi
2021-09-15 21:01:29 +01:00
committed by GitHub
parent 1e7460b98e b731957e65
commit c1070fabc0
11 changed files with 246 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+2 -1
View File
@@ -188,7 +188,8 @@ bool BMC::visit(FunctionDefinition const& _function)
{
reset();
initFunction(_function);
m_context.addAssertion(state().txTypeConstraints() && state().txFunctionConstraints(_function));
if (_function.isConstructor() || _function.isPublic())
m_context.addAssertion(state().txTypeConstraints() && state().txFunctionConstraints(_function));
resetStateVariables();
}