7.10.7 Parameter commands

mmc_options option1 option2 ...

This command sets the options that will be passed to ‘mmc’ to compile your query when you use one of the query commands: ‘query’, ‘cc_query’, or ‘io_query’. For example, if a query results in a compile error, it may sometimes be helpful to use ‘mmc_options --verbose-error-messages’.

printlevel none

Sets the default print level to ‘none’.

printlevel some

Sets the default print level to ‘some’.

printlevel all

Sets the default print level to ‘all’.

printlevel

Reports the current default print level.

scroll on

Turns on user control over the scrolling of sequences of event reports. This means that every screenful of event reports will be followed by a ‘--more--’ prompt. You may type an empty line, which allows the debugger to continue to print the next screenful of event reports. By typing a line that starts with ‘a’, ‘s’ or ‘n’, you can override the print level of the current command, setting it to ‘all’, ‘some’ or ‘none’ respectively. By typing a line that starts with ‘q’, you can abort the current debugger command and get back control at the next event.

scroll off

Turns off user control over the scrolling of sequences of event reports.

scroll size

Sets the scroll window size to size, which tells scroll control to stop and print a ‘--more--’ prompt after every size − 1 events. The default value of size is the value of the ‘LINES’ environment variable, which should correspond to the number of lines available on the terminal.

scroll

Reports whether user scroll control is enabled and what the window size is.

stack_default_limit size

Set the default number of lines printed by the ‘stack’ and ‘nondet_stack’ commands to size. If size is zero, the limit is disabled.

goal_paths on

Turns on printing of goal paths at events.

goal_paths off

Turns off printing of goal paths at events.

goal_paths

Reports whether goal paths are printed at events.

scope all

Sets the default scope of new breakpoints to “all”, i.e. by default, new breakpoints on procedures will stop at all events in the procedure.

scope interface

Sets the default scope of new breakpoints to “interface”, i.e. by default, new breakpoints on procedures will stop at all interface events in the procedure.

scope entry

Sets the default scope of new breakpoints to “entry”, i.e. by default, new breakpoints on procedures will stop only at events representing calls to the procedure.

scope

Reports the current default scope of new breakpoints.

echo on

Turns on the echoing of commands.

echo off

Turns off the echoing of commands.

echo

Reports whether commands are being echoed or not.

context none

When reporting events or ancestor levels, does not print contexts (filename/line number pairs).

context before

When reporting events or ancestor levels, prints contexts (filename/line number pairs) before the identification of the event or call to which they refer, on the same line. With long fully qualified predicate and function names, this may make the line wrap around.

context after

When reporting events or ancestor levels, prints contexts (filename/line number pairs) after the identification of the event or call to which they refer, on the same line. With long fully qualified predicate and function names, this may make the line wrap around.

context prevline

When reporting events or ancestor levels, prints contexts (filename/line number pairs) on a separate line before the identification of the event or call to which they refer.

context nextline

When reporting events or ancestor levels, prints contexts (filename/line number pairs) on a separate line after the identification of the event or call to which they refer.

context

Reports where contexts are being printed.

user_event_context none

When reporting user-defined events, does not print either filename/line number pairs or procedure ids.

user_event_context file

When reporting user-defined events, prints only filename/line number pairs, not procedure ids.

user_event_context proc

When reporting user-defined events, prints only procedure ids, not filename/line number pairs.

user_event_context full

When reporting user-defined events, prints both filename/line number pairs and procedure ids.

user_event_context

Reports what parts of the context are being printed at user events.

list_context_lines num

Sets the number of lines to be printed by the ‘list’ command printed before and after the target context.

list_context_lines

Prints the number of lines to be printed by the ‘list’ command printed before and after the target context.

list_path dir1 dir2 ...

The ‘list’ command searches a list of directories when looking for a source code file. The ‘list_path’ command sets the search path to the given list of directories.

list_path

When invoked without arguments, the ‘list_path’ command prints the search path consulted by the ‘list’ command.

push_list_dir dir1 dir2 ...

Pushes the given directories on to the search path consulted by the ‘list’ command.

pop_list_dir

Pops the leftmost (most recently pushed) directory from the search path consulted by the ‘list’ command.

fail_trace_counts filename

The declarative debugger can exploit information about the failing and passing test cases to ask better questions. This command tells the ‘dice’ command that filename contains execution trace counts from failing test cases. The ‘dice’ command will use this file unless this is overridden with its ‘--fail-trace-counts’ option.

fail_trace_counts

Prints the name of the file containing execution trace counts from failing test cases, if this has already been set.

pass_trace_counts filename

The declarative debugger can exploit information about the failing and passing test cases to ask better questions. This command tells the ‘dice’ command that filename contains execution trace counts from passing test cases. The ‘dice’ command will use this file unless this is overridden with its ‘--pass-trace-counts’ option.

pass_trace_counts

Prints the name of the file containing execution trace counts from passing test cases, if this has already been set.

max_io_actions num

Set the maximum number of I/O actions to print in questions from the declarative debugger to num.

max_io_actions

Prints the maximum number of I/O actions to print in questions from the declarative debugger.

xml_browser_cmd command

Set the shell command used to launch an XML browser to command. If you want a stylesheet to be applied to the XML before the browser is invoked, then you should do that in this command using the appropriate program (such as xsltproc, which comes with libxslt and is available from http://xmlsoft.org/XSLT/). By default if xsltproc and mozilla (or firefox) are available, xsltproc is invoked to apply the xul_tree.xsl stylesheet in extras/xml_stylesheets, then mozilla is invoked on the resulting XUL file.

You can use the apostrophe character (') to quote the command string, for example "xml_browser_cmd 'firefox file:///tmp/mdbtmp.xml'".

xml_browser_cmd

Prints the shell command used to launch an XML browser, if this has been set.

xml_tmp_filename filename

Tells the debugger to dump XML into the named file before invoking the XML browser. The command named as the argument of ‘xml_browser_cmd’ will usually refer to this file.

xml_tmp_filename

Prints the temporary filename used for XML browsing, if this has been set.

format [-APB] format

Sets the default format of the browser to format, which should be one of ‘flat’, ‘pretty’ and ‘verbose’.

The browser maintains separate configuration parameters for the three commands ‘print *’, ‘print var’, and ‘browse var’. A ‘format’ command applies to all three, unless it specifies one or more of the options ‘-A’ or ‘--print-all’, ‘-P’ or ‘--print’, and ‘-B’ or ‘--browse’, in which case it will set only the selected command's default format.

format_param [-APBfpv] param value

Sets one of the parameters of the browser to the given value. The parameter param must be one of ‘depth’, ‘size’, ‘width’ and ‘lines’.

• ‘depth’ is the maximum depth to which subterms will be displayed. Subterms at the depth limit may be abbreviated as functor/arity, or (in lists) may be replaced by an ellipsis (‘...’). The principal functor of any term has depth zero. For subterms which are not lists, the depth of any argument of the functor is one greater than the depth of the functor. For subterms which are lists, the depth of each element of the list is one greater than the depth of the list.

• ‘size’ is the suggested maximum number of functors to display. Beyond this limit, subterms may be abbreviated as functor/arity, or (in lists) may be replaced by an ellipsis (‘...’). For the purposes of this parameter, the size of a list is one greater than the sum of the sizes of the elements in the list.

• ‘width’ is the width of the screen in characters.

• ‘lines’ is the preferred maximum number of lines of one term to display.

The browser maintains separate configuration parameters for the three commands ‘print *’, ‘print var’, and ‘browse var’. A ‘format_param’ command applies to all three, unless it specifies one or more of the options ‘-A’ or ‘--print-all’, ‘-P’ or ‘--print’, and ‘-B’ or ‘--browse’, in which case it will set only the selected command's parameters.

The browser also maintains separate configuration parameters for the different output formats: flat, pretty and verbose. A ‘format_param’ command applies to all of these, unless it specifies one or more of the options ‘-f’ or ‘--flat’, ‘-p’ or ‘--pretty’, and ‘-v’ or ‘--verbose’, in which case it will set only the selected format's parameter.

alias name command [command-parameter ...]

Introduces name as an alias for the given command with the given parameters. Whenever a command line has name as its first word, the debugger will substitute the given command and parameters for this word before executing the command line.

If name is the upper-case word ‘EMPTY’, the debugger will substitute the given command and parameters whenever the user types in an empty command line.

If name is the upper-case word ‘NUMBER’, the debugger will insert the given command and parameters before the command line whenever the user types in a command line that consists of a single number.

unalias name

Removes any existing alias for name.