• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
      • Must-fail
      • Assert!-stobj
      • Must-eval-to
      • Assert!
      • Must-succeed
      • Must-succeed*
      • Assert?
      • Must-fail-with-soft-error
        • Ensure-soft-error
      • Must-fail-with-hard-error
      • Must-fail-with-error
      • Must-eval-to-t
      • Must-prove
      • Must-not-prove
      • Must-not-be-table-key
      • Must-be-redundant
      • Must-fail-local
      • Must-be-table-key
      • Assert-equal
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/testing
• Errors
• Must-fail

Must-fail-with-soft-error

A specialization of must-fail to ensure that a soft error occurs.

Evaluation of (must-fail-with-soft-error <form>) returns without error exactly when evaluation of <form> causes a soft error.

See must-fail for more details, as must-fail-with-soft-error abbreviates must-fail as follows.

Macro: must-fail-with-soft-error

(defmacro must-fail-with-soft-error (form &rest args)
  (list* 'must-fail
         form :expected
         :soft args))

Also see must-fail-with-error and must-fail-with-hard-error.

Subtopics

Ensure-soft-error

Deprecated synonym of must-fail-with-soft-error