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 implicit constructor summary predicate

Browse Source
This commit is contained in:
Leonardo Alt 2020-10-13 09:38:58 +01:00
parent abfa136afb
commit 1e568d7dc6
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/PredicateInstance.cpp
View File

@ -64,7 +64,7 @@ smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const
return _pred(currentFunctionVariables(*constructor, &_contract, _context)); return _pred(currentFunctionVariables(*constructor, &_contract, _context));
auto& state = _context.state(); auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state()}; vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state(0), state.state()};
return _pred(stateExprs + currentStateVariables(_contract, _context)); return _pred(stateExprs + currentStateVariables(_contract, _context));
} }

2
libsolidity/formal/PredicateSort.cpp
View File

@ -60,7 +60,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
return functionSort(*constructor, &_contract, _state); return functionSort(*constructor, &_contract, _state);
return make_shared<FunctionSort>( return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()} + stateSorts(_contract), vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract),
SortProvider::boolSort SortProvider::boolSort
); );
} }