Major Section: TRACE
Trace*
is a minor variant of trace$
, the ACL2 tracing utility.
See trace$ for detailed documentation.
The only difference between trace*
and trace$
is that trace*
provides perhaps more pleasant output, as follows. If a function is traced
without option :entry
or :exit
, then trace*
avoids using the name
of the so-called ``*1* function'' (also known as ``executable-counterpart
function'' or ``logic function'').
The log below illustrates the difference when using
:set-guard-checking :none
, which restricts execution to *1* functions.
Here we assume the following definition.
(defun fact (n) (if (zp n) 1 (* n (fact (1- n)))))And here is the log promised above, first showing
trace$
and then the
(prettier output from) trace*
.
ACL2 >(trace$ fact) ((FACT)) ACL2 >(fact 3) 1> (ACL2_*1*_ACL2::FACT 3) 2> (ACL2_*1*_ACL2::FACT 2) 3> (ACL2_*1*_ACL2::FACT 1) 4> (ACL2_*1*_ACL2::FACT 0) <4 (ACL2_*1*_ACL2::FACT 1) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 2) <1 (ACL2_*1*_ACL2::FACT 6) 6 ACL2 >(trace* fact) ((FACT :ENTRY (CONS 'FACT ARGLIST) :EXIT (CONS 'FACT VALUES))) ACL2 >(fact 3) 1> (FACT 3) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (FACT 6) 6 ACL2 >