| 1272 | } |
| 1273 | |
| 1274 | void SMTEncoder::visitStructConstructorCall(FunctionCall const& _funCall) |
| 1275 | { |
| 1276 | solAssert(*_funCall.annotation().kind == FunctionCallKind::StructConstructorCall, ""); |
| 1277 | if (smt::isNonRecursiveStruct(*_funCall.annotation().type)) |
| 1278 | { |
| 1279 | auto& structSymbolicVar = dynamic_cast<smt::SymbolicStructVariable&>(*m_context.expression(_funCall)); |
| 1280 | auto structType = dynamic_cast<StructType const*>(structSymbolicVar.type()); |
| 1281 | solAssert(structType, ""); |
| 1282 | auto const& structMembers = structType->structDefinition().members(); |
| 1283 | solAssert(structMembers.size() == _funCall.sortedArguments().size(), ""); |
| 1284 | auto args = _funCall.sortedArguments(); |
| 1285 | structSymbolicVar.assignAllMembers(applyMap( |
| 1286 | ranges::views::zip(args, structMembers), |
| 1287 | [this] (auto const& argMemberPair) { return expr(*argMemberPair.first, argMemberPair.second->type()); } |
| 1288 | )); |
| 1289 | } |
| 1290 | |
| 1291 | } |
| 1292 | |
| 1293 | void SMTEncoder::endVisit(Literal const& _literal) |
| 1294 | { |
nothing calls this directly
no test coverage detected