public override bool Visit()

in Sources/SolToBoogie/ProcedureTranslator.cs [1969:2068]
88 lines of code
32 McCabe index (conditional complexity)

        public override bool Visit(ExpressionStatement node)
        {
            preTranslationAction(node);
            if (node.Expression is UnaryOperation unaryOperation)
            {
                // only handle increment and decrement operators in a separate statement
                VeriSolAssert(!(unaryOperation.SubExpression is UnaryOperation));
                
                BoogieExpr lhs = TranslateExpr(unaryOperation.SubExpression);
                if (unaryOperation.Operator.Equals("++") ||
                    unaryOperation.Operator.Equals("--"))
                {
                    var oper = unaryOperation.Operator.Equals("++") ? BoogieBinaryOperation.Opcode.ADD : BoogieBinaryOperation.Opcode.SUB;
                    BoogieExpr rhs = new BoogieBinaryOperation(oper, lhs, new BoogieLiteralExpr(1));
                    rhs = AddModuloOp(unaryOperation.SubExpression, rhs, unaryOperation.SubExpression.TypeDescriptions);
                    BoogieAssignCmd assignCmd = new BoogieAssignCmd(lhs, rhs);
                    currentStmtList.AddStatement(assignCmd);
                    
                    var typeDescription = unaryOperation.SubExpression.TypeDescriptions;
                    var isInt = typeDescription.IsInt() || typeDescription.IsUint();
                    if (context.TranslateFlags.InstrumentSums && isInt && unaryOperation.SubExpression is IndexAccess access &&
                        lhs is BoogieMapSelect sel && sel.BaseExpr is BoogieMapSelect arrIdent)
                    {
                        currentStmtList.AddStatement(adjustSum(oper,  arrIdent.Arguments[0], new BoogieLiteralExpr(BigInteger.One)));
                    }
                    
                    //print the value
                    if (!context.TranslateFlags.NoDataValuesInfoFlag)
                    {
                        var callCmd = new BoogieCallCmd("boogie_si_record_sol2Bpl_int", new List<BoogieExpr>() { lhs }, new List<BoogieIdentifierExpr>());
                        callCmd.Attributes = new List<BoogieAttribute>();
                        callCmd.Attributes.Add(new BoogieAttribute("cexpr", $"\"{unaryOperation.SubExpression.ToString()}\""));
                        currentStmtList.AddStatement(callCmd);
                    }
                    AddAssumeForUints(unaryOperation, lhs, unaryOperation.TypeDescriptions);
                }
                else if (unaryOperation.Operator.Equals("delete"))
                {
                    var typeDescription = unaryOperation.SubExpression.TypeDescriptions;
                    var isBasicType = typeDescription.IsInt() || typeDescription.IsUint()
                                      || typeDescription.IsBool() || typeDescription.IsString();

                    // var isArrayAccess = unaryOperation.SubExpression is IndexAccess;
                    if (typeDescription.IsDynamicArray())
                    {
                        BoogieExpr element = TranslateExpr(unaryOperation.SubExpression);
                        BoogieExpr lengthMapSelect = new BoogieMapSelect(new BoogieIdentifierExpr("Length"), element);
                        BoogieExpr rhs = new BoogieLiteralExpr(BigInteger.Zero);
                        var assignCmd = new BoogieAssignCmd(lengthMapSelect, rhs);
                        currentStmtList.AddStatement(assignCmd);

                        var isInt = typeDescription.IsInt() || typeDescription.IsUint();
                        if (context.TranslateFlags.InstrumentSums && isInt)
                        {
                            BoogieExpr sumExpr = getSumAccess(element);
                            var sumAssign = new BoogieAssignCmd(sumExpr, new BoogieLiteralExpr(BigInteger.Zero));
                            currentStmtList.AddStatement(sumAssign);
                        }
                    }
                    else if (typeDescription.IsStaticArray())
                    {
                        // TODO: Handle static arrauy
                        Console.WriteLine($"Warning!!: Currently not handling delete of static arrays");
                    }
                    // This handle cases like delete x with "x" a basic type or delete x[i] when x[i] being a basic type;
                    else if (isBasicType)
                    {
                        var isInt = typeDescription.IsInt() || typeDescription.IsUint();
                        if (context.TranslateFlags.InstrumentSums && isInt && unaryOperation.SubExpression is IndexAccess access &&
                            lhs is BoogieMapSelect sel && sel.BaseExpr is BoogieMapSelect arrIdent)
                        {
                            currentStmtList.AddStatement(adjustSum(BoogieBinaryOperation.Opcode.SUB, arrIdent.Arguments[0], lhs));
                        }
                        
                        BoogieExpr rhs = null;
                        if (typeDescription.IsInt() || typeDescription.IsUint())
                            rhs = new BoogieLiteralExpr(BigInteger.Zero);
                        else if (typeDescription.IsBool())
                            rhs = new BoogieLiteralExpr(false);
                        else if (typeDescription.IsString())
                        {
                            var emptyStr = "";
                            rhs = new BoogieLiteralExpr(new BigInteger(emptyStr.GetHashCode()));
                        }
                        var assignCmd = new BoogieAssignCmd(lhs, rhs);
                        currentStmtList.AddStatement(assignCmd);
                    }
                    else
                    {
                        Console.WriteLine($"Warning!!: Only handle delete for scalars and arrays, found {typeDescription.TypeString}");
                    }
                }
                return false;
            }
            else
            {
                // distribute to different visit functions
                return true;
            }
        }