• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
          • Atj
            • Atj-implementation
              • Atj-types
              • Atj-java-primitive-array-model
              • Atj-java-abstract-syntax
              • Atj-input-processing
              • Atj-java-pretty-printer
              • Atj-code-generation
                • Atj-gen-test-method
                • Atj-shallow-code-generation
                • Atj-common-code-generation
                • Atj-shallow-quoted-constant-generation
                • Atj-pre-translation
                • Atj-gen-everything
                • Atj-name-translation
                • Atj-gen-test-cunit
                • Atj-gen-test-class
                • Atj-gen-main-file
                • Atj-post-translation
                  • Atj-post-translation-remove-array-write-calls
                  • Atj-post-translation-cache-const-methods
                  • Atj-post-translation-tailrec-elimination
                  • Atj-post-translation-fold-returns
                  • Atj-post-translate-body
                  • Atj-post-translation-lift-loop-tests
                  • Atj-post-translation-simplify-conds
                  • Atj-post-translate-jcbody-elements
                  • Atj-post-translation-remove-continue
                    • Atj-remove-ending-continue
                    • Atj-remove-continue-in-jstatems+jblocks
                • Atj-deep-code-generation
                • Atj-gen-test-methods
                • Atj-gen-test-file
                • Atj-gen-env-file
                • Atj-gen-output-subdir
              • Atj-java-primitives
              • Atj-java-primitive-arrays
              • Atj-type-macros
              • Atj-java-syntax-operations
              • Atj-fn
              • Atj-library-extensions
              • Atj-java-input-types
              • Atj-test-structures
              • Aij-notions
              • Atj-macro-definition
            • Atj-tutorial
          • Aij
          • Language
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Atj-post-translation

Atj-post-translation-remove-continue

Post-translation step: remove unnecessary continue statements.

The tail recursion elimination step produces loops where the recursive calls are replaced with continue statements. However, when one of these statements is the last thing executed in the loop body, it is superfluous and can be removed.

This post-translation step performs this removal.

Subtopics

Atj-remove-ending-continue
Remove any ending continue statements from a block that forms a loop body.
Atj-remove-continue-in-jstatems+jblocks
Remove the ending continue statements in all the loops found in statements and blocks.