• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
        • Syntax-for-tools
        • Atc
        • Transformation-tools
        • Language
          • Abstract-syntax
          • Integer-ranges
          • Implementation-environments
          • Dynamic-semantics
            • Exec-expr
            • Exec
            • Exec-arrsub
            • Variable-resolution-preservation
            • Init-value-to-value
            • Apconvert-expr-value
            • Execution-limit-monotonicity
              • Exec-2limits
                • Exec-expr-list-2limits
                • Exec-stmt-while-2limits
                • Exec-stmt-dowhile-2limits
                • Exec-obj-declon-2limits
                • Exec-initer-2limits
                • Exec-fun-2limits
                • Exec-block-item-list-2limits
                • Exec-block-item-2limits
                • Exec-stmt-2limits
                • Exec-expr-2limits
              • Exec-monotone
              • Exec-2limits-to-exec
            • Exec-memberp
            • Exec-stmt
            • Exec-address
            • Init-scope
            • Exec-unary
            • Exec-member
            • Exec-fun
            • Exec-stmt-while
            • Eval-iconst
            • Exec-binary-strict-pure
            • Variable-visibility-preservation
            • Object-type-preservation
            • Eval-binary-strict-pure
            • Exec-block-item-list
            • Exec-indir
            • Exec-ident
            • Exec-block-item
            • Eval-cast
            • Frame-and-scope-peeling
            • Exec-expr-list
            • Exec-obj-declon
            • Exec-cast
            • Exec-const
            • Eval-unary
            • Exec-stmt-dowhile
            • Exec-initer
            • Eval-const
            • Execution-without-function-calls
          • Static-semantics
          • Grammar
          • Types
          • Integer-formats-definitions
          • Computation-states
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
          • Object-designators
          • Operations
          • Errors
          • Tag-environments
          • Function-environments
          • Character-sets
          • Flexible-array-member-removal
          • Arithmetic-operations
          • Pointer-operations
          • Real-operations
          • Array-operations
          • Scalar-operations
          • Structure-operations
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Execution-limit-monotonicity

Exec-2limits

Execution functions with two limits.

This defines the induction schema described in execution-limit-monotonicity. We do not bother verifying the guards or proving return theorems, because we only use this function logically.

Definitions and Theorems

Function: exec-fun-2limits

(defun exec-fun-2limits (fun args compst fenv limit limit1)
  (declare (xargs :guard t))
  (b*
    (((when (or (zp limit1) (zp limit)))
      (mv (error :limit)
          (compustate-fix compst)))
     (info (fun-env-lookup fun fenv))
     ((when (not info))
      (mv (error (list :function-undefined (ident-fix fun)))
          (compustate-fix compst)))
     ((fun-info info) info)
     (scope (init-scope info.params args))
     ((when (errorp scope))
      (mv scope (compustate-fix compst)))
     (frame (make-frame :function fun
                        :scopes (list scope)))
     (compst (push-frame frame compst))
     ((mv sval compst)
      (exec-block-item-list-2limits info.body compst fenv (1- limit)
                                    (1- limit1)))
     (compst (pop-frame compst))
     ((when (errorp sval)) (mv sval compst))
     (val? (stmt-value-case sval
                            :none nil
                            :return sval.value?))
     ((unless (equal (type-of-value-option val?)
                     (tyname-to-type info.result)))
      (mv (error (list :return-value-mistype
                       :required info.result
                       :supplied (type-of-value-option val?)))
          compst)))
    (mv val? compst)))

Function: exec-expr-2limits

(defun exec-expr-2limits (e compst fenv limit limit1)
 (declare (xargs :guard t))
 (b* (((when (or (zp limit1) (zp limit)))
       (mv (error :limit)
           (compustate-fix compst))))
  (expr-case
   e :ident
   (mv (exec-ident e.get compst)
       (compustate-fix compst))
   :const
   (mv (exec-const e.get)
       (compustate-fix compst))
   :arrsub
   (b* (((unless (and (expr-purep e.arr)
                      (expr-purep e.sub)))
         (mv (error (list :arrsub-nonpure-arg (expr-fix e)))
             (compustate-fix compst)))
        ((mv arr compst)
         (exec-expr-2limits e.arr compst fenv (1- limit)
                            (1- limit1)))
        ((when (errorp arr)) (mv arr compst))
        ((unless arr)
         (mv (error (list :arrsub-void-expr e.arr))
             compst))
        ((mv sub compst)
         (exec-expr-2limits e.sub compst fenv (1- limit)
                            (1- limit1)))
        ((when (errorp sub)) (mv sub compst))
        ((unless sub)
         (mv (error (list :arrsub-void-expr e.sub))
             compst)))
     (mv (exec-arrsub arr sub compst)
         compst))
   :call
   (b* (((unless (expr-list-purep e.args))
         (mv (error (list :call-nonpure-args (expr-fix e)))
             (compustate-fix compst)))
        ((mv vals compst)
         (exec-expr-list-2limits e.args compst fenv (1- limit)
                                 (1- limit1)))
        ((when (errorp vals)) (mv vals compst))
        ((mv val? compst)
         (exec-fun-2limits e.fun vals compst fenv (1- limit)
                           (1- limit1)))
        ((when (errorp val?)) (mv val? compst)))
     (if val? (mv (make-expr-value :value val?
                                   :object nil)
                  compst)
       (mv nil compst)))
   :member
   (b* (((mv str compst)
         (exec-expr-2limits e.target compst fenv (1- limit)
                            (1- limit1)))
        ((when (errorp str)) (mv str compst))
        ((unless str)
         (mv (error (list :member-void-expr (expr-fix e)))
             compst)))
     (mv (exec-member str e.name) compst))
   :memberp
   (b* (((mv str compst)
         (exec-expr-2limits e.target compst fenv (1- limit)
                            (1- limit1)))
        ((when (errorp str)) (mv str compst))
        ((unless str)
         (mv (error (list :memberp-void-expr (expr-fix e)))
             compst)))
     (mv (exec-memberp str e.name compst)
         compst))
   :postinc
   (mv (error (list :expression-not-supported (expr-fix e)))
       (compustate-fix compst))
   :postdec
   (mv (error (list :expression-not-supported (expr-fix e)))
       (compustate-fix compst))
   :preinc
   (mv (error (list :expression-not-supported (expr-fix e)))
       (compustate-fix compst))
   :predec
   (mv (error (list :expression-not-supported (expr-fix e)))
       (compustate-fix compst))
   :unary
   (b* (((mv arg compst)
         (exec-expr-2limits e.arg compst fenv (1- limit)
                            (1- limit1)))
        ((when (errorp arg)) (mv arg compst))
        ((unless arg)
         (mv (error (list :unary-void-expr e.arg))
             compst)))
     (mv (exec-unary e.op arg compst)
         compst))
   :cast
   (b* (((mv arg compst)
         (exec-expr-2limits e.arg compst fenv (1- limit)
                            (1- limit1)))
        ((when (errorp arg)) (mv arg compst))
        ((unless arg)
         (mv (error (list :cast-void-expr e.arg))
             compst)))
     (mv (exec-cast e.type arg) compst))
   :binary
   (cond
    ((and (binop-strictp e.op)
          (binop-purep e.op))
     (b*
      (((unless (and (expr-purep e.arg1)
                     (expr-purep e.arg2)))
        (mv
          (error
               (list :pure-strict-binary-nonpure-args (expr-fix e)))
          (compustate-fix compst)))
       ((mv arg1-eval compst)
        (exec-expr-2limits e.arg1 compst fenv (1- limit)
                           (1- limit1)))
       ((when (errorp arg1-eval))
        (mv arg1-eval compst))
       ((unless arg1-eval)
        (mv (error (list :binary-void-expr e.arg1))
            compst))
       ((mv arg2-eval compst)
        (exec-expr-2limits e.arg2 compst fenv (1- limit)
                           (1- limit1)))
       ((when (errorp arg2-eval))
        (mv arg2-eval compst))
       ((unless arg2-eval)
        (mv (error (list :binary-void-expr e.arg2))
            compst)))
      (mv (exec-binary-strict-pure e.op arg1-eval arg2-eval)
          compst)))
    ((binop-case e.op :logand)
     (b* (((mv arg1-eval compst)
           (exec-expr-2limits e.arg1 compst fenv (1- limit)
                              (1- limit1)))
          ((when (errorp arg1-eval))
           (mv arg1-eval compst))
          ((unless arg1-eval)
           (mv (error (list :logand-void-arg (expr-fix e)))
               compst))
          (arg1 (apconvert-expr-value arg1-eval))
          ((when (errorp arg1)) (mv arg1 compst))
          (test1 (test-value (expr-value->value arg1)))
          ((when (errorp test1))
           (mv test1 compst))
          ((when (not test1))
           (mv (make-expr-value :value (value-sint 0)
                                :object nil)
               compst))
          ((mv arg2-eval compst)
           (exec-expr-2limits e.arg2 compst fenv (1- limit)
                              (1- limit1)))
          ((when (errorp arg2-eval))
           (mv arg2-eval compst))
          ((unless arg2-eval)
           (mv (error (list :logand-void-arg (expr-fix e)))
               compst))
          (arg2 (apconvert-expr-value arg2-eval))
          ((when (errorp arg2)) (mv arg2 compst))
          (test2 (test-value (expr-value->value arg2)))
          ((when (errorp test2))
           (mv test2 compst)))
       (if test2 (mv (make-expr-value :value (value-sint 1)
                                      :object nil)
                     compst)
         (mv (make-expr-value :value (value-sint 0)
                              :object nil)
             compst))))
    ((binop-case e.op :logor)
     (b* (((mv arg1-eval compst)
           (exec-expr-2limits e.arg1 compst fenv (1- limit)
                              (1- limit1)))
          ((when (errorp arg1-eval))
           (mv arg1-eval compst))
          ((unless arg1-eval)
           (mv (error (list :logor-void-arg (expr-fix e)))
               compst))
          (arg1 (apconvert-expr-value arg1-eval))
          ((when (errorp arg1)) (mv arg1 compst))
          (test1 (test-value (expr-value->value arg1)))
          ((when (errorp test1))
           (mv test1 compst))
          ((when test1)
           (mv (make-expr-value :value (value-sint 1)
                                :object nil)
               compst))
          ((mv arg2-eval compst)
           (exec-expr-2limits e.arg2 compst fenv (1- limit)
                              (1- limit1)))
          ((when (errorp arg2-eval))
           (mv arg2-eval compst))
          ((unless arg2-eval)
           (mv (error (list :logor-void-arg (expr-fix e)))
               compst))
          (arg2 (apconvert-expr-value arg2-eval))
          ((when (errorp arg2)) (mv arg2 compst))
          (test2 (test-value (expr-value->value arg2)))
          ((when (errorp test2))
           (mv test2 compst)))
       (if test2 (mv (make-expr-value :value (value-sint 1)
                                      :object nil)
                     compst)
         (mv (make-expr-value :value (value-sint 0)
                              :object nil)
             compst))))
    ((binop-case e.op :asg)
     (b* ((left (expr-binary->arg1 e))
          (right (expr-binary->arg2 e))
          ((unless (expr-purep left))
           (mv (error (list :asg-left-nonpure (expr-fix e)))
               (compustate-fix compst)))
          ((unless (or (expr-case left :ident)
                       (expr-purep right)))
           (mv (error (list :asg-right-nonpure (expr-fix e)))
               (compustate-fix compst)))
          ((mv left-eval compst)
           (exec-expr-2limits left compst fenv (1- limit)
                              (1- limit1)))
          ((when (errorp left-eval))
           (mv left-eval compst))
          ((unless left-eval)
           (mv (error (list :asg-left-void (expr-fix e)))
               compst))
          (left-eval (apconvert-expr-value left-eval))
          ((when (errorp left-eval))
           (mv left-eval compst))
          (objdes (expr-value->object left-eval))
          ((unless objdes)
           (mv (error (list :asg-not-lvalue left))
               compst))
          ((mv right-eval compst)
           (exec-expr-2limits right compst fenv (1- limit)
                              (1- limit1)))
          ((when (errorp right-eval))
           (mv right-eval compst))
          ((when (not right-eval))
           (mv (error (list :asg-right-void right))
               compst))
          (right-eval (apconvert-expr-value right-eval))
          ((when (errorp right-eval))
           (mv right-eval compst))
          (val (expr-value->value right-eval))
          (compst/error (write-object objdes val compst))
          ((when (errorp compst/error))
           (mv compst/error compst))
          (compst compst/error))
       (mv (make-expr-value :value val :object nil)
           compst)))
    (t (mv (error (list :expression-not-supported (expr-fix e)))
           (compustate-fix compst))))
   :cond
   (b* (((mv test compst)
         (exec-expr-2limits e.test compst fenv (1- limit)
                            (1- limit1)))
        ((when (errorp test)) (mv test compst))
        ((unless test)
         (mv (error (list :cond-void-test (expr-fix e)))
             compst))
        (test (apconvert-expr-value test))
        ((when (errorp test)) (mv test compst))
        (test (test-value (expr-value->value test)))
        ((when (errorp test)) (mv test compst)))
     (if test (b* (((mv eval compst)
                    (exec-expr-2limits e.then compst fenv (1- limit)
                                       (1- limit1)))
                   ((when (errorp eval)) (mv eval compst))
                   ((unless eval)
                    (mv (error (list :cond-void-then (expr-fix e)))
                        compst))
                   (eval (apconvert-expr-value eval))
                   ((when (errorp eval)) (mv eval compst)))
                (mv (change-expr-value eval :object nil)
                    compst))
       (b* (((mv eval compst)
             (exec-expr-2limits e.else compst fenv (1- limit)
                                (1- limit1)))
            ((when (errorp eval)) (mv eval compst))
            ((unless eval)
             (mv (error (list :cond-void-else (expr-fix e)))
                 compst))
            (eval (apconvert-expr-value eval))
            ((when (errorp eval)) (mv eval compst)))
         (mv (change-expr-value eval :object nil)
             compst)))))))

Function: exec-expr-list-2limits

(defun exec-expr-list-2limits (es compst fenv limit limit1)
  (declare (xargs :guard (and (expr-listp es)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit)
                              (natp limit1))))
  (b* (((when (zp limit))
        (mv (error :limit)
            (compustate-fix compst)))
       ((when (endp es))
        (mv nil (compustate-fix compst)))
       ((mv eval compst)
        (exec-expr-2limits (car es)
                           compst fenv (1- limit)
                           (1- limit1)))
       ((when (errorp eval)) (mv eval compst))
       ((unless eval)
        (mv (error (list :void-expr-in-list (expr-fix (car es))))
            compst))
       (eval (apconvert-expr-value eval))
       ((when (errorp eval)) (mv eval compst))
       (val (expr-value->value eval))
       ((mv vals compst)
        (exec-expr-list-2limits (cdr es)
                                compst fenv (1- limit)
                                (1- limit1)))
       ((when (errorp vals)) (mv vals compst)))
    (mv (cons val vals) compst)))

Function: exec-stmt-2limits

(defun exec-stmt-2limits (s compst fenv limit limit1)
 (declare (xargs :guard t))
 (b* (((when (or (zp limit1) (zp limit)))
       (mv (error :limit)
           (compustate-fix compst)))
      (s (stmt-fix s)))
  (stmt-case
    s :labeled
    (mv (error (list :exec-stmt s))
        (compustate-fix compst))
    :compound
    (b*
      ((compst (enter-scope compst))
       ((mv sval compst)
        (exec-block-item-list-2limits s.items compst fenv (1- limit)
                                      (1- limit1))))
      (mv sval (exit-scope compst)))
    :expr
    (b* (((mv eval compst)
          (exec-expr-2limits s.get compst fenv (1- limit)
                             (1- limit1)))
         ((when (errorp eval)) (mv eval compst)))
      (mv (stmt-value-none) compst))
    :null
    (mv (stmt-value-none)
        (compustate-fix compst))
    :if
    (b* (((mv test compst)
          (exec-expr-2limits s.test compst fenv (1- limit)
                             (1- limit1)))
         ((when (errorp test)) (mv test compst))
         ((unless test)
          (mv (error (list :void-if-test s.test))
              compst))
         (test (apconvert-expr-value test))
         ((when (errorp test)) (mv test compst))
         (test (expr-value->value test))
         (test (test-value test))
         ((when (errorp test)) (mv test compst)))
      (if test (exec-stmt-2limits s.then compst fenv (1- limit)
                                  (1- limit1))
        (mv (stmt-value-none) compst)))
    :ifelse
    (b* (((mv test compst)
          (exec-expr-2limits s.test compst fenv (1- limit)
                             (1- limit1)))
         ((when (errorp test)) (mv test compst))
         ((unless test)
          (mv (error (list :void-ifelse-test s.test))
              compst))
         (test (apconvert-expr-value test))
         ((when (errorp test)) (mv test compst))
         (test (expr-value->value test))
         (test (test-value test))
         ((when (errorp test)) (mv test compst)))
      (if test (exec-stmt-2limits s.then compst fenv (1- limit)
                                  (1- limit1))
        (exec-stmt-2limits s.else compst fenv (1- limit)
                           (1- limit1))))
    :switch
    (mv (error (list :exec-stmt s))
        (compustate-fix compst))
    :while
    (exec-stmt-while-2limits s.test s.body compst fenv (1- limit)
                             (1- limit1))
    :dowhile
    (b* ((compst (enter-scope compst))
         ((mv sval compst)
          (exec-stmt-dowhile-2limits
               s.body s.test compst fenv (1- limit)
               (1- limit1)))
         ((when (errorp sval))
          (mv sval (exit-scope compst)))
         (compst (exit-scope compst)))
      (mv sval compst))
    :for
    (mv (error (list :exec-stmt s))
        (compustate-fix compst))
    :goto
    (mv (error (list :exec-stmt s))
        (compustate-fix compst))
    :continue
    (mv (error (list :exec-stmt s))
        (compustate-fix compst))
    :break
    (mv (error (list :exec-stmt s))
        (compustate-fix compst))
    :return
    (if (exprp s.value)
        (b* (((mv eval? compst)
              (exec-expr-2limits s.value compst fenv (1- limit)
                                 (1- limit1)))
             ((when (errorp eval?))
              (mv eval? compst))
             ((when (not eval?))
              (mv (error (list :return-void-expr s.value))
                  compst))
             (eval eval?)
             (eval (apconvert-expr-value eval))
             ((when (errorp eval)) (mv eval compst))
             (val (expr-value->value eval)))
          (mv (stmt-value-return val) compst))
      (mv (stmt-value-return nil)
          (compustate-fix compst))))))

Function: exec-stmt-while-2limits

(defun exec-stmt-while-2limits (test body compst fenv limit limit1)
  (declare (xargs :guard t))
  (b* (((when (or (zp limit1) (zp limit)))
        (mv (error :limit)
            (compustate-fix compst)))
       ((mv test-eval compst)
        (exec-expr-2limits test compst fenv (1- limit)
                           (1- limit1)))
       ((when (errorp test-eval))
        (mv test-eval compst))
       ((unless test-eval)
        (mv (error (list :void-while-test (expr-fix test)))
            compst))
       (test-eval (apconvert-expr-value test-eval))
       ((when (errorp test-eval))
        (mv test-eval compst))
       (test-val (expr-value->value test-eval))
       (continuep (test-value test-val))
       ((when (errorp continuep))
        (mv continuep compst))
       ((when (not continuep))
        (mv (stmt-value-none) compst))
       ((mv sval compst)
        (exec-stmt-2limits body compst fenv (1- limit)
                           (1- limit1)))
       ((when (errorp sval)) (mv sval compst))
       ((when (stmt-value-case sval :return))
        (mv sval compst)))
    (exec-stmt-while-2limits test body compst fenv (1- limit)
                             (1- limit1))))

Function: exec-stmt-dowhile-2limits

(defun exec-stmt-dowhile-2limits
       (body test compst fenv limit limit1)
  (declare (xargs :guard t))
  (b* (((when (or (zp limit1) (zp limit)))
        (mv (error :limit)
            (compustate-fix compst)))
       (compst (enter-scope compst))
       ((mv sval compst)
        (exec-stmt-2limits body compst fenv (1- limit)
                           (1- limit1)))
       ((when (errorp sval))
        (mv sval (exit-scope compst)))
       (compst (exit-scope compst))
       ((when (stmt-value-case sval :return))
        (mv sval compst))
       ((mv test-eval compst)
        (exec-expr-2limits test compst fenv (1- limit)
                           (1- limit1)))
       ((when (errorp test-eval))
        (mv test-eval compst))
       ((unless test-eval)
        (mv (error (list :void-dowhile-test (expr-fix test)))
            compst))
       (test-eval (apconvert-expr-value test-eval))
       ((when (errorp test-eval))
        (mv test-eval compst))
       (test-val (expr-value->value test-eval))
       (continuep (test-value test-val))
       ((when (errorp continuep))
        (mv continuep compst))
       ((when (not continuep))
        (mv (stmt-value-none) compst)))
    (exec-stmt-dowhile-2limits body test compst fenv (1- limit)
                               (1- limit1))))

Function: exec-initer-2limits

(defun exec-initer-2limits (initer compst fenv limit limit1)
 (declare (xargs :guard t))
 (b* (((when (or (zp limit1) (zp limit)))
       (mv (error :limit)
           (compustate-fix compst))))
  (initer-case
     initer :single
     (b* (((mv eval compst)
           (exec-expr-2limits initer.get compst fenv (1- limit)
                              (1- limit1)))
          ((when (errorp eval)) (mv eval compst))
          ((when (not eval))
           (mv (error (list :void-initializer (initer-fix initer)))
               compst))
          (eval (apconvert-expr-value eval))
          ((when (errorp eval)) (mv eval compst))
          (val (expr-value->value eval))
          (ival (init-value-single val)))
       (mv ival compst))
     :list
     (b* (((unless (or (<= (len initer.get) 1)
                       (expr-list-purep initer.get)))
           (mv (error (list :non-pure-initer (initer-fix initer)))
               (compustate-fix compst)))
          ((mv vals compst)
           (exec-expr-list-2limits initer.get compst fenv (1- limit)
                                   (1- limit1)))
          ((when (errorp vals)) (mv vals compst))
          (ival (init-value-list vals)))
       (mv ival compst)))))

Function: exec-obj-declon-2limits

(defun exec-obj-declon-2limits (declon compst fenv limit limit1)
  (declare (xargs :guard t))
  (b* (((when (or (zp limit1) (zp limit)))
        (error :limit))
       ((mv var scspec tyname init?)
        (obj-declon-to-ident+scspec+tyname+init declon))
       ((unless (scspecseq-case scspec :none))
        (error :unsupported-storage-class-specifier))
       (type (tyname-to-type tyname))
       ((when (type-case type :array))
        (error :unsupported-local-array))
       ((when (not init?))
        (error :unsupported-no-initializer))
       (init init?)
       ((mv ival compst)
        (exec-initer-2limits init compst fenv (1- limit)
                             (1- limit1)))
       ((when (errorp ival)) ival)
       (val (init-value-to-value type ival))
       ((when (errorp val)) val))
    (create-var var val compst)))

Function: exec-block-item-2limits

(defun exec-block-item-2limits (item compst fenv limit limit1)
 (declare (xargs :guard t))
 (b* (((when (or (zp limit1) (zp limit)))
       (mv (error :limit)
           (compustate-fix compst))))
  (block-item-case
    item :declon
    (b*
      ((new-compst
            (exec-obj-declon-2limits item.get compst fenv (1- limit)
                                     (1- limit1)))
       ((when (errorp new-compst))
        (mv new-compst (compustate-fix compst))))
      (mv (stmt-value-none) new-compst))
    :stmt (exec-stmt-2limits item.get compst fenv (1- limit)
                             (1- limit1)))))

Function: exec-block-item-list-2limits

(defun exec-block-item-list-2limits (items compst fenv limit limit1)
  (declare (xargs :guard t))
  (b* (((when (or (zp limit1) (zp limit)))
        (mv (error :limit)
            (compustate-fix compst)))
       ((when (endp items))
        (mv (stmt-value-none)
            (compustate-fix compst)))
       ((mv sval compst)
        (exec-block-item-2limits (car items)
                                 compst fenv (1- limit)
                                 (1- limit1)))
       ((when (errorp sval)) (mv sval compst))
       ((when (stmt-value-case sval :return))
        (mv sval compst)))
    (exec-block-item-list-2limits (cdr items)
                                  compst fenv (1- limit)
                                  (1- limit1))))

Subtopics

Exec-expr-list-2limits

Exec-stmt-while-2limits

Exec-stmt-dowhile-2limits

Exec-obj-declon-2limits

Exec-initer-2limits

Exec-fun-2limits

Exec-block-item-list-2limits

Exec-block-item-2limits

Exec-stmt-2limits

Exec-expr-2limits