Skip to content

Trace output configuration options #1565

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 13 commits into from
Closed

Trace output configuration options #1565

Show file tree
Hide file tree
Changes from 12 commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
18a45e3
Output lines of code in trace and values in hex format
polgreen Oct 17, 2017
686fedd
Start of HTML goto trace output
polgreen Oct 4, 2017
6725c8c
Output function calls in trace
polgreen Oct 18, 2017
24a4875
Change "violated assumption" to "assumption" in trace
polgreen Oct 20, 2017
7a1dca7
Add trace_configuration struct to global config
polgreen Oct 20, 2017
cb560d3
Tidy up CBMC parse_options trace configuration
polgreen Oct 24, 2017
d88d5d6
switch show_goto_trace to use trace_configurationt
polgreen Oct 20, 2017
c05ab18
Update html_goto_trace to use trace_configurationt
polgreen Oct 20, 2017
671db6b
rename "html-trace" to "trace-html"
polgreen Oct 24, 2017
51bfbd7
Fix html trace colour alternation for function calls
polgreen Oct 23, 2017
5129907
replace assert with invariant
polgreen Nov 7, 2017
94391c1
doxygen changes
polgreen Nov 7, 2017
9b8cbfb
configure trace otuput for graphml witness
polgreen Nov 7, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 42 additions & 0 deletions src/cbmc/cbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,6 +102,36 @@ void cbmc_parse_optionst::eval_verbosity()
ui_message_handler.set_verbosity(v);
}

void cbmc_parse_optionst::configure_trace_output()
{
if(cmdline.isset("trace-hex"))
config.trace_config.numeric_representation =
configt::numeric_representationt::HEX;
else
config.trace_config.numeric_representation =
configt::numeric_representationt::BINARY;

config.trace_config.show_source_code =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Using config for this kind of settings is uncommon. Use options.

cmdline.isset("trace-show-source-code");

config.trace_config.show_value_assignments =
!cmdline.isset("trace-hide-assignments");

config.trace_config.show_inputs =
!cmdline.isset("trace-hide-inputs");

config.trace_config.show_outputs =
!cmdline.isset("trace-hide-ouputs");

config.trace_config.show_function_calls =
cmdline.isset("trace-show-function-calls");

if(cmdline.isset("trace-html"))
config.trace_config.trace_format = configt::trace_formatt::HTML;
else
config.trace_config.trace_format = configt::trace_formatt::STANDARD;
}

void cbmc_parse_optionst::get_command_line_options(optionst &options)
{
if(config.set(cmdline))
Expand Down Expand Up @@ -154,7 +184,10 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)

if(cmdline.isset("trace") ||
cmdline.isset("stop-on-fail"))
{
options.set_option("trace", true);
configure_trace_output();
}

if(cmdline.isset("localize-faults"))
options.set_option("localize-faults", true);
Expand Down Expand Up @@ -1024,5 +1057,14 @@ void cbmc_parse_optionst::help()
" --xml-interface bi-directional XML interface\n"
" --json-ui use JSON-formatted output\n"
" --verbosity # verbosity level\n"
"\n"
"Trace formatting options\n"
"--trace-show-function-calls show functions calls and returns in trace (default is to hide)\n" // NOLINT(*)
"--trace-hide-assignments hide all assignments in trace (default is to show)\n" // NOLINT(*)
"--trace-hide-inputs hide all inputs in trace (default is to show)\n" // NOLINT(*)
"--trace-hide-outputs hide all outputs in trace (default is to show)\n" // NOLINT(*)
"--trace-show-source-code show lines of source code (default is to hide)\n" // NOLINT(*)
"--trace-hex outputs assignments to variables in hex (default is binary)\n" // NOLINT(*)
"--trace-html outputs trace in html format\n"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is the result of using --trace-htmltogether with --json-ui?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

json overrides. I don't know what the expected result should be, but the json trace doesn't use any of my new configuration options

"\n";
}
4 changes: 4 additions & 0 deletions src/cbmc/cbmc_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,9 @@ class optionst;
"(show-claims)(claim):(show-properties)" \
"(drop-unused-functions)" \
"(property):(stop-on-fail)(trace)" \
"(trace-hex)(trace-show-source-code)(trace-hide-assignments)"\
"(trace-show-function-calls)(trace-html)(trace-hide-inputs)" \
"(trace-hide-outputs)" \
"(error-label):(verbosity):(no-library)" \
"(nondet-static)" \
"(version)" \
Expand Down Expand Up @@ -89,6 +92,7 @@ class cbmc_parse_optionst:
void eval_verbosity();
void register_languages();
void get_command_line_options(optionst &);
void configure_trace_output();
void preprocessing();
int get_goto_program(const optionst &);
bool process_goto_program(const optionst &);
Expand Down
1 change: 1 addition & 0 deletions src/goto-programs/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ SRC = basic_blocks.cpp \
goto_program_template.cpp \
goto_trace.cpp \
graphml_witness.cpp \
html_goto_trace.cpp \
instrument_preconditions.cpp \
interpreter.cpp \
interpreter_evaluate.cpp \
Expand Down
Loading