public override bool Visit()

in Sources/SolToBoogie/ProcedureTranslator.cs [3660:3788]
103 lines of code
12 McCabe index (conditional complexity)

        public override bool Visit(IndexAccess node)
        {
            preTranslationAction(node);
            Expression baseExpression = node.BaseExpression;
            Expression indexExpression = node.IndexExpression;

            BoogieType indexType = MapArrayHelper.InferExprTypeFromTypeString(indexExpression.TypeDescriptions.TypeString);
            BoogieExpr indexExpr = TranslateExpr(indexExpression);

            // the baseExpression has an array or mapping type
            BoogieType baseKeyType = MapArrayHelper.InferKeyTypeFromTypeString(baseExpression.TypeDescriptions.TypeString);
            BoogieType baseValType = MapArrayHelper.InferValueTypeFromTypeString(baseExpression.TypeDescriptions.TypeString);
            BoogieExpr baseExpr = null;

            baseExpr = TranslateExpr(baseExpression);
            //if (node.BaseExpression is Identifier identifier)
            //{
            //    baseExpr = TranslateExpr(identifier);
            //}
            //else if (node.BaseExpression is IndexAccess indexAccess)
            //{
            //    baseExpr = TranslateExpr(indexAccess);
            //}
            //else
            //{
            //    VeriSolAssert(false, $"Unknown base in index access: {node.BaseExpression}");
            //}

            BoogieExpr indexAccessExpr = new BoogieMapSelect(baseExpr, indexExpr);
            currentExpr = MapArrayHelper.GetMemoryMapSelectExpr(baseKeyType, baseValType, baseExpr, indexExpr);

            if (context.TranslateFlags.LazyNestedAlloc)
            {
                var valTypeString = MapArrayHelper.GetValueTypeString(baseExpression.TypeDescriptions.TypeString);
                var valIsMapping = MapArrayHelper.IsMappingTypeString(valTypeString);
                var valIsArray = MapArrayHelper.IsArrayTypeString(valTypeString);

                if (valIsArray || valIsMapping)
                {
                    // Check and alloc.
                    BoogieStmtList allocAndInit = new BoogieStmtList();
                    var tmpVarIdentExpr = MkNewLocalVariableWithType(baseValType);
                    allocAndInit.AddStatement(new BoogieCallCmd("FreshRefGenerator",
                        new List<BoogieExpr>(),
                        new List<BoogieIdentifierExpr>() {tmpVarIdentExpr}
                    ));
                    allocAndInit.AddStatement(new BoogieAssignCmd(currentExpr, tmpVarIdentExpr));

                    if (valIsArray)
                    {
                        allocAndInit.AddStatement(new BoogieAssignCmd(new BoogieMapSelect(new BoogieIdentifierExpr("Length"), currentExpr), new BoogieLiteralExpr(0)));
                    }
                    
                    BoogieType nestedValType = MapArrayHelper.InferValueTypeFromTypeString(valTypeString);
                    BoogieType nestedKeyType = MapArrayHelper.InferKeyTypeFromTypeString(valTypeString);

                    var mapName = new BoogieIdentifierExpr(MapArrayHelper.GetMemoryMapName(nestedKeyType, nestedValType));
                    var derefCurrExpr = new BoogieMapSelect(mapName, currentExpr);
                    
                    var qVar1 = QVarGenerator.NewQVar(0, 0);
                    var idxNestedMap = new BoogieMapSelect(derefCurrExpr, qVar1);
                    if (nestedValType == BoogieType.Bool)
                    {
                        if (context.TranslateFlags.QuantFreeAllocs)
                        {
                            allocAndInit.AddStatement(new BoogieAssignCmd(derefCurrExpr, GetCallExprForZeroInit(nestedKeyType, BoogieType.Bool)));
                        }
                        else
                        {
                            var bodyExpr = new BoogieBinaryOperation(
                                BoogieBinaryOperation.Opcode.EQ, 
                                idxNestedMap,
                                new BoogieLiteralExpr(false));
                            var qExpr = new BoogieQuantifiedExpr(true, new List<BoogieIdentifierExpr>() {qVar1},
                                new List<BoogieType>() {nestedKeyType}, bodyExpr);
                            allocAndInit.AddStatement(new BoogieAssumeCmd(qExpr));
                        }
                    }
                    else if (nestedValType == BoogieType.Int)
                    {
                        if (context.TranslateFlags.QuantFreeAllocs)
                        {
                            allocAndInit.AddStatement(new BoogieAssignCmd(derefCurrExpr, GetCallExprForZeroInit(nestedKeyType, BoogieType.Int)));
                        }
                        else
                        {
                            var bodyExpr = new BoogieBinaryOperation(
                                BoogieBinaryOperation.Opcode.EQ, 
                                idxNestedMap,
                                new BoogieLiteralExpr(0));
                            var qExpr = new BoogieQuantifiedExpr(true, new List<BoogieIdentifierExpr>() {qVar1},
                                new List<BoogieType>() {nestedKeyType}, bodyExpr);
                            allocAndInit.AddStatement(new BoogieAssumeCmd(qExpr));
                        }

                        if (context.TranslateFlags.InstrumentSums)
                        {
                            allocAndInit.AddStatement(new BoogieAssignCmd(getSumAccess(currentExpr), new BoogieLiteralExpr(BigInteger.Zero)));
                        }
                    }
                    else if (nestedValType == BoogieType.Ref)
                    {
                        if (context.TranslateFlags.QuantFreeAllocs)
                        {
                            allocAndInit.AddStatement(new BoogieAssignCmd(derefCurrExpr, GetCallExprForZeroInit(nestedKeyType, BoogieType.Ref)));
                        }
                        else
                        {
                            var bodyExpr = new BoogieBinaryOperation(
                                BoogieBinaryOperation.Opcode.EQ, 
                                idxNestedMap,
                                new BoogieIdentifierExpr("null"));
                            var qExpr = new BoogieQuantifiedExpr(true, new List<BoogieIdentifierExpr>() {qVar1},
                                new List<BoogieType>() {nestedKeyType}, bodyExpr);
                            allocAndInit.AddStatement(new BoogieAssumeCmd(qExpr));
                        }
                    }
                    else
                    {
                        throw new Exception("Unexpected type in nested mapping.");
                    }

                    currentStmtList.AddStatement(new BoogieIfCmd(
                        new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, currentExpr,
                            new BoogieIdentifierExpr("null")), allocAndInit, null));
                }
            }
            return false;
        }