{"action":"created","issue":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/197","repository_url":"https://api.github.com/repos/diffblue/cbmc","labels_url":"https://api.github.com/repos/diffblue/cbmc/issues/197/labels{/name}","comments_url":"https://api.github.com/repos/diffblue/cbmc/issues/197/comments","events_url":"https://api.github.com/repos/diffblue/cbmc/issues/197/events","html_url":"https://github.com/diffblue/cbmc/issues/197","id":170486183,"number":197,"title":"identifier __CPROVER_memory not found","user":{"login":"peterschrammel","id":4222448,"avatar_url":"https://avatars.githubusercontent.com/u/4222448?v=3","gravatar_id":"","url":"https://api.github.com/users/peterschrammel","html_url":"https://github.com/peterschrammel","followers_url":"https://api.github.com/users/peterschrammel/followers","following_url":"https://api.github.com/users/peterschrammel/following{/other_user}","gists_url":"https://api.github.com/users/peterschrammel/gists{/gist_id}","starred_url":"https://api.github.com/users/peterschrammel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/peterschrammel/subscriptions","organizations_url":"https://api.github.com/users/peterschrammel/orgs","repos_url":"https://api.github.com/users/peterschrammel/repos","events_url":"https://api.github.com/users/peterschrammel/events{/privacy}","received_events_url":"https://api.github.com/users/peterschrammel/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/diffblue/cbmc/labels/bug","name":"bug","color":"fc2929"}],"state":"open","locked":false,"assignee":{"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},"assignees":[{"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}],"milestone":null,"comments":5,"created_at":"2016-08-10T18:30:12Z","updated_at":"2016-08-20T16:54:31Z","closed_at":null,"body":"Hello,\r\n\r\ncurrent CBMC master crashes on the attached Java program (distilled\r\nfrom production code).\r\n\r\nThanks,\r\n\r\nVladimir Klebanov\r\n\r\n-----\r\n\r\nCBMC version 5.4 64-bit x86_64 linux\r\nParsing Driver.class\r\nJava main class: Driver\r\nfailed to load class `java.lang.String'\r\nfailed to load class `java.lang.Object'\r\nfailed to load class `java.lang.Class'\r\nfailed to load class `java.lang.AssertionError'\r\nConverting\r\nGenerating GOTO Program\r\nAdding CPROVER library (x86_64)\r\nRemoval of function pointers and virtual functions\r\nPartial Inlining\r\nGeneric Property Instrumentation\r\nStarting Bounded Model Checking\r\n**** WARNING: no body for function\r\njava::java.lang.Class.desiredAssertionStatus:()Z\r\n**** WARNING: no body for function java::java.lang.Object.<init>:()V\r\n**** WARNING: no body for function java::java.lang.AssertionError.<init>:()V\r\nfile Driver.java line 50: identifier __CPROVER_memory not found\r\n\r\n\r\n```\r\npublic class Driver {\r\n\r\n    static byte[] out,in;\r\n\r\n    public static void main(String[] argv) {\r\n\r\n        X x = new X();\r\n        x.y(out);\r\n\r\n    }\r\n\r\n}\r\n\r\nfinal class X {\r\n\r\n    private static final int DIGEST_SIZE = 20;\r\n    private transient MyMessageDigest digest;\r\n    private byte[] state;\r\n\r\n    public X() {\r\n        init(null);\r\n    }\r\n\r\n    private void init(byte[] seed) {\r\n        digest = new MyMessageDigest();\r\n\r\n        if (seed != null) {\r\n            state = digest.digest(seed);\r\n        }\r\n    }\r\n\r\n    public synchronized void y(byte[] result) {\r\n        byte[] output = digest.digest();\r\n    }\r\n}\r\n\r\n\r\nclass MyMessageDigest {\r\n\r\n    private byte[] state = null;\r\n\r\n\r\n    public void update(byte[] input) {\r\n        assert(input.length == 20);\r\n        state = input;\r\n    }\r\n\r\n\r\n    public byte[] digest() {\r\n        byte[] tmp = state;\r\n        state = null;\r\n        return tmp;\r\n    }\r\n\r\n    public byte[] digest(byte[] input) {\r\n        update(input);\r\n        return digest();\r\n    }\r\n\r\n\r\n}\r\n```\r\n"},"comment":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/comments/241210842","html_url":"https://github.com/diffblue/cbmc/issues/197#issuecomment-241210842","issue_url":"https://api.github.com/repos/diffblue/cbmc/issues/197","id":241210842,"user":{"login":"vladrich","id":2369345,"avatar_url":"https://avatars.githubusercontent.com/u/2369345?v=3","gravatar_id":"","url":"https://api.github.com/users/vladrich","html_url":"https://github.com/vladrich","followers_url":"https://api.github.com/users/vladrich/followers","following_url":"https://api.github.com/users/vladrich/following{/other_user}","gists_url":"https://api.github.com/users/vladrich/gists{/gist_id}","starred_url":"https://api.github.com/users/vladrich/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vladrich/subscriptions","organizations_url":"https://api.github.com/users/vladrich/orgs","repos_url":"https://api.github.com/users/vladrich/repos","events_url":"https://api.github.com/users/vladrich/events{/privacy}","received_events_url":"https://api.github.com/users/vladrich/received_events","type":"User","site_admin":false},"created_at":"2016-08-20T16:54:30Z","updated_at":"2016-08-20T16:54:30Z","body":"Thanks for looking at this, Chris. I grafted your patch onto current master and it does prevent the crash. Verification of the particular benchmark now completes, but the results are surprising to me. At the moment, I cannot say if this is a genuine finding or some misunderstanding of mine. I will investigate the issue."}}
{"actor":{"display_login":"vladrich"}}