| 361 | } |
| 362 | |
| 363 | std::vector<std::optional<std::string>> Predicate::summaryPostInputValues(std::vector<smtutil::Expression> const& _args) const |
| 364 | { |
| 365 | /// The signature of a function summary predicate is: summary(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). |
| 366 | /// Here we are interested in postInputVars. |
| 367 | auto const* function = programFunction(); |
| 368 | solAssert(function, ""); |
| 369 | |
| 370 | auto stateVars = stateVariables(); |
| 371 | solAssert(stateVars.has_value(), ""); |
| 372 | |
| 373 | auto const& inParams = function->parameters(); |
| 374 | |
| 375 | auto first = _args.begin() + static_cast<int>(firstArgIndex()) + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1; |
| 376 | auto last = first + static_cast<int>(inParams.size()); |
| 377 | |
| 378 | solAssert(first >= _args.begin() && first <= _args.end(), ""); |
| 379 | solAssert(last >= _args.begin() && last <= _args.end(), ""); |
| 380 | |
| 381 | std::vector<smtutil::Expression> inValues(first, last); |
| 382 | solAssert(inValues.size() == inParams.size(), ""); |
| 383 | auto inTypes = SMTEncoder::replaceUserTypes(FunctionType(*function).parameterTypes()); |
| 384 | return formatExpressions(inValues, inTypes); |
| 385 | } |
| 386 | |
| 387 | std::vector<std::optional<std::string>> Predicate::summaryPostOutputValues(std::vector<smtutil::Expression> const& _args) const |
| 388 | { |
no test coverage detected