void Jump()

in ironclad-apps/tools/DafnyCC/CompileMethod.cs [251:338]
88 lines of code
37 McCabe index (conditional complexity)

    void Jump(string label, Expression exp, bool jumpIf = true)
    {
        exp = GetExp(exp);
        RtlExp e = AsSimple(exp);
        BinaryExpr binary = exp as BinaryExpr;
        UnaryExpr unary = exp as UnaryExpr;
        MemberSelectExpr memberSelect = exp as MemberSelectExpr;
        if (e != null)
        {
            Jump(label, new RtlBinary(jumpIf ? "!=" : "==", e, new RtlInt(0)));
        }
        else if (binary != null && jumpOps.ContainsKey(binary.Op.ToString()))
        {
            Type t = AppType(binary.E0.Type);
            UserDefinedType ut = t as UserDefinedType;
            if (!t.Equals(AppType(binary.E1.Type)))
            {
                throw new Exception("not supported: comparison of values with different types");
            }
            else if (t is SeqType && (binary.Op == BinaryExpr.Opcode.Eq || binary.Op == BinaryExpr.Opcode.Neq))
            {
                var tmp = TempVar(Type.Bool);
                var m = dafnySpec.GetSeqMethod(AppType(t), "seq_Equal");
                AddCall(new List<RtlVar> { tmp }, false, true, m.Item1,
                    new List<RtlVar> { null, null },
                    new List<Expression> { binary.E0, binary.E1 },
                    m.Item1.Outs, m.Item2);
                jumpIf = (jumpIf == (binary.Op == BinaryExpr.Opcode.Eq));
                Jump(label, new RtlBinary(jumpIf ? "!=" : "==", tmp, new RtlInt(0)));
            }
            else if (t is IntType || t is BoolType || (ut != null && ut.Name == "array"))
            {
                RtlExp e0 = AsSimpleOrTemp(binary.E0);
                RtlExp e1 = AsSimpleOrTemp(binary.E1);
                Jump(label, new RtlBinary(
                    (jumpIf ? jumpOps : jumpOpsNot)[binary.Op.ToString()], e0, e1));
            }
            else
            {
                throw new Exception("not supported: comparison of values of type " + t);
            }
        }
        else if (binary != null && binary.Op == BinaryExpr.Opcode.Iff && jumpIf)
        {
            Jump(label, DafnySpec.MakeBinaryExpr(BinaryExpr.Opcode.Or, BinaryExpr.ResolvedOpcode.Or, Type.Bool,
                DafnySpec.MakeBinaryExpr(BinaryExpr.Opcode.And, BinaryExpr.ResolvedOpcode.And, Type.Bool, binary.E0, binary.E1),
                DafnySpec.MakeBinaryExpr(BinaryExpr.Opcode.And, BinaryExpr.ResolvedOpcode.And, Type.Bool,
                    new UnaryOpExpr(binary.tok, UnaryOpExpr.Opcode.Not, binary.E0),
                    new UnaryOpExpr(binary.tok, UnaryOpExpr.Opcode.Not, binary.E1))), jumpIf);
        }
        else if (binary != null && binary.Op == BinaryExpr.Opcode.Imp)
        {
            Jump(label, DafnySpec.MakeBinaryExpr(BinaryExpr.Opcode.Or, BinaryExpr.ResolvedOpcode.Or, Type.Bool,
                new UnaryOpExpr(binary.tok, UnaryOpExpr.Opcode.Not, binary.E0), binary.E1), jumpIf);
        }
        else if (binary != null && (
                    (binary.Op == BinaryExpr.Opcode.Or && jumpIf)
                 || (binary.Op == BinaryExpr.Opcode.And && !jumpIf)))
        {
            Jump(label, binary.E0, jumpIf);
            Jump(label, binary.E1, jumpIf);
        }
        else if (binary != null && (
                    (binary.Op == BinaryExpr.Opcode.Or && !jumpIf)
                 || (binary.Op == BinaryExpr.Opcode.And && jumpIf)))
        {
            string skip = NewLabel();
            Jump(skip, binary.E0, !jumpIf);
            Jump(label, binary.E1, jumpIf);
            Label(skip);
        } 
        else if (unary != null && unary is UnaryOpExpr && ((UnaryOpExpr)unary).Op == UnaryOpExpr.Opcode.Not)
        {
            Jump(label, unary.E, !jumpIf);
        }
        else if (memberSelect != null && memberSelect.Member is Field && memberSelect.MemberName.EndsWith("?"))
        {
          string constructor = memberSelect.MemberName.Substring(0, memberSelect.MemberName.Length - 1);
            RtlVar e0 = AsVarOrTemp(memberSelect.Obj);
            JumpIfHasType(label, e0, constructor, memberSelect.Obj.Type, jumpIf);
        }
        else
        {
            RtlVar tmp = TempVar(exp.Type);
            AddExpression(tmp, exp);
            Jump(label, new RtlBinary(jumpIf ? "!=" : "==", tmp, new RtlInt(0)));
        }
    }