Skip to content

All-properties verifier [depends: 3584, blocks: 3794] #3585

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 10 commits into from
Jan 14, 2019
Merged

All-properties verifier [depends: 3584, blocks: 3794] #3585

merged 10 commits into from
Jan 14, 2019

Conversation

peterschrammel
Copy link
Member

@peterschrammel peterschrammel commented Dec 16, 2018 •
edited
Loading

This is going to replace all_properties (can be instantiated with any incremental_goto_checkert: multi-path and single-path will come next).

Based on #3584, only review last 3 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/1] 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 All-properties verifier [depends: 3585] All-properties verifier [depends: 3584] Dec 16, 2018
@peterschrammel peterschrammel force-pushed the all-properties-verifier branch from 2c3ed7f to 3d5e246 Compare December 17, 2018 10:40
tautschnig
tautschnig reviewed Dec 17, 2018
View reviewed changes
src/goto-checker/properties.cpp Outdated
// then overall it's still a PASS.
if(
result == property_resultt::NOT_REACHED ||
result == property_resultt::NOT_REACHABLE)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Since we do distinguish NOT_REACHED from NOT_REACHABLE, shouldn't the former yield UNKNOWN?

src/goto-checker/all_properties_verifier.h Outdated
const optionst &options,
ui_message_handlert &ui_message_handler,
abstract_goto_modelt &goto_model)
: goto_verifiert(options, 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.

Is this actually used in any way?

@peterschrammel peterschrammel force-pushed the all-properties-verifier branch from 3d5e246 to b0a05a8 Compare January 13, 2019 15:04
@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 all-properties-verifier branch 2 times, most recently from 615786a to 1f2b8c5 Compare January 13, 2019 17:11
@peterschrammel peterschrammel mentioned this pull request Jan 13, 2019
Merged
7 tasks
@peterschrammel peterschrammel changed the title All-properties verifier [depends: 3584] All-properties verifier [depends: 3584, blocks: 3794] Jan 13, 2019
@peterschrammel peterschrammel force-pushed the all-properties-verifier branch from 1f2b8c5 to 407b527 Compare January 13, 2019 20:26
tautschnig
tautschnig approved these changes Jan 13, 2019
View reviewed changes
src/goto-checker/all_properties_verifier.h Outdated
goto_model(goto_model),
incremental_goto_checker(options, ui_message_handler, goto_model)
{
properties = std::move(initialize_properties(goto_model));
Copy link
Collaborator

Choose a reason for hiding this comment

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

I think you don't need std::move with an unnamed temporary, but I could be wrong.

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes, this should work without move; there is only a single allocation site in the callee.

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: 407b527).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97175651

@peterschrammel peterschrammel force-pushed the all-properties-verifier branch from 407b527 to 7ea25b5 Compare January 13, 2019 22:35
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: 7ea25b5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97180336

@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
Add functions to combine property results
3c2778e 
Used to update the properties map and
to compute the overall result.
@peterschrammel
Add has_properties_to_check
4b55962
@peterschrammel
Add all_properties_verifier
c61ca64 
This will replace bmc_all_propertiest.
@peterschrammel peterschrammel force-pushed the all-properties-verifier branch from 7ea25b5 to c61ca64 Compare January 14, 2019 00:44
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: c61ca64).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97183649

@tautschnig tautschnig merged commit 73ebbb4 into diffblue:develop Jan 14, 2019
@peterschrammel peterschrammel deleted the all-properties-verifier 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