{"action":"created","issue":{"url":"https://api.github.com/repos/OrenGitHub/klee/issues/26","repository_url":"https://api.github.com/repos/OrenGitHub/klee","labels_url":"https://api.github.com/repos/OrenGitHub/klee/issues/26/labels{/name}","comments_url":"https://api.github.com/repos/OrenGitHub/klee/issues/26/comments","events_url":"https://api.github.com/repos/OrenGitHub/klee/issues/26/events","html_url":"https://github.com/OrenGitHub/klee/issues/26","id":307933068,"number":26,"title":"Context driven / aware semantics for strchr","user":{"login":"OrenGitHub","id":6602314,"avatar_url":"https://avatars2.githubusercontent.com/u/6602314?v=4","gravatar_id":"","url":"https://api.github.com/users/OrenGitHub","html_url":"https://github.com/OrenGitHub","followers_url":"https://api.github.com/users/OrenGitHub/followers","following_url":"https://api.github.com/users/OrenGitHub/following{/other_user}","gists_url":"https://api.github.com/users/OrenGitHub/gists{/gist_id}","starred_url":"https://api.github.com/users/OrenGitHub/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/OrenGitHub/subscriptions","organizations_url":"https://api.github.com/users/OrenGitHub/orgs","repos_url":"https://api.github.com/users/OrenGitHub/repos","events_url":"https://api.github.com/users/OrenGitHub/events{/privacy}","received_events_url":"https://api.github.com/users/OrenGitHub/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2018-03-23T07:57:58Z","updated_at":"2018-03-23T17:12:24Z","closed_at":null,"author_association":"OWNER","body":"Hi all,\r\nI have revisited the Z3 string API, to make sure we're not missing\r\nout on any opportunities, and when I reached **str.contains**, I have decided\r\nto profile it and see if it is merely syntactic sugar for (str.indexof == -1).\r\nI was somewhat surprised to see it's not, and in fact **str.indexof** uses\r\n**str.contains** and not the other way around (!)\r\n\r\n[see this response](https://github.com/Z3Prover/z3/issues/1548)\r\n\r\nso this really gives an incentive to define a **context driven semantics** to strchr (!)\r\nEither as having a Boolean returned value like here:\r\n\r\n    p1 = strchr (p2 + 2, ' ');    /* no space allowed inside sip-url */\r\n    if (p1 == NULL) { // ... }\r\n\r\nOr as having it follow the usual semantics like here\r\n\r\n    tmp_comma = strchr (comma + 1, ',');\r\n    while (1)\r\n    {\r\n        if (tmp_comma < tmp_quote1)\r\n        {\r\n            break;              /* ok (before to quotes) */\r\n        }\r\n        // ...\r\n    }\r\n\r\nBecause **now there will be** a different z3 solving time (!)\r\n\r\nCC: @kren1 @ccadar @rinetzky \r\n"},"comment":{"url":"https://api.github.com/repos/OrenGitHub/klee/issues/comments/375736968","html_url":"https://github.com/OrenGitHub/klee/issues/26#issuecomment-375736968","issue_url":"https://api.github.com/repos/OrenGitHub/klee/issues/26","id":375736968,"user":{"login":"OrenGitHub","id":6602314,"avatar_url":"https://avatars2.githubusercontent.com/u/6602314?v=4","gravatar_id":"","url":"https://api.github.com/users/OrenGitHub","html_url":"https://github.com/OrenGitHub","followers_url":"https://api.github.com/users/OrenGitHub/followers","following_url":"https://api.github.com/users/OrenGitHub/following{/other_user}","gists_url":"https://api.github.com/users/OrenGitHub/gists{/gist_id}","starred_url":"https://api.github.com/users/OrenGitHub/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/OrenGitHub/subscriptions","organizations_url":"https://api.github.com/users/OrenGitHub/orgs","repos_url":"https://api.github.com/users/OrenGitHub/repos","events_url":"https://api.github.com/users/OrenGitHub/events{/privacy}","received_events_url":"https://api.github.com/users/OrenGitHub/received_events","type":"User","site_admin":false},"created_at":"2018-03-23T17:12:24Z","updated_at":"2018-03-23T17:12:24Z","author_association":"OWNER","body":"Clearly, an arbitrary C code is allowed to have multiple null termination inside a properly allocated buffer ..."}}
{"actor":{"display_login":"OrenGitHub"}}