Skip to content

Utilities for reporting overall result/status/exit code [depends: 3583, blocks: 3585] #3584

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

Jump to bottom
Merged
merged 7 commits into from
Jan 14, 2019
Merged

Utilities for reporting overall result/status/exit code [depends: 3583, blocks: 3585] #3584

merged 7 commits into from
Jan 14, 2019

Conversation

peterschrammel
Copy link
Member

@peterschrammel peterschrammel commented Dec 16, 2018 •
edited by tautschnig
Loading

Based on #3583, only review last 4 commits.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • [n/a] My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@peterschrammel peterschrammel changed the title Overall reporting utils [depends: 3584] Utilities for reporting overall result/status/exit code [depends: 3584] Dec 16, 2018
@peterschrammel peterschrammel mentioned this pull request Dec 16, 2018
Merged
6 tasks
@peterschrammel peterschrammel changed the title Utilities for reporting overall result/status/exit code [depends: 3584] Utilities for reporting overall result/status/exit code [depends: 3583, blocks: 3585] Dec 16, 2018
@peterschrammel peterschrammel force-pushed the overall-reporting-utils branch from 89c7580 to 2c92ab1 Compare December 17, 2018 10:39
tautschnig
tautschnig reviewed Dec 17, 2018
View reviewed changes
src/goto-checker/report_util.cpp Outdated
report_error(ui_message_handler);
break;
}
}
Copy link
Collaborator

Choose a reason for hiding this comment

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

Missing newline

src/goto-checker/report_util.cpp
@@ -71,6 +71,62 @@ void report_failure(ui_message_handlert &ui_message_handler)
}
}

void report_inconclusive(ui_message_handlert &ui_message_handler)
Copy link
Collaborator

Choose a reason for hiding this comment

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

The commit message talks about the wrong file.

src/goto-checker/report_util.cpp Outdated
void report_inconclusive(ui_message_handlert &ui_message_handler)
{
messaget msg(ui_message_handler);
msg.result() << "INCONCLUSIVE" << messaget::eom;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Don't we already use "UNKNOWN" in places (goto-analyzer, for example)?

Copy link
Member Author

Choose a reason for hiding this comment

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

I don't mind. Any preferences?

src/goto-checker/report_util.cpp
void report_error(ui_message_handlert &ui_message_handler)
{
messaget msg(ui_message_handler);
msg.result() << "VERIFICATION ERROR" << messaget::eom;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Applies to all the report* functions: do we print both formatted and unformatted output in case of both XML and JSON?!

Copy link
Member Author

Choose a reason for hiding this comment

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

That's the current behaviour. 387834c#diff-6b42a28511965b646db79583668c5e6eL161

@peterschrammel peterschrammel force-pushed the overall-reporting-utils branch from 2c92ab1 to 6516d1f Compare January 13, 2019 15:03
@peterschrammel
Add count_properties with given result
cc1a90e 
To count how many properties have a certain status.
This will be used in property reporting.
@peterschrammel
Add property output functions
4da669d 
Plain text, XML and JSON output for property results.
@peterschrammel
Add report_util for outputting verification results
519fb98 
Prints the property report in plain text, JSON or XML.
@peterschrammel
Move reporting functions to report_util
0ba2e84
@peterschrammel peterschrammel force-pushed the overall-reporting-utils branch from 6516d1f to 323f131 Compare January 13, 2019 16:50
allredj
allredj reviewed Jan 13, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: 323f131).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97168736

@peterschrammel
Add report_error and report_inconclusive to report_util
0ba0833
@peterschrammel
Add result_to_exit_code
02bc690 
Enable consistent result-dependent exit codes across all
driver programs.
@peterschrammel
Utility for printing overall result
b1587fa 
Enable consistent overall status reporting
across all driver programs.
@peterschrammel peterschrammel force-pushed the overall-reporting-utils branch from 323f131 to b1587fa Compare January 14, 2019 00:43
allredj
allredj reviewed Jan 14, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: b1587fa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97183590

@tautschnig tautschnig merged commit ce577d8 into diffblue:develop Jan 14, 2019
@peterschrammel peterschrammel deleted the overall-reporting-utils branch January 14, 2019 09:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@tautschnig tautschnig tautschnig approved these changes

@cesaro cesaro Awaiting requested review from cesaro

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@cristina-david cristina-david Awaiting requested review from cristina-david

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

@smowton smowton Awaiting requested review from smowton

Assignees

@peterschrammel peterschrammel

Labels
blocker dependent - do not merge Goto-checker
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@peterschrammel @tautschnig @allredj