{"action":"created","issue":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/283","repository_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks","labels_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/283/labels{/name}","comments_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/283/comments","events_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/283/events","html_url":"https://github.com/sosy-lab/sv-benchmarks/pull/283","id":192311075,"number":283,"title":"Remove calls to __VERIFIER_nondet_pointer() from ldv-regression/test*.c","user":{"login":"mikhailramalho","id":1328287,"avatar_url":"https://avatars.githubusercontent.com/u/1328287?v=3","gravatar_id":"","url":"https://api.github.com/users/mikhailramalho","html_url":"https://github.com/mikhailramalho","followers_url":"https://api.github.com/users/mikhailramalho/followers","following_url":"https://api.github.com/users/mikhailramalho/following{/other_user}","gists_url":"https://api.github.com/users/mikhailramalho/gists{/gist_id}","starred_url":"https://api.github.com/users/mikhailramalho/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mikhailramalho/subscriptions","organizations_url":"https://api.github.com/users/mikhailramalho/orgs","repos_url":"https://api.github.com/users/mikhailramalho/repos","events_url":"https://api.github.com/users/mikhailramalho/events{/privacy}","received_events_url":"https://api.github.com/users/mikhailramalho/received_events","type":"User","site_admin":false},"labels":[{"id":472360268,"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/labels/issue%20with%20benchmark","name":"issue with benchmark","color":"d93f0b","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2016-11-29T15:23:35Z","updated_at":"2016-11-30T12:53:28Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/pulls/283","html_url":"https://github.com/sosy-lab/sv-benchmarks/pull/283","diff_url":"https://github.com/sosy-lab/sv-benchmarks/pull/283.diff","patch_url":"https://github.com/sosy-lab/sv-benchmarks/pull/283.patch"},"body":"I removed the nondet_pointer calls and replaced them with an static variable and nondet initialization of its content.\r\n\r\nI decided to use the static variable instead of malloc'ing to avoid memory leak. The programs use goto statements to jump to the __VERIFIER_error() function call, so by using a static variable we avoid changing too much the program."},"comment":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/comments/263866270","html_url":"https://github.com/sosy-lab/sv-benchmarks/pull/283#issuecomment-263866270","issue_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/283","id":263866270,"user":{"login":"schrodibear","id":4588805,"avatar_url":"https://avatars.githubusercontent.com/u/4588805?v=3","gravatar_id":"","url":"https://api.github.com/users/schrodibear","html_url":"https://github.com/schrodibear","followers_url":"https://api.github.com/users/schrodibear/followers","following_url":"https://api.github.com/users/schrodibear/following{/other_user}","gists_url":"https://api.github.com/users/schrodibear/gists{/gist_id}","starred_url":"https://api.github.com/users/schrodibear/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/schrodibear/subscriptions","organizations_url":"https://api.github.com/users/schrodibear/orgs","repos_url":"https://api.github.com/users/schrodibear/repos","events_url":"https://api.github.com/users/schrodibear/events{/privacy}","received_events_url":"https://api.github.com/users/schrodibear/received_events","type":"User","site_admin":false},"created_at":"2016-11-30T12:53:28Z","updated_at":"2016-11-30T12:53:28Z","body":"Might it be cleaner to just model the `__VERIFIER_nondet_pointer` function by non-deterministically choosing from a number of allocated variable addresses? For instance, if a test uses `__VERIFIER_nondet_pointer` to obtain *n* pointers to variables of type *t*, it might be modeled by allocating *n* global variables of type *t* and non-deterministically choosing one of the addresses or a `NULL` reference:\r\n\r\n```c\r\nt v1, ..., vn;\r\n\r\nvoid *__DUMMY_nondet_pointer()\r\n{\r\n   t *pt;\r\n  __VERIFIER_assume(pt == &v1 || ... || pt == &vn || pt == NULL);\r\n  return pt;\r\n}\r\n```\r\nThis should cover all most important cases e.g. all possible equivalence class partitionings including one for the `NULL` pointer. For modelling invalid pointers local stack variables can be added in `__DUMMY_nondet_pointer` (the addresses become invalid after return) and aliasing between pointers to different types seems irrelevant for these particular tests."}}
{"actor":{"display_login":"schrodibear"}}