| 1262 | } |
| 1263 | |
| 1264 | void SMTEncoder::visitFunctionIdentifier(Identifier const& _identifier) |
| 1265 | { |
| 1266 | auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type); |
| 1267 | if (replaceUserTypes(fType.returnParameterTypes()).size() == 1) |
| 1268 | { |
| 1269 | defineGlobalVariable(fType.identifier(), _identifier); |
| 1270 | m_context.createExpression(_identifier, m_context.globalSymbol(fType.identifier())); |
| 1271 | } |
| 1272 | } |
| 1273 | |
| 1274 | void SMTEncoder::visitStructConstructorCall(FunctionCall const& _funCall) |
| 1275 | { |
nothing calls this directly
no test coverage detected