public override bool Visit()

in Sources/SolToBoogie/ProcedureTranslator.cs [2331:2492]
138 lines of code
26 McCabe index (conditional complexity)

        public override bool Visit(FunctionCall node)
        {
            preTranslationAction(node);

            // VeriSolAssert(!(node.Expression is NewExpression), $"new expressions should be handled in assignment");
            if (node.Expression is NewExpression)
            {
                BoogieIdentifierExpr tmpVarExpr = MkNewLocalVariableForFunctionReturn(node);
                TranslateNewStatement(node, tmpVarExpr);
                currentExpr = tmpVarExpr;
                return false;
            }

            var functionName = TransUtils.GetFuncNameFromFuncCall(node);

            if (functionName.Equals("assert"))
            {
                // TODO:
                //countNestedFuncCallsRelExprs--;
                VeriSolAssert(node.Arguments.Count == 1);
                BoogieExpr predicate = TranslateExpr(node.Arguments[0]);
                BoogieAssertCmd assertCmd = new BoogieAssertCmd(predicate);
                currentStmtList.AddStatement(assertCmd);
            }
            else if (functionName.Equals("require"))
            {
                // TODO:
                //countNestedFuncCallsRelExprs--;
                VeriSolAssert(node.Arguments.Count == 1 || node.Arguments.Count == 2);
                BoogieExpr predicate = TranslateExpr(node.Arguments[0]);

                if (!context.TranslateFlags.ModelReverts)
                {
                    BoogieAssumeCmd assumeCmd = new BoogieAssumeCmd(predicate);
                    currentStmtList.AddStatement(assumeCmd);
                }
                else
                {
                    BoogieStmtList revertLogic = new BoogieStmtList();

                    emitRevertLogic(revertLogic);

                    BoogieIfCmd requierCheck = new BoogieIfCmd(new BoogieUnaryOperation(BoogieUnaryOperation.Opcode.NOT, predicate), revertLogic, null);

                    currentStmtList.AddStatement(requierCheck);
                }
            }
            else if (functionName.Equals("revert"))
            {
                VeriSolAssert(node.Arguments.Count == 0 || node.Arguments.Count == 1);
                if (!context.TranslateFlags.ModelReverts)
                {
                    BoogieAssumeCmd assumeCmd = new BoogieAssumeCmd(new BoogieLiteralExpr(false));
                    currentStmtList.AddStatement(assumeCmd);
                }
                else
                {
                    emitRevertLogic(currentStmtList);
                }
            }
            else if (IsImplicitFunc(node))
            {
                BoogieIdentifierExpr tmpVarExpr = MkNewLocalVariableForFunctionReturn(node);
                bool isElementaryCast = false;  

                if (IsContractConstructor(node)) {
                    TranslateNewStatement(node, tmpVarExpr);
                } else if (IsTypeCast(node)) {
                    TranslateTypeCast(node, tmpVarExpr, out isElementaryCast);
                } else if (IsAbiEncodePackedFunc(node)) {
                    TranslateAbiEncodedFuncCall(node, tmpVarExpr);
                } else if (IsKeccakFunc(node)) {
                    TranslateKeccakFuncCall(node, tmpVarExpr);
                } else if (IsStructConstructor(node)) {
                    TranslateStructConstructor(node, tmpVarExpr);
                } else
                {
                    VeriSolAssert(false, $"Unexpected implicit function {node.ToString()}");
                }

                if (!isElementaryCast)
                {
                    // We should not introduce temporaries for address(this).balance in a specification
                    currentExpr = tmpVarExpr;
                }
            }
            else if (IsVeriSolCodeContractFunction(node))
            {
                // we cannot use temporaries as we are translating a specification
                currentExpr = TranslateVeriSolCodeContractFuncCall(node);
            }
            else if (context.HasEventNameInContract(currentContract, functionName))
            {
                // generate empty statement list to ignore the event call                
                List<BoogieAttribute> attributes = new List<BoogieAttribute>()
                {
                new BoogieAttribute("EventEmitted", "\"" + functionName + "_" + currentContract.Name + "\""),
                };
                currentStmtList.AddStatement(new BoogieAssertCmd(new BoogieLiteralExpr(true), attributes));
            }
            else if (functionName.Equals("call"))
            {
                TranslateCallStatement(node);
            }
            else if (functionName.Equals("delegatecall"))
            {
                VeriSolAssert(false, "low-level delegatecall statements not supported...");
            }
            else if (IsBuiltInTransferFunc(functionName, node))
            {
                TranslateTransferCallStmt(node);
            }
            else if (functionName.Equals("send"))
            {
                var tmpVarExpr = MkNewLocalVariableForFunctionReturn(node);
                var amountExpr = TranslateExpr(node.Arguments[0]);
                TranslateSendCallStmt(node, tmpVarExpr, amountExpr);
                currentExpr = tmpVarExpr;
            }
            else if (IsDynamicArrayPush(node))
            {
                TranslateDynamicArrayPush(node);
            }
            else if (IsExternalFunctionCall(node))
            {
                // external function calls

                var memberAccess = node.Expression as MemberAccess;
                VeriSolAssert(memberAccess != null, $"An external function has to be a member access, found {node.ToString()}");

                // HACK: this is the way to identify the return type is void and hence don't need temporary variable
                if (node.TypeDescriptions.TypeString != "tuple()")
                {
                    var tmpVarExpr = MkNewLocalVariableForFunctionReturn(node);
                    var outParams = new List<BoogieIdentifierExpr>() { tmpVarExpr };
                    TranslateExternalFunctionCall(node, outParams);
                    currentExpr = tmpVarExpr;
                }
                else
                {
                    TranslateExternalFunctionCall(node);
                }
            }
            else // internal function calls
            {
                // HACK: this is the way to identify the return type is void and hence don't need temporary variable
                if (node.TypeDescriptions.TypeString != "tuple()")
                {
                    // internal function calls
                    var tmpVarExpr = MkNewLocalVariableForFunctionReturn(node);
                    var outParams = new List<BoogieIdentifierExpr>() { tmpVarExpr };
                    TranslateInternalFunctionCall(node, outParams);
                    currentExpr = tmpVarExpr;
                }
                else
                {
                    TranslateInternalFunctionCall(node);
                }

            }
            return false;
        }