{"action":"created","issue":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/388","repository_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks","labels_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/388/labels{/name}","comments_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/388/comments","events_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/388/events","html_url":"https://github.com/sosy-lab/sv-benchmarks/pull/388","id":196949860,"number":388,"title":"Renaming problematic benchmarks in MemSafety","user":{"login":"versokova","id":9674306,"avatar_url":"https://avatars.githubusercontent.com/u/9674306?v=3","gravatar_id":"","url":"https://api.github.com/users/versokova","html_url":"https://github.com/versokova","followers_url":"https://api.github.com/users/versokova/followers","following_url":"https://api.github.com/users/versokova/following{/other_user}","gists_url":"https://api.github.com/users/versokova/gists{/gist_id}","starred_url":"https://api.github.com/users/versokova/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/versokova/subscriptions","organizations_url":"https://api.github.com/users/versokova/orgs","repos_url":"https://api.github.com/users/versokova/repos","events_url":"https://api.github.com/users/versokova/events{/privacy}","received_events_url":"https://api.github.com/users/versokova/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":9,"created_at":"2016-12-21T14:46:05Z","updated_at":"2016-12-22T16:39:05Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/pulls/388","html_url":"https://github.com/sosy-lab/sv-benchmarks/pull/388","diff_url":"https://github.com/sosy-lab/sv-benchmarks/pull/388.diff","patch_url":"https://github.com/sosy-lab/sv-benchmarks/pull/388.patch"},"body":"This PR is meant to address issues #337, #333, and #375. It is related to the discussion about memory leaks in the mailing list. In the discussion, if I am right, it was decided that all benchmarks that are problematic from the point of view of memory leaks should be sanitized or removed. \r\n\r\nWe see as problematic the following groups of benchmarks obtained by adding benchmarks from ReachSafety to MemSafety:\r\n\r\n**1) `*false-unreach-call_true-valid-memsafety*`**\r\nthese benchmarks are labeled as true memsafety, but they end by an abort (__VERIFIER_error()), leading to not freed memory (memory leak, but still reachable according to valgrind). We suggest to remove these benchmarks from MemSafety. Moreover, note that these benchmarks have always variants `*true-unreach-call*` or directly `*true-valid-memsafety*` that are basically equal from the point of view of memory management up to the problematic call of abort().\r\n```\r\nforester-heap/*false-unreach-call_true-valid-memsafety.{i,c}\r\nheap-manipulation/*false-unreach-call_true-valid-memsafety.{i,c}\r\nlist-ext-properties/*false-unreach-call_true-valid-memsafety.{i,c}\r\nlist-properties/*false-unreach-call_true-valid-memsafety.{i,c}\r\n```\r\nNamely:\r\n```\r\nforester-heap/dll-01_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/dll-01_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/dll-circular_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/dll-circular_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/dll-optional_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/dll-optional_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/dll-queue_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/dll-queue_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/dll-simple-white-blue_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/dll-simple-white-blue_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/dll-sorted_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/dll-sorted_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/dll-token_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/dll-token_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/sll-buckets_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/sll-buckets_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/sll-circular_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/sll-circular_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/sll-optional_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/sll-optional_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/sll-queue_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/sll-queue_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/sll-rb-sentinel_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/sll-rb-sentinel_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/sll-simple-white-blue_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/sll-simple-white-blue_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/sll-sorted_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/sll-sorted_false-unreach-call_true-valid-memsafety.i\r\nforester-heap/sll-token_false-unreach-call_true-valid-memsafety.c\r\nforester-heap/sll-token_false-unreach-call_true-valid-memsafety.i\r\nheap-manipulation/bubble_sort_linux_false-unreach-call_true-valid-memsafety.c\r\nheap-manipulation/bubble_sort_linux_false-unreach-call_true-valid-memsafety.i\r\nheap-manipulation/dll_of_dll_false-unreach-call_true-valid-memsafety.c\r\nheap-manipulation/dll_of_dll_false-unreach-call_true-valid-memsafety.i\r\nheap-manipulation/merge_sort_false-unreach-call_true-valid-memsafety.c\r\nheap-manipulation/merge_sort_false-unreach-call_true-valid-memsafety.i\r\nheap-manipulation/sll_to_dll_rev_false-unreach-call_true-valid-memsafety.c\r\nheap-manipulation/sll_to_dll_rev_false-unreach-call_true-valid-memsafety.i\r\nheap-manipulation/tree_false-unreach-call_true-valid-memsafety.c\r\nheap-manipulation/tree_false-unreach-call_true-valid-memsafety.i\r\nlist-ext-properties/simple-ext_false-unreach-call_true-valid-memsafety.c\r\nlist-ext-properties/simple-ext_false-unreach-call_true-valid-memsafety.i\r\nlist-properties/alternating_list_false-unreach-call_true-valid-memsafety.c\r\nlist-properties/alternating_list_false-unreach-call_true-valid-memsafety.i\r\nlist-properties/list_search_false-unreach-call_true-valid-memsafety.c\r\nlist-properties/list_search_false-unreach-call_true-valid-memsafety.i\r\n```\r\n**2) `*false-unreach-call_false-valid-memtrack*`**\r\nthese benchmarks are labeled as false valid memtrack, because they end by an abort (__VERIFIER_error()), leading to not freed memory (memory leak, but still reachable according to valgrind). As in Point 1, we suggest to remove these benchmarks from MemSafety. Again, note that these benchmarks have always variants `*true-unreach-call*` that are basically equal from the point of view of memory management up to the problematic call of abort().\r\n```\r\nlist-properties/*false-unreach-call_false-valid-memtrack.{i,c}\r\n```\r\nNamely:\r\n```\r\nlist-properties/list_false-unreach-call_false-valid-memtrack.c\r\nlist-properties/list_false-unreach-call_false-valid-memtrack.i\r\nlist-properties/list_flag_false-unreach-call_false-valid-memtrack.c\r\nlist-properties/list_flag_false-unreach-call_false-valid-memtrack.i\r\nlist-properties/simple_false-unreach-call_false-valid-memtrack.c\r\nlist-properties/simple_false-unreach-call_false-valid-memtrack.i\r\nlist-properties/splice_false-unreach-call_false-valid-memtrack.c\r\nlist-properties/splice_false-unreach-call_false-valid-memtrack.i\r\n```"},"comment":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/comments/268838293","html_url":"https://github.com/sosy-lab/sv-benchmarks/pull/388#issuecomment-268838293","issue_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/388","id":268838293,"user":{"login":"versokova","id":9674306,"avatar_url":"https://avatars.githubusercontent.com/u/9674306?v=3","gravatar_id":"","url":"https://api.github.com/users/versokova","html_url":"https://github.com/versokova","followers_url":"https://api.github.com/users/versokova/followers","following_url":"https://api.github.com/users/versokova/following{/other_user}","gists_url":"https://api.github.com/users/versokova/gists{/gist_id}","starred_url":"https://api.github.com/users/versokova/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/versokova/subscriptions","organizations_url":"https://api.github.com/users/versokova/orgs","repos_url":"https://api.github.com/users/versokova/repos","events_url":"https://api.github.com/users/versokova/events{/privacy}","received_events_url":"https://api.github.com/users/versokova/received_events","type":"User","site_admin":false},"created_at":"2016-12-22T16:39:05Z","updated_at":"2016-12-22T16:39:05Z","body":"@mikhailramalho, I think ddv_machzwd programs are true memsafety. Do you think something else? e.g.: program `ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i` ends by an abort after calling: main -> call_ddv -> ... -> _ddv_module_init = zf_init -> zf_readw -> outb -> __VERIFIER_assert. That means before calling malloc.\r\nOther one.: program `forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.c`, there exists trace that missing free(null) => memleak."}}
{"actor":{"display_login":"versokova"}}