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 #10026 from ethereum/smt_fix_predicates_again

Browse Source 
[SMTChecker] Fix counterexample state reporting
This commit is contained in:
Leonardo 2020-10-13 23:05:05 +01:00 committed by GitHub
commit 4d94a9e35b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsolidity/formal/Predicate.cpp
View File

@ -189,7 +189,7 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
vector<string> Predicate::summaryStateValues(vector<string> const& _args) const vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
{ {
/// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of an implicit constructor summary predicate is: summary(error, this, txData, postBlockchainState, postStateVars). /// The signature of an implicit constructor summary predicate is: summary(error, this, txData, preBlockSchainState, postBlockchainState, postStateVars).
/// Here we are interested in postStateVars. /// Here we are interested in postStateVars.
auto stateVars = stateVariables(); auto stateVars = stateVariables();
@ -204,7 +204,7 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
} }
else if (programContract()) else if (programContract())
{ {
stateFirst = _args.begin() + 4; stateFirst = _args.begin() + 5;
stateLast = stateFirst + static_cast<int>(stateVars->size()); stateLast = stateFirst + static_cast<int>(stateVars->size());
} }
else else