public static BoogieIfCmd GenerateChoiceBlock()

in Sources/SolToBoogie/TransUtils.cs [781:864]
74 lines of code
18 McCabe index (conditional complexity)

        public static BoogieIfCmd GenerateChoiceBlock(List<ContractDefinition> contracts, TranslatorContext context, Tuple<string, string> callBackTarget = null)
        {
            BoogieIfCmd ifCmd = null;
            int j = 0;
            foreach (var contract in contracts)
            {
                if (contract.ContractKind != EnumContractKind.CONTRACT) continue;

                HashSet<FunctionDefinition> funcDefs = context.GetVisibleFunctionsByContract(contract);
                List<FunctionDefinition> publicFuncDefs = new List<FunctionDefinition>();
                foreach (FunctionDefinition funcDef in funcDefs)
                {
                    if (funcDef.IsConstructor) continue;
                    if (funcDef.IsFallback) continue; //let us not call fallback directly in harness
                    if (funcDef.Visibility == EnumVisibility.PUBLIC || funcDef.Visibility == EnumVisibility.EXTERNAL)
                    {
                        publicFuncDefs.Add(funcDef);
                    }
                }
                for (int i = publicFuncDefs.Count - 1; i >= 0; --i)
                {
                    j++; 
                    BoogieExpr guard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ,
                        new BoogieIdentifierExpr("choice"),
                        new BoogieLiteralExpr(j));

                    BoogieStmtList thenBody = new BoogieStmtList();

                    FunctionDefinition funcDef = publicFuncDefs[i];
                    string callee = TransUtils.GetCanonicalFunctionName(funcDef, context);
                    List<BoogieExpr> inputs = new List<BoogieExpr>()
                {
                    // let us just call back into the calling contract
                    callBackTarget != null ? new BoogieIdentifierExpr(callBackTarget.Item1) : new BoogieIdentifierExpr("this"),
                    callBackTarget != null ? new BoogieIdentifierExpr(callBackTarget.Item2) : new BoogieIdentifierExpr("msgsender_MSG"), 
                    new BoogieIdentifierExpr("msgvalue_MSG"),
                };
                    var inpParamCount = 0;
                    foreach (VariableDeclaration param in funcDef.Parameters.Parameters)
                    {
                        string name = $"__arg_{inpParamCount++}_" + funcDef.Name;
                        if (!string.IsNullOrEmpty(param.Name))
                        {
                            name = TransUtils.GetCanonicalLocalVariableName(param, context);
                        }
                        inputs.Add(new BoogieIdentifierExpr(name));
                        if (param.TypeName is ArrayTypeName array)
                        {
                            thenBody.AddStatement(new BoogieCallCmd(
                                "FreshRefGenerator",
                                new List<BoogieExpr>(), new List<BoogieIdentifierExpr>() { new BoogieIdentifierExpr(name) }));
                        }

                    }

                    List<BoogieIdentifierExpr> outputs = new List<BoogieIdentifierExpr>();
                    var retParamCount = 0;

                    foreach (VariableDeclaration param in funcDef.ReturnParameters.Parameters)
                    {
                        string name = $"__ret_{retParamCount++}_" + funcDef.Name;
                        if (!string.IsNullOrEmpty(param.Name))
                        {
                            name = TransUtils.GetCanonicalLocalVariableName(param, context);

                        }

                        outputs.Add(new BoogieIdentifierExpr(name));
                    }

                    if (context.TranslateFlags.InstrumentGas)
                    {
                        var gasVar = new BoogieIdentifierExpr("gas");
                        thenBody.AddStatement(new BoogieAssignCmd(gasVar, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.SUB, gasVar, new BoogieLiteralExpr(TranslatorContext.TX_GAS_COST))));
                    }
                    BoogieCallCmd callCmd = new BoogieCallCmd(callee, inputs, outputs);
                    thenBody.AddStatement(callCmd);

                    BoogieStmtList elseBody = ifCmd == null ? null : BoogieStmtList.MakeSingletonStmtList(ifCmd);
                    ifCmd = new BoogieIfCmd(guard, thenBody, elseBody);
                }
            }
            return ifCmd;
        }