{"action":"created","issue":{"url":"https://api.github.com/repos/cristina-david/cbmc/issues/15","repository_url":"https://api.github.com/repos/cristina-david/cbmc","labels_url":"https://api.github.com/repos/cristina-david/cbmc/issues/15/labels{/name}","comments_url":"https://api.github.com/repos/cristina-david/cbmc/issues/15/comments","events_url":"https://api.github.com/repos/cristina-david/cbmc/issues/15/events","html_url":"https://github.com/cristina-david/cbmc/pull/15","id":176057733,"number":15,"title":"Infer Java block structure, plus many misc fixes","user":{"login":"smowton","id":283483,"avatar_url":"https://avatars.githubusercontent.com/u/283483?v=3","gravatar_id":"","url":"https://api.github.com/users/smowton","html_url":"https://github.com/smowton","followers_url":"https://api.github.com/users/smowton/followers","following_url":"https://api.github.com/users/smowton/following{/other_user}","gists_url":"https://api.github.com/users/smowton/gists{/gist_id}","starred_url":"https://api.github.com/users/smowton/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/smowton/subscriptions","organizations_url":"https://api.github.com/users/smowton/orgs","repos_url":"https://api.github.com/users/smowton/repos","events_url":"https://api.github.com/users/smowton/events{/privacy}","received_events_url":"https://api.github.com/users/smowton/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-09-09T16:58:18Z","updated_at":"2016-09-14T12:21:36Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/cristina-david/cbmc/pulls/15","html_url":"https://github.com/cristina-david/cbmc/pull/15","diff_url":"https://github.com/cristina-david/cbmc/pull/15.diff","patch_url":"https://github.com/cristina-david/cbmc/pull/15.patch"},"body":"Changes:\r\n\r\n* When Java is compiled with debug information (yielding a local variable table), we now introduce block structure into the intermediate representation according to the variable live ranges given. This results in appropriate `dead` opcodes in the final program.\r\n  * Also introduced support for `dead` destructor generation on `goto` out of scope, which should be present for C/C++ in any case, and is ubiquitous in Java since all branches are compiled to `goto`.\r\n  * This can deal with simple linear live ranges, and with live ranges that include simple splits, as typically seen in `try/catch` blocks. More complex cases yet to be seen in the wild, but theoretically possible.\r\n* Java array accesses and creation both validate their index arguments, for now with an `assert` rather than a `throw`.\r\n* Java `checkcast` opcodes now actually do check, again with an `assert`. This implements `instanceof`.\r\n* Various static objects (e.g. `.class` objects, string literals) are nondet-initialised, rather than being left for cbmc to pick arbitrary pointer values.\r\n* Improved virtual function dispatch, so we should no longer see inappropriate downcasts.\r\n* Improved symex of variable-length arrays, removing `derference` opcodes in array-size arguments so that they appear in the trace with their actual runtime type.\r\n* Support array size limitation when compiling Java, (`--java-max-vla-length`), intended to prevent generated testcases from consuming an unreasonable amount of memory during interpretation / execution.\r\n* Various trivial fixes"},"comment":{"url":"https://api.github.com/repos/cristina-david/cbmc/issues/comments/246995558","html_url":"https://github.com/cristina-david/cbmc/pull/15#issuecomment-246995558","issue_url":"https://api.github.com/repos/cristina-david/cbmc/issues/15","id":246995558,"user":{"login":"smowton","id":283483,"avatar_url":"https://avatars.githubusercontent.com/u/283483?v=3","gravatar_id":"","url":"https://api.github.com/users/smowton","html_url":"https://github.com/smowton","followers_url":"https://api.github.com/users/smowton/followers","following_url":"https://api.github.com/users/smowton/following{/other_user}","gists_url":"https://api.github.com/users/smowton/gists{/gist_id}","starred_url":"https://api.github.com/users/smowton/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/smowton/subscriptions","organizations_url":"https://api.github.com/users/smowton/orgs","repos_url":"https://api.github.com/users/smowton/repos","events_url":"https://api.github.com/users/smowton/events{/privacy}","received_events_url":"https://api.github.com/users/smowton/received_events","type":"User","site_admin":false},"created_at":"2016-09-14T12:21:36Z","updated_at":"2016-09-14T12:21:36Z","body":"Updated this just now to be mergeable"}}
{"actor":{"display_login":"smowton"}}