public override bool Visit()

in Sources/SolToBoogie/ProcedureTranslator.cs [3538:3645]
99 lines of code
29 McCabe index (conditional complexity)

        public override bool Visit(BinaryOperation node)
        {
            preTranslationAction(node);
            BoogieExpr leftExpr = TranslateExpr(node.LeftExpression);
            BoogieExpr rightExpr = TranslateExpr(node.RightExpression);

            BoogieBinaryOperation.Opcode op;
            switch (node.Operator)
            {
                case "+":
                    op = BoogieBinaryOperation.Opcode.ADD;
                    break;
                case "-":
                    op = BoogieBinaryOperation.Opcode.SUB;
                    break;
                case "*":
                    op = BoogieBinaryOperation.Opcode.MUL;
                    break;
                case "**":
                    // Handled below for constants only
                    // TODO: Need to introduce opcode for power operation
                    op = BoogieBinaryOperation.Opcode.MUL;
                    break;
                case "/":
                    op = BoogieBinaryOperation.Opcode.DIV;
                    break;
                case "%":
                    op = BoogieBinaryOperation.Opcode.MOD;
                    break;
                case "==":
                    op = BoogieBinaryOperation.Opcode.EQ;
                    break;
                case "!=":
                    op = BoogieBinaryOperation.Opcode.NEQ;
                    break;
                case ">":
                    op = BoogieBinaryOperation.Opcode.GT;
                    break;
                case ">=":
                    op = BoogieBinaryOperation.Opcode.GE;
                    break;
                case "<":
                    op = BoogieBinaryOperation.Opcode.LT;
                    break;
                case "<=":
                    op = BoogieBinaryOperation.Opcode.LE;
                    break;
                case "&&":
                    op = BoogieBinaryOperation.Opcode.AND;
                    break;
                case "||":
                    op = BoogieBinaryOperation.Opcode.OR;
                    break;
                default:
                    op = BoogieBinaryOperation.Opcode.UNKNOWN;
                    VeriSolAssert(false, $"Unknown binary operator: {node.Operator}");
                    break;
            }

            BoogieExpr binaryExpr;
            if (node.Operator == "**")
            {
                if (node.LeftExpression.TypeDescriptions.IsUintConst(node.LeftExpression, out BigInteger valueLeft, out uint szLeft) &&
                    node.RightExpression.TypeDescriptions.IsUintConst(node.RightExpression, out BigInteger valueRight, out uint szRight))
                {

                    binaryExpr = new BoogieLiteralExpr((BigInteger)Math.Pow((double)valueLeft, (double)valueRight));
                }
                else
                {
                    Console.WriteLine($"VeriSol translation error: power operation for non-constants or with constant subexpressions is not supported; hint: use temps for subexpressions");
                    return false;
                }
            }
            else
            {
                binaryExpr = new BoogieBinaryOperation(op, leftExpr, rightExpr);
            }
            currentExpr = binaryExpr;

            if (context.TranslateFlags.UseModularArithmetic)
            {
                //if (node.Operator == "+" || node.Operator == "-" || node.Operator == "*" || node.Operator == "/" || node.Operator == "**")
                if (node.Operator == "+" || node.Operator == "-" || node.Operator == "*" || node.Operator == "/")
                {
                    if (node.LeftExpression.TypeDescriptions != null && node.RightExpression.TypeDescriptions != null)
                    {
                        var isUintLeft = node.LeftExpression.TypeDescriptions.IsUintWSize(node.LeftExpression, out uint szLeft);
                        var isUintRight = node.RightExpression.TypeDescriptions.IsUintWSize(node.RightExpression, out uint szRight);
                        var isUintConstLeft = node.LeftExpression.TypeDescriptions.IsUintConst(node.LeftExpression, out BigInteger valueLeft, out uint szLeftConst);
                        var isUintConstRight = node.RightExpression.TypeDescriptions.IsUintConst(node.RightExpression, out BigInteger valueRight, out uint szRightConst);
                        // If both operands are literals, do not use "modBpl" for the binary operation:
                        if (isUintLeft && isUintRight)
                        {
                            if (!isUintConstLeft || !isUintConstRight)
                            {
                                VeriSolAssert(szLeft != 0, $"size of uint lhs in binary expr is zero");
                                VeriSolAssert(szRight != 0, $"size of uint rhs in binary expr is zero");
                                BigInteger maxUIntValue = (BigInteger)Math.Pow(2, Math.Max(szLeft, szRight));
                                currentExpr = new BoogieFuncCallExpr("modBpl", new List<BoogieExpr>() { binaryExpr, new BoogieLiteralExpr(maxUIntValue) });
                            }        
                        }
                    }
                }
            }
            
            return false;
        }