private void generateRevertLogicForCmd()

in Sources/SolToBoogie/RevertLogicGenerator.cs [137:226]
83 lines of code
20 McCabe index (conditional complexity)

        private void generateRevertLogicForCmd(BoogieCmd cmd, BoogieStmtList parent, bool isFail, bool inHarness)
        {
            List<BoogieExpr> dupAndReplaceExprList(List<BoogieExpr> exprs)
            {
                return exprs.Select(e => dupAndReplaceExpr(e, isFail, inHarness)).ToList();
            }
            
            BoogieStmtList dupAndReplaceStmList(BoogieStmtList stmtList)
            {
                if (stmtList == null)
                    return null;

                BoogieStmtList newList = new BoogieStmtList();
                stmtList.BigBlocks[0].SimpleCmds.ForEach(c => generateRevertLogicForCmd(c, newList, isFail, inHarness));
                return newList;
            }
            
            if (cmd is BoogieAssignCmd assignCmd)
            {
                parent.AddStatement(new BoogieAssignCmd(dupAndReplaceExpr(assignCmd.Lhs, isFail, inHarness),
                                                        dupAndReplaceExpr(assignCmd.Rhs, isFail, inHarness)));
            }
            else if (cmd is BoogieCallCmd callCmd)
            {
                string calleeName = callCmd.Callee;
                bool emitCheckRevertLogic = false;
                if (!isHarnessProcudure(calleeName) && procsWiltImplNames.Contains(calleeName))
                {
                    if (!inHarness || !isPublic(proceduresInProgram[calleeName]))
                    {
                        emitCheckRevertLogic = !inHarness && !catchesExceptions(calleeName);
                        calleeName = calleeName + (isFail ? "__fail" : "__success");
                    }
                }

                var newIns = callCmd.Ins != null ? dupAndReplaceExprList(callCmd.Ins) : null;
                var newOuts = callCmd.Outs?.Select(e => (BoogieIdentifierExpr) dupAndReplaceExpr(e, isFail, inHarness)).ToList();
                parent.AddStatement(new BoogieCallCmd(calleeName, newIns, newOuts));

                if (emitCheckRevertLogic)
                {
                    BoogieStmtList thenBody = new BoogieStmtList();
                    thenBody.AddStatement(new BoogieReturnCmd());

                    parent.AddStatement(new BoogieIfCmd(new BoogieIdentifierExpr("revert"), thenBody, null));
                }
            }
            else if (cmd is BoogieAssertCmd assertCmd)
            {
                if (!isFail)
                {
                    parent.AddStatement(new BoogieAssertCmd(dupAndReplaceExpr(assertCmd.Expr, false, inHarness), assertCmd.Attributes));
                }
            }
            else if (cmd is BoogieAssumeCmd assumeCmd)
            {
                parent.AddStatement(new BoogieAssumeCmd(dupAndReplaceExpr(assumeCmd.Expr, isFail, inHarness)));
            }
            else if (cmd is BoogieLoopInvCmd loopInvCmd)
            {
                parent.AddStatement(new BoogieLoopInvCmd(dupAndReplaceExpr(loopInvCmd.Expr, isFail, inHarness)));
            }
            else if (cmd is BoogieReturnExprCmd returnExprCmd)
            {
                // This one does not seem to be used.
                parent.AddStatement(new BoogieReturnExprCmd(dupAndReplaceExpr(returnExprCmd.Expr, isFail, inHarness)));
            }
            else if (cmd is BoogieHavocCmd havocCmd)
            {
                parent.AddStatement(new BoogieHavocCmd(havocCmd.Vars.Select(id => (BoogieIdentifierExpr) dupAndReplaceExpr(id, isFail, inHarness)).ToList()));
            }
            else if (cmd is BoogieIfCmd ifCmd)
            {
                parent.AddStatement(new BoogieIfCmd(dupAndReplaceExpr(ifCmd.Guard, isFail, inHarness),
                                       dupAndReplaceStmList(ifCmd.ThenBody),
                                       dupAndReplaceStmList(ifCmd.ElseBody)));
            }
            else if (cmd is BoogieWhileCmd whileCmd)
            {
                var body = dupAndReplaceStmList(whileCmd.Body);
                BoogieStmtList invsAsStmtList = new BoogieStmtList();
                whileCmd.Invariants.ForEach(i => generateRevertLogicForCmd(i, invsAsStmtList, isFail, inHarness));
                List<BoogiePredicateCmd> invs = invsAsStmtList.BigBlocks[0].SimpleCmds.Select(c => (BoogiePredicateCmd) c).ToList();
                parent.AddStatement( new BoogieWhileCmd(dupAndReplaceExpr(whileCmd.Guard, isFail, inHarness), body, invs));
            }
            else
            {
                parent.AddStatement(cmd);
            }
        }