Skip to content

Multi-path symex checker [blocks: 3796] #3795

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 25 commits into from
Jan 31, 2019
Merged

Multi-path symex checker [blocks: 3796] #3795

merged 25 commits into from
Jan 31, 2019

Conversation

peterschrammel
Copy link
Member

@peterschrammel peterschrammel commented Jan 13, 2019 •
edited
Loading

Based on #3794, only review after the first 7 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).
  • 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 Multi path symex checker [depends: 3794] Multi-path symex checker [depends: 3794] Jan 13, 2019
@peterschrammel peterschrammel force-pushed the multi-path-symex-checker branch 2 times, most recently from 6ec0f1d to 457ebc5 Compare January 13, 2019 20:39
@peterschrammel peterschrammel mentioned this pull request Jan 13, 2019
Merged
7 tasks
@peterschrammel peterschrammel changed the title Multi-path symex checker [depends: 3794] Multi-path symex checker [depends: 3794, blocks: 3795] Jan 13, 2019
@peterschrammel peterschrammel force-pushed the multi-path-symex-checker branch from 457ebc5 to 29cdfd7 Compare January 14, 2019 00:52
@peterschrammel peterschrammel self-assigned this Jan 14, 2019
@peterschrammel peterschrammel force-pushed the multi-path-symex-checker branch 3 times, most recently from 4aeca61 to 492866a Compare January 20, 2019 15:23
@peterschrammel peterschrammel force-pushed the multi-path-symex-checker branch 5 times, most recently from 0104344 to 17ebf64 Compare January 20, 2019 23:14
@peterschrammel peterschrammel force-pushed the multi-path-symex-checker branch from 17ebf64 to eb01fae Compare January 21, 2019 00:00
@peterschrammel
Clarify comment on updated properties
baf79ff
@peterschrammel
Split updating properties from equation
c7966c8 
This previously performed two actions that should be done separately:
- updating properties whose status has been explicitly determined
  in the equation
- setting a status for properties that do not occur in the equation
@peterschrammel
Fix wrong include
90625eb
@peterschrammel
Fix documentation
d51437f
@peterschrammel
Move counterexample beautification to goto_checker
2fcc886 
This is language-independent and can be used by
incremental goto checkers that provide traces.
@peterschrammel
Fix whitespace
0ab57df
@peterschrammel
Clang-format
dd49711
@peterschrammel
Output SUCCESS and FAILURE for property status
8fcb968 
This is currently used in all the regression tests.
@peterschrammel
Support outputting properties into JSON streams
adbb483
@peterschrammel
Factor out output_properties_plain text
6adaffe 
To allow reuse for output with/without traces
@peterschrammel
Add goto trace storage
e2f2c31 
In all properties mode, traces are currently output
at the very end. Hence, we have to store them.
@peterschrammel
Output property results with traces
7574896
@peterschrammel
Output number of incremental goto checker iterations
3573395 
in message "x out of y failed (z iterations)".
@peterschrammel
Do not output results if there are no properties
201ad4d
@peterschrammel
Missing line number for unwinding assertion
d7cde75
@peterschrammel
Add all properties verifier with trace storage
eb39229 
All-properties currently doesn't output the traces continuously,
but waits until the end. Hence, we have to store the traces.
@peterschrammel
Add multi path symex checker
f2fb9ab 
multi_path_symex_only_checkert is a
bounded model checking algorithm that determines the
status of properties through symbolic execution,
constant propagation and SAT solving.
@peterschrammel
Use goto verifier for all-properties in CBMC
c84f516
@peterschrammel
Fix test matching missing property description
7663837 
All properties have a description now.
@peterschrammel
Multi-path checker for Java requires preprocessing
3414d55
@peterschrammel
Use goto verifier for all-properties in JBMC
093718a
@peterschrammel
Add goto-checker documentation
37ae8b1
@peterschrammel peterschrammel force-pushed the multi-path-symex-checker branch from 72b4ab1 to 37ae8b1 Compare January 31, 2019 15:29
allredj
allredj reviewed Jan 31, 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: 37ae8b1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99316896

@tautschnig tautschnig assigned peterschrammel and unassigned smowton and thk123 Jan 31, 2019
@peterschrammel peterschrammel merged commit b0806f2 into diffblue:develop Jan 31, 2019
@peterschrammel peterschrammel deleted the multi-path-symex-checker branch January 31, 2019 21:03
@peterschrammel peterschrammel mentioned this pull request Feb 12, 2019
Merged
7 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@forejtv forejtv forejtv left review comments

@allredj allredj allredj approved these changes

@smowton smowton smowton approved these changes

@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

@NathanJPhillips NathanJPhillips Awaiting requested review from NathanJPhillips

@thk123 thk123 Awaiting requested review from thk123

Assignees

@peterschrammel peterschrammel

Labels
blocker Goto-checker
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@peterschrammel @smowton @tautschnig @forejtv @allredj @thk123