Fmx-cw
(fmx-cw str &rest args) => state
Fmx-cw is a variant of cw: both take the same arguments
and have the same behavior on well-formed input, and both return nil.
See cw for documentation on how to use both utilities. Unlike cw,
which has a guard of t, fmx-cw has a non-trivial guard that
can can catch errors in the use of tilde-directives. Here is an example of
such a guard violation, where the corresponding call of cw would instead
cause a hard error.
ACL2 !>(fmx-cw "Hello ~s0." '(world))
ACL2 Error in TOP-LEVEL: Guard violation for FMX-CW-FN:
Illegal Fmt Syntax. The tilde-s directive at position 6 of the string
below is illegal because its variable evaluated to (WORLD), which is
not a symbol, a string, or a number.
"Hello ~s0."
ACL2 !>
Thus, call fmx-cw instead of cw in the body of :logic mode definition when you want its guard verification to help
ensure the absence of runtime errors from that call. Note that if you call
fmx-cw in a definition, the guard proof may benefit from the lemma,
fmx-cw-msg-1-opener, found in community-book
books/system/fmx-cw.lisp.
The variant fmx!-cw avoids the insertion of backslash () characters
when forced to print past the right margin. Thus, use fmx!-cw instead of
fmx-cw if you want the output to be machine-readable.
