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

Merge pull request #10014 from ethereum/smt_fix_predicagte

Browse Source 
[SMTChecker] Fix implicit constructor summary predicate
This commit is contained in:
Leonardo 2020-10-13 14:55:52 +01:00 committed by GitHub
commit 8fd6de9403
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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));
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));
}

2
libsolidity/formal/PredicateSort.cpp
View File

@ -60,7 +60,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
return functionSort(*constructor, &_contract, _state);
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
);
}