		Search-engine friendly clone of the ACL2 documentation.

Programming

Errors

Support for causing runtime errors, breaks, assertions, etc.

Subtopics

Value-triple: Compute a value, optionally checking that it is not nil
Error-checking: A library of utilities for error checking.
Assert-event: Assert that a given form returns a non-nil value
Er: Print an error message and ``cause an error''
Error-triple: A common ACL2 programming idiom
Set-inhibit-er-soft: Control the error output
Hard-error: Print an error message and stop execution
Must-fail: A top-level assert$-like command. Ensures that a command which returns an error-triple—e.g., defun or defthm—will not be successful.
Breaks: Common Lisp breaks
Assert!-stobj: Variant of assert! and assert-event allowing stobjs
Ctxp: Recognizer for context objects for error messages
Must-eval-to: A top-level assert$-like command to ensure that a form evaluates to a non-erroneous error triple with the value of a specified expression.
Ctx: Context object for error messages
Assert!: Event variant of assert$ that abbreviates assert-event
Must-succeed: A top-level assert$-like command. Ensures that a command which returns an error-triple—e.g., a defun or defthm—will return successfully.
Assert$: Cause a hard error if the given test is false
Illegal: Print an error message and stop execution
Er-progn: Perform a sequence of state-changing ``error triples''
Error1: Print an error message and cause a ``soft error''
Toggle-inhibit-er-soft: Add or delete an error output string from the inhibit-er-soft-table
Must-succeed*: A variant of must-succeed that accepts multiple forms.
Assert*: Create a guard proof obligation that given test holds
Assert?: A variation of assert$ with customizable context and message.
Er-soft+: Print an error message and ``cause an error''
Must-fail-with-soft-error: A specialization of must-fail to ensure that a soft error occurs.
Must-fail-with-hard-error: A specialization of must-fail to ensure that a hard error occurs.
Must-fail-with-error: A specialization of must-fail to ensure that an error occurs.
Break$: Cause an immediate Lisp break
Must-eval-to-t: A specialization of must-eval-to to ensure that a form evaluates to a non-erroneous error triple with value t.
Er-soft-logic: Print an error message and ``cause an error''
Convert-soft-error: Convert a soft error to have a specified (mv erp val state)
Er-soft: Print an error message and ``cause a soft error''
Toggle-inhibit-er-soft!: Toggle an inhibit-er-soft-table entry non-locally
Set-inhibit-er-soft!: Control error output non-locally
Must-not-prove: A top-level assert$-like command to ensure that a formula does not get proved.
Must-prove: A top-level assert$-like command to ensure that a formula gets proved.
Must-fail!: A variant of must-fail suitable for inclusion in books
Must-be-redundant: A top-level assert$-like command to ensure that given forms are redundant.
Must-succeed!: A variant of must-succeed
Must-fail-local: A local variant of must-fail.
Assert-equal: Abbreviation for calling assert! on an equality.