{"action":"created","issue":{"url":"https://api.github.com/repos/smackers/smack/issues/191","repository_url":"https://api.github.com/repos/smackers/smack","labels_url":"https://api.github.com/repos/smackers/smack/issues/191/labels{/name}","comments_url":"https://api.github.com/repos/smackers/smack/issues/191/comments","events_url":"https://api.github.com/repos/smackers/smack/issues/191/events","html_url":"https://github.com/smackers/smack/issues/191","id":194186644,"number":191,"title":"Generating address axioms for removed globals","user":{"login":"zvonimir","id":1040926,"avatar_url":"https://avatars.githubusercontent.com/u/1040926?v=3","gravatar_id":"","url":"https://api.github.com/users/zvonimir","html_url":"https://github.com/zvonimir","followers_url":"https://api.github.com/users/zvonimir/followers","following_url":"https://api.github.com/users/zvonimir/following{/other_user}","gists_url":"https://api.github.com/users/zvonimir/gists{/gist_id}","starred_url":"https://api.github.com/users/zvonimir/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/zvonimir/subscriptions","organizations_url":"https://api.github.com/users/zvonimir/orgs","repos_url":"https://api.github.com/users/zvonimir/repos","events_url":"https://api.github.com/users/zvonimir/events{/privacy}","received_events_url":"https://api.github.com/users/zvonimir/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2016-12-07T22:13:24Z","updated_at":"2016-12-10T23:09:36Z","closed_at":null,"body":"I just noticed this piece of code in a Boogie file generated by SMACK:\r\n```\r\nconst .str: ref;\r\naxiom (.str == $sub.ref(0, 16));\r\nconst {:count 16} .str.1: ref;\r\naxiom (.str.1 == $sub.ref(0, 32));\r\nconst {:count 14} .str.2: ref;\r\naxiom (.str.2 == $sub.ref(0, 46));\r\nconst {:count 31} .str.3: ref;\r\naxiom (.str.3 == $sub.ref(0, 77));\r\nconst {:count 14} .str.4: ref;\r\naxiom (.str.4 == $sub.ref(0, 91));\r\n```\r\nThese globals are not mentioned anywhere else in the file. I believe this indicates that we are generating these axioms even for globals that are not used anywhere. It might be a simple optimization to clean this up."},"comment":{"url":"https://api.github.com/repos/smackers/smack/issues/comments/266246831","html_url":"https://github.com/smackers/smack/issues/191#issuecomment-266246831","issue_url":"https://api.github.com/repos/smackers/smack/issues/191","id":266246831,"user":{"login":"michael-emmi","id":1457498,"avatar_url":"https://avatars.githubusercontent.com/u/1457498?v=3","gravatar_id":"","url":"https://api.github.com/users/michael-emmi","html_url":"https://github.com/michael-emmi","followers_url":"https://api.github.com/users/michael-emmi/followers","following_url":"https://api.github.com/users/michael-emmi/following{/other_user}","gists_url":"https://api.github.com/users/michael-emmi/gists{/gist_id}","starred_url":"https://api.github.com/users/michael-emmi/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/michael-emmi/subscriptions","organizations_url":"https://api.github.com/users/michael-emmi/orgs","repos_url":"https://api.github.com/users/michael-emmi/repos","events_url":"https://api.github.com/users/michael-emmi/events{/privacy}","received_events_url":"https://api.github.com/users/michael-emmi/received_events","type":"User","site_admin":false},"created_at":"2016-12-10T23:09:36Z","updated_at":"2016-12-10T23:09:36Z","body":"At the moment it is not clear what filter can be used to rule out the `const` declarations here. We filter out their static initializers when the address is either read or not unnamed. The following regression prevents us from using that same filter to remove these declarations, since there are strings (they have unnamed addresses) which are never read but nevertheless used:\r\n\r\nhttps://github.com/smackers/smack/blob/develop/test/basic/func_ptr_vararg.c"}}
{"actor":{"display_login":"michael-emmi"}}