{"action":"created","issue":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/230","repository_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks","labels_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/230/labels{/name}","comments_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/230/comments","events_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/230/events","html_url":"https://github.com/sosy-lab/sv-benchmarks/issues/230","id":190818636,"number":230,"title":"Benchmarks depending on undefined functions in DeviceDriversLinux64","user":{"login":"mchalupa","id":2385056,"avatar_url":"https://avatars.githubusercontent.com/u/2385056?v=3","gravatar_id":"","url":"https://api.github.com/users/mchalupa","html_url":"https://github.com/mchalupa","followers_url":"https://api.github.com/users/mchalupa/followers","following_url":"https://api.github.com/users/mchalupa/following{/other_user}","gists_url":"https://api.github.com/users/mchalupa/gists{/gist_id}","starred_url":"https://api.github.com/users/mchalupa/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mchalupa/subscriptions","organizations_url":"https://api.github.com/users/mchalupa/orgs","repos_url":"https://api.github.com/users/mchalupa/repos","events_url":"https://api.github.com/users/mchalupa/events{/privacy}","received_events_url":"https://api.github.com/users/mchalupa/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":14,"created_at":"2016-11-21T19:53:32Z","updated_at":"2016-12-20T17:26:18Z","closed_at":null,"body":"Hi,\r\n\r\nin those benchmarks there are calls to functions (or dereference of an external variable in one case) that are not defined and then a decision is made based on the return value (I linked exact lines):\r\n\r\nhttps://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--net--usb--cdc_subset.ko-entry_point_true-unreach-call.cil.out.c#L6096\r\n\r\nhttps://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-commit-tester/m0_true-unreach-call_drivers-usb-gadget-g_printer-ko--106_1a--2b9ec6c.c#L3827\r\n\r\nhttps://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_ltlk.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c#L588\r\n\r\nCould somebody from ldv team check it? I have more 'candidates' on my list that I haven't checked yet, so maybe I'll add some more later.\r\n\r\nThanks,\r\nMarek"},"comment":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/comments/268304093","html_url":"https://github.com/sosy-lab/sv-benchmarks/issues/230#issuecomment-268304093","issue_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/230","id":268304093,"user":{"login":"sfsiegel","id":5314038,"avatar_url":"https://avatars.githubusercontent.com/u/5314038?v=3","gravatar_id":"","url":"https://api.github.com/users/sfsiegel","html_url":"https://github.com/sfsiegel","followers_url":"https://api.github.com/users/sfsiegel/followers","following_url":"https://api.github.com/users/sfsiegel/following{/other_user}","gists_url":"https://api.github.com/users/sfsiegel/gists{/gist_id}","starred_url":"https://api.github.com/users/sfsiegel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/sfsiegel/subscriptions","organizations_url":"https://api.github.com/users/sfsiegel/orgs","repos_url":"https://api.github.com/users/sfsiegel/repos","events_url":"https://api.github.com/users/sfsiegel/events{/privacy}","received_events_url":"https://api.github.com/users/sfsiegel/received_events","type":"User","site_admin":false},"created_at":"2016-12-20T17:26:18Z","updated_at":"2016-12-20T17:26:18Z","body":"Assuming undefined functions return a nondeterministic value of the right type and don't modify anything is one reasonable interpretation, but not the only one and not my preferred solution.    In my view it is too unsafe --- what if the unknown function really does modify some global variable for example --- then your verifier might tell you your program is safe when it isn't.   You could argue that an equally \"graceful\" approach would be to assume that the function modifies everything if no further information is provided.   I would prefer that the user make the assumption explicit, whatever it is.  (Or there could be a command line option to state a blanket assumption --- but it wouldn't be the default.)\r\n\r\nSome tools would use a contract on the function declaration to express this assumption (\\assigns nothing;); others might require a simple stub, which is what I thought Dirk said should be done for SV-COMP.  Maybe there should be an exception for some category or another if that is not practical. \r\n\r\nIn any case, the policy should just be clearly stated somewhere so we don't have to argue about each benchmark on a case by case basis.\r\n"}}
{"actor":{"display_login":"sfsiegel"}}