public void AddCallInstruction()

in ironclad-apps/tools/DafnyCC/CompileMethod.cs [1014:1082]
68 lines of code
26 McCabe index (conditional complexity)

    public void AddCallInstruction(List<RtlVar> destVars, List<Formal> ins, string name, List<Expression> args,
        Attributes attrs, List<RtlExp> rtlExps = null)
    {
        name = GhostProcName(name);
        var operands = InstructionAttributes(attrs);
        bool strictOperands = Attributes.Contains(attrs, "strict_operands");
        bool modifiesIo = Attributes.Contains(attrs, "modifies_io");
        string envArgs = ", objLayouts, $S, $toAbs, $absMem, $commonVars, $gcVars, init, stk, statics, core_state, ptMem, mems, $stacksFrames";
        string envIn = modifiesIo ? ", io" + envArgs : "";
        string envOut = modifiesIo ? ", io" : "";
        for (int i = 0; i < args.Count; i++)
        {
            RtlExp re = (rtlExps == null) ? null : rtlExps[i];
            envIn += ", " + ((re != null) ? re.ToString() : GhostExpression(args[i]).ToString());
        }
        envOut += String.Concat(destVars.Select(x => ", " + x));
        if (instructionProcArgs != null)
        {
            var operandString = String.Concat(instructionProcArgs.Select(arg => ", " + arg));
            stmts.Add(new RtlGhostStmtComputed(s => "call r" + envOut + " := " + name + "(r" + envIn + operandString + ");", new RtlExp[0]));
        }
        else if (destVars.Count == 1 && args.Count == 2 && operands.Count == 2
            && operands[0].Item1 == "inout" && operands[1].Item1 == "in"
            && !strictOperands)
        {
            //- optimized path for binary expressions
            AddBinary(destVars[0], name, args[0], args[1], operands.ConvertAll(o => o.Item2), envIn, envOut);
        }
        else
        {
            List<RtlArg> rtlArgs = new List<RtlArg>();
            int kIn = 0;
            int kOut = 0;
            foreach (var opn in operands)
            {
                RtlExp re = (rtlExps == null) ? null : rtlExps[kIn];
                RtlArg arg;
                switch (opn.Item1)
                {
                    case "in":
                        if (strictOperands && (re == null || re is RtlInt))
                        {
                            var tmp = TempVar(Type.Int);
                            if (re == null) { AddExpression(tmp, args[kIn]); }
                            else { Move(tmp, re, false); }
                            arg = new RtlArg(true, false, tmp);
                        }
                        else
                        {
                            arg = new RtlArg(true, false, re != null ? re : AsSimpleOrTemp(args[kIn]));
                        }
                        kIn++;
                        break;
                    case "inout":
                        if (re == null) { AddExpression(destVars[kOut], args[kIn]); }
                        else { Move(destVars[kOut], re, false); }
                        kIn++;
                        arg = new RtlArg(true, true, destVars[kOut++]);
                        break;
                    case "out": arg = new RtlArg(false, true, destVars[kOut++]); break;
                    case "mem": arg = new RtlArg(true, false, re != null ? re : AsRtlMem(args[kIn])); kIn++; break;
                    default: throw new Exception("expected 'in', 'inout', 'out', or 'mem' on instruction attributes");
                }
                arg.pinReg = opn.Item2;
                rtlArgs.Add(arg);
            }
            stmts.Add(new RtlInst(name, rtlArgs, false, envIn, envOut));
        }
    }