{"action":"created","issue":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/196","repository_url":"https://api.github.com/repos/diffblue/cbmc","labels_url":"https://api.github.com/repos/diffblue/cbmc/issues/196/labels{/name}","comments_url":"https://api.github.com/repos/diffblue/cbmc/issues/196/comments","events_url":"https://api.github.com/repos/diffblue/cbmc/issues/196/events","html_url":"https://github.com/diffblue/cbmc/issues/196","id":170384330,"number":196,"title":"Expressions in array sizes that are not statically evaluated cause problems in linking","user":{"login":"martin-cs","id":5333188,"avatar_url":"https://avatars.githubusercontent.com/u/5333188?v=3","gravatar_id":"","url":"https://api.github.com/users/martin-cs","html_url":"https://github.com/martin-cs","followers_url":"https://api.github.com/users/martin-cs/followers","following_url":"https://api.github.com/users/martin-cs/following{/other_user}","gists_url":"https://api.github.com/users/martin-cs/gists{/gist_id}","starred_url":"https://api.github.com/users/martin-cs/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/martin-cs/subscriptions","organizations_url":"https://api.github.com/users/martin-cs/orgs","repos_url":"https://api.github.com/users/martin-cs/repos","events_url":"https://api.github.com/users/martin-cs/events{/privacy}","received_events_url":"https://api.github.com/users/martin-cs/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2016-08-10T10:28:35Z","updated_at":"2016-08-11T15:43:47Z","closed_at":null,"body":"@kroening @tautschnig \r\n\r\nGiven the following program (inline because github can't attach actual code to bug reports):\r\n\r\n```\r\n#include <assert.h>\r\n\r\nint a[(int)(10./1.)];\r\nint b[(int)2] = { 10, 20 };\r\nint c[(int)(10./1.)] = { 10, 20 };\r\nint d[(int)(10/1)] = { 10, 20 };\r\n\r\nint main (void) {\r\n  if (a[0]) {\r\n    assert(b[1] + c[2] > 20);\r\n  }\r\n\r\n  return 1;\r\n}\r\n\r\nextern int g_array[];\r\nint array[(int)(10./1)];\r\n\r\nint array2[(int)(10./1)];\r\n```\r\n\r\nWe get the following error (with added pretty()) form the zero initialisation in the linker:\r\n\r\ncbmc --show-vcc examples.c\r\nCBMC version 5.4 64-bit x86_64 linux\r\nParsing examples.c\r\nConverting\r\nType-checking examples\r\nfile examples.c line 4: symbol\r\n  * type: signedbv\r\n      * width: 64\r\n      * #constant: 1\r\n      * #c_type: signed_long_int\r\n  * identifier: a$array_size0\r\nfailed to zero-initialize array of non-fixed size `a$array_size0'\r\nCONVERSION ERROR\r\n\r\nWhat seems to be happening is that somewhere in the front-end `(int)(10./1.)` is not being  constant folded, thus it is replaced with `a$array_size0` leading to problems in the linker.\r\n\r\nAs best I can work out, this is not valid C90 and may not be valid in later versions and is potentially tricky as there are all of the usual issues about evaluating floating-point numbers at compile time.  However, this is a \"pain point\" for a major customer so it would be nice if we could do something.\r\n\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/comments/239201368","html_url":"https://github.com/diffblue/cbmc/issues/196#issuecomment-239201368","issue_url":"https://api.github.com/repos/diffblue/cbmc/issues/196","id":239201368,"user":{"login":"kroening","id":1830565,"avatar_url":"https://avatars.githubusercontent.com/u/1830565?v=3","gravatar_id":"","url":"https://api.github.com/users/kroening","html_url":"https://github.com/kroening","followers_url":"https://api.github.com/users/kroening/followers","following_url":"https://api.github.com/users/kroening/following{/other_user}","gists_url":"https://api.github.com/users/kroening/gists{/gist_id}","starred_url":"https://api.github.com/users/kroening/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kroening/subscriptions","organizations_url":"https://api.github.com/users/kroening/orgs","repos_url":"https://api.github.com/users/kroening/repos","events_url":"https://api.github.com/users/kroening/events{/privacy}","received_events_url":"https://api.github.com/users/kroening/received_events","type":"User","site_admin":false},"created_at":"2016-08-11T15:43:47Z","updated_at":"2016-08-11T15:43:47Z","body":"Please check whether 8be4c7a fixes this. The rounding mode to use is obviously tricky, and right now simply hard-wired to RNE."}}
{"actor":{"display_login":"kroening"}}