{"action":"created","issue":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/1641","repository_url":"https://api.github.com/repos/diffblue/cbmc","labels_url":"https://api.github.com/repos/diffblue/cbmc/issues/1641/labels{/name}","comments_url":"https://api.github.com/repos/diffblue/cbmc/issues/1641/comments","events_url":"https://api.github.com/repos/diffblue/cbmc/issues/1641/events","html_url":"https://github.com/diffblue/cbmc/pull/1641","id":277858583,"number":1641,"title":"Add support for path exploration to CBMC/JBMC, in addition to full bounded model checking","user":{"login":"karkhaz","id":2887605,"avatar_url":"https://avatars1.githubusercontent.com/u/2887605?v=4","gravatar_id":"","url":"https://api.github.com/users/karkhaz","html_url":"https://github.com/karkhaz","followers_url":"https://api.github.com/users/karkhaz/followers","following_url":"https://api.github.com/users/karkhaz/following{/other_user}","gists_url":"https://api.github.com/users/karkhaz/gists{/gist_id}","starred_url":"https://api.github.com/users/karkhaz/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/karkhaz/subscriptions","organizations_url":"https://api.github.com/users/karkhaz/orgs","repos_url":"https://api.github.com/users/karkhaz/repos","events_url":"https://api.github.com/users/karkhaz/events{/privacy}","received_events_url":"https://api.github.com/users/karkhaz/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"karkhaz","id":2887605,"avatar_url":"https://avatars1.githubusercontent.com/u/2887605?v=4","gravatar_id":"","url":"https://api.github.com/users/karkhaz","html_url":"https://github.com/karkhaz","followers_url":"https://api.github.com/users/karkhaz/followers","following_url":"https://api.github.com/users/karkhaz/following{/other_user}","gists_url":"https://api.github.com/users/karkhaz/gists{/gist_id}","starred_url":"https://api.github.com/users/karkhaz/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/karkhaz/subscriptions","organizations_url":"https://api.github.com/users/karkhaz/orgs","repos_url":"https://api.github.com/users/karkhaz/repos","events_url":"https://api.github.com/users/karkhaz/events{/privacy}","received_events_url":"https://api.github.com/users/karkhaz/received_events","type":"User","site_admin":false},"assignees":[{"login":"karkhaz","id":2887605,"avatar_url":"https://avatars1.githubusercontent.com/u/2887605?v=4","gravatar_id":"","url":"https://api.github.com/users/karkhaz","html_url":"https://github.com/karkhaz","followers_url":"https://api.github.com/users/karkhaz/followers","following_url":"https://api.github.com/users/karkhaz/following{/other_user}","gists_url":"https://api.github.com/users/karkhaz/gists{/gist_id}","starred_url":"https://api.github.com/users/karkhaz/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/karkhaz/subscriptions","organizations_url":"https://api.github.com/users/karkhaz/orgs","repos_url":"https://api.github.com/users/karkhaz/repos","events_url":"https://api.github.com/users/karkhaz/events{/privacy}","received_events_url":"https://api.github.com/users/karkhaz/received_events","type":"User","site_admin":false}],"milestone":null,"comments":37,"created_at":"2017-11-29T18:25:13Z","updated_at":"2018-02-18T09:37:37Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/diffblue/cbmc/pulls/1641","html_url":"https://github.com/diffblue/cbmc/pull/1641","diff_url":"https://github.com/diffblue/cbmc/pull/1641.diff","patch_url":"https://github.com/diffblue/cbmc/pull/1641.patch"},"body":"CBMC can now model-check each path of a program one at a time, displaying the verification result for that path before continuing to symbolically execute other paths. This functionality is similar to what the `symex` tool provides, but uses the `goto-symex` core that is already used by CBMC rather than having a disjoint symbolic execution codebase. This functionality is enabled by passing the `--paths` flag to CBMC or JBMC.\r\n\r\nWhen `--paths` is passed, CBMC does not perform path merging when it encounters a program join point. Instead, whenever it encounters a conditional `goto` instruction, it saves the state of the symbolic executor onto a workqueue and executes one of the branches. Once symbolic execution has finished and the verification result printed out, CBMC pops the workqueue and resumes executing the untaken branch.\r\n\r\nThis is all integrated with the existing `bmc` and `goto_symext` classes, with no change in CBMC's original model-checking functionality. Without the `--paths` flag, CBMC's full-program model-checking behaviour is an edge-case of path exploration, whereby no goto branch-points are saved and so the entire program is only symbolically executed once.\r\n\r\nThe main patch in this patchset is `[path explore 5/6] Support path-based exploration`. Other commits are fairly small and introduce features that are necessary for path exploration, but which are also desirable changes by themselves."},"comment":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/comments/366503580","html_url":"https://github.com/diffblue/cbmc/pull/1641#issuecomment-366503580","issue_url":"https://api.github.com/repos/diffblue/cbmc/issues/1641","id":366503580,"user":{"login":"karkhaz","id":2887605,"avatar_url":"https://avatars1.githubusercontent.com/u/2887605?v=4","gravatar_id":"","url":"https://api.github.com/users/karkhaz","html_url":"https://github.com/karkhaz","followers_url":"https://api.github.com/users/karkhaz/followers","following_url":"https://api.github.com/users/karkhaz/following{/other_user}","gists_url":"https://api.github.com/users/karkhaz/gists{/gist_id}","starred_url":"https://api.github.com/users/karkhaz/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/karkhaz/subscriptions","organizations_url":"https://api.github.com/users/karkhaz/orgs","repos_url":"https://api.github.com/users/karkhaz/repos","events_url":"https://api.github.com/users/karkhaz/events{/privacy}","received_events_url":"https://api.github.com/users/karkhaz/received_events","type":"User","site_admin":false},"created_at":"2018-02-18T09:37:36Z","updated_at":"2018-02-18T09:37:36Z","author_association":"CONTRIBUTOR","body":"Thanks @tautschnig, that worked! FWIW I tried to \"restart\" the job by `git commit --amend`ing and re-pushing, but it timed out again. Anyway, ready for review. Cheers!"}}
{"actor":{"display_login":"karkhaz"}}