private void GenerateInitializationForMappingStateVar()

in Sources/SolToBoogie/ProcedureTranslator.cs [687:800]
101 lines of code
18 McCabe index (conditional complexity)

        private void GenerateInitializationForMappingStateVar(VariableDeclaration varDecl, Mapping mapping)
        {
            BoogieMapSelect lhsMap = CreateDistinctArrayMappingAddress(currentStmtList, varDecl);

            //nested arrays (only 1 level for now)
            if (mapping.ValueType is ArrayTypeName array)
            {
                Console.WriteLine($"Warning: A mapping with nested array {varDecl.Name} of valuetype {mapping.ValueType.ToString()}");

                InitializeNestedArrayMappingStateVar(varDecl, mapping);
            }
            else if (mapping.ValueType is Mapping mappingNested)
            {
                InitializeNestedArrayMappingStateVar(varDecl, mapping);
                // TODO: add the initialization of m[i][j]
            }
            else if (mapping.ValueType is UserDefinedTypeName userTypeName ||
                mapping.ValueType.ToString().Equals("address") ||
                mapping.ValueType.ToString().Equals("address payable") ||
                mapping.ValueType.ToString().StartsWith("bytes")
                )
            {
                currentStmtList.AddStatement(new BoogieCommentCmd($"Initialize address/contract mapping {varDecl.Name}"));

                BoogieType mapKeyType;
                BoogieMapSelect lhs;
                GetBoogieTypesFromMapping(varDecl, mapping, out mapKeyType, out lhs);
                if (!context.TranslateFlags.QuantFreeAllocs)
                {
                    var qVar = QVarGenerator.NewQVar(0, 0);
                    BoogieExpr zeroExpr = new BoogieIdentifierExpr("null");

                    if (mapping.ValueType.ToString().StartsWith("bytes"))
                        zeroExpr = new BoogieLiteralExpr(BigInteger.Zero);

                    var bodyExpr = new BoogieBinaryOperation(
                        BoogieBinaryOperation.Opcode.EQ,
                        new BoogieMapSelect(lhs, qVar),
                        zeroExpr);
                    var qExpr = new BoogieQuantifiedExpr(true, new List<BoogieIdentifierExpr>() {qVar},
                        new List<BoogieType>() {mapKeyType}, bodyExpr);
                    currentStmtList.AddStatement(new BoogieAssumeCmd(qExpr));
                }
                else
                {
                    if (mapping.ValueType.ToString().StartsWith("bytes"))
                        currentStmtList.AddStatement(new BoogieAssignCmd(lhs,
                            GetCallExprForZeroInit(mapKeyType, BoogieType.Int)));
                    else
                        currentStmtList.AddStatement(new BoogieAssignCmd(lhs, GetCallExprForZeroInit(mapKeyType, BoogieType.Ref)));
                }
            }
            else if (mapping.ValueType.ToString().Equals("bool"))
            {
                currentStmtList.AddStatement(new BoogieCommentCmd($"Initialize Boolean mapping {varDecl.Name}"));

                BoogieType mapKeyType;
                BoogieMapSelect lhs;
                GetBoogieTypesFromMapping(varDecl, mapping, out mapKeyType, out lhs);
                if (!context.TranslateFlags.QuantFreeAllocs)
                {
                    var qVar = QVarGenerator.NewQVar(0, 0);
                    var bodyExpr =
                        new BoogieUnaryOperation(BoogieUnaryOperation.Opcode.NOT, new BoogieMapSelect(lhs, qVar));
                    var qExpr = new BoogieQuantifiedExpr(true, new List<BoogieIdentifierExpr>() {qVar},
                        new List<BoogieType>() {mapKeyType}, bodyExpr);
                    currentStmtList.AddStatement(new BoogieAssumeCmd(qExpr));
                }
                else
                {
                    currentStmtList.AddStatement(new BoogieAssignCmd(lhs, GetCallExprForZeroInit(mapKeyType, BoogieType.Bool)));
                }
            }
            // TODO: Cleanup, StartsWith("uint") can include uint[12] as well. 
            else if (mapping.ValueType.ToString().StartsWith("uint") ||
                mapping.ValueType.ToString().StartsWith("int"))
            {
                // Issue a warning for intXX type in case /useModularArithemtic option is used:
                if (context.TranslateFlags.UseModularArithmetic && mapping.ValueType.ToString().StartsWith("int"))
                {
                    Console.WriteLine($"Warning: signed integer arithmetic is not handled with /useModularArithmetic option");
                }

                currentStmtList.AddStatement(new BoogieCommentCmd($"Initialize Integer mapping {varDecl.Name}"));

                BoogieType mapKeyType;
                BoogieMapSelect lhs;
                GetBoogieTypesFromMapping(varDecl, mapping, out mapKeyType, out lhs);
                if (!context.TranslateFlags.QuantFreeAllocs)
                {
                    var qVar = QVarGenerator.NewQVar(0, 0);
                    var bodyExpr = new BoogieBinaryOperation(
                        BoogieBinaryOperation.Opcode.EQ,
                        new BoogieMapSelect(lhs, qVar),
                        new BoogieLiteralExpr(0));
                    var qExpr = new BoogieQuantifiedExpr(true, new List<BoogieIdentifierExpr>() {qVar},
                        new List<BoogieType>() {mapKeyType}, bodyExpr);
                    currentStmtList.AddStatement(new BoogieAssumeCmd(qExpr));
                }
                else
                {
                    currentStmtList.AddStatement(new BoogieAssignCmd(lhs, GetCallExprForZeroInit(mapKeyType, BoogieType.Int)));
                }

                if (context.TranslateFlags.InstrumentSums)
                {
                    currentStmtList.AddStatement(new BoogieAssignCmd(getSumAccess(lhsMap), new BoogieLiteralExpr(BigInteger.Zero)));
                }
            }
            else
            {
                Console.WriteLine($"Warning: A mapping with complex value type {varDecl.Name} of valuetype {mapping.ValueType.ToString()}");
            }
        }