{"action":"created","issue":{"url":"https://api.github.com/repos/tracer-x/klee/issues/122","repository_url":"https://api.github.com/repos/tracer-x/klee","labels_url":"https://api.github.com/repos/tracer-x/klee/issues/122/labels{/name}","comments_url":"https://api.github.com/repos/tracer-x/klee/issues/122/comments","events_url":"https://api.github.com/repos/tracer-x/klee/issues/122/events","html_url":"https://github.com/tracer-x/klee/pull/122","id":167799624,"number":122,"title":"Avoid inserting null interpolant to the SubsumptionTableEntry by add …","user":{"login":"feliciahalim","id":11381494,"avatar_url":"https://avatars.githubusercontent.com/u/11381494?v=3","gravatar_id":"","url":"https://api.github.com/users/feliciahalim","html_url":"https://github.com/feliciahalim","followers_url":"https://api.github.com/users/feliciahalim/followers","following_url":"https://api.github.com/users/feliciahalim/following{/other_user}","gists_url":"https://api.github.com/users/feliciahalim/gists{/gist_id}","starred_url":"https://api.github.com/users/feliciahalim/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/feliciahalim/subscriptions","organizations_url":"https://api.github.com/users/feliciahalim/orgs","repos_url":"https://api.github.com/users/feliciahalim/repos","events_url":"https://api.github.com/users/feliciahalim/events{/privacy}","received_events_url":"https://api.github.com/users/feliciahalim/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":15,"created_at":"2016-07-27T08:31:58Z","updated_at":"2016-07-29T10:16:03Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/tracer-x/klee/pulls/122","html_url":"https://github.com/tracer-x/klee/pull/122","diff_url":"https://github.com/tracer-x/klee/pull/122.diff","patch_url":"https://github.com/tracer-x/klee/pull/122.patch"},"body":"…additional checking\r\n\r\nThis fix helps increase passing tests in the regression test, with current result:\r\nTesting Time: 619.16s\r\nFailing Tests (6):\r\n    KLEE :: Feature/MemoryLimit.c\r\n    KLEE :: Runtime/POSIX/DirConsistency.c\r\n    KLEE :: Runtime/POSIX/DirSeek.c\r\n    KLEE :: Runtime/POSIX/Futimesat.c\r\n    KLEE :: Runtime/POSIX/SeedAndFail.c\r\n    KLEE :: Runtime/POSIX/Write2.c\r\n\r\n  Expected Passes    : 162\r\n  Expected Failures  : 2\r\n  Unsupported Tests  : 2\r\n  Unexpected Failures: 6\r\n\r\nResult from master branch:\r\nTesting Time: 617.83s\r\nFailing Tests (9):\r\nKLEE :: Feature/KleeReportError.c\r\nKLEE :: Feature/MemoryLimit.c\r\nKLEE :: Feature/OvershiftCheck.c\r\nKLEE :: Feature/consecutive_divide_by_zero.c\r\nKLEE :: Runtime/POSIX/DirConsistency.c\r\nKLEE :: Runtime/POSIX/DirSeek.c\r\nKLEE :: Runtime/POSIX/Futimesat.c\r\nKLEE :: Runtime/POSIX/SeedAndFail.c\r\nKLEE :: Runtime/POSIX/Write2.c\r\n\r\nExpected Passes : 159\r\nExpected Failures : 2\r\nUnsupported Tests : 2\r\nUnexpected Failures: 9\r\n"},"comment":{"url":"https://api.github.com/repos/tracer-x/klee/issues/comments/236145364","html_url":"https://github.com/tracer-x/klee/pull/122#issuecomment-236145364","issue_url":"https://api.github.com/repos/tracer-x/klee/issues/122","id":236145364,"user":{"login":"domainexpert","id":696558,"avatar_url":"https://avatars.githubusercontent.com/u/696558?v=3","gravatar_id":"","url":"https://api.github.com/users/domainexpert","html_url":"https://github.com/domainexpert","followers_url":"https://api.github.com/users/domainexpert/followers","following_url":"https://api.github.com/users/domainexpert/following{/other_user}","gists_url":"https://api.github.com/users/domainexpert/gists{/gist_id}","starred_url":"https://api.github.com/users/domainexpert/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/domainexpert/subscriptions","organizations_url":"https://api.github.com/users/domainexpert/orgs","repos_url":"https://api.github.com/users/domainexpert/repos","events_url":"https://api.github.com/users/domainexpert/events{/privacy}","received_events_url":"https://api.github.com/users/domainexpert/received_events","type":"User","site_admin":false},"created_at":"2016-07-29T10:16:03Z","updated_at":"2016-07-29T10:16:03Z","body":"Thank you @feliciahalim . I think Lines 543-553 of `ITreeNode::setNodeLocation` can be replaced with just\r\n```\r\nstorable = !(instr->getParent()->getParent()->getName().substr(0, 5).equals(\"klee_\"));\r\n```\r\nThis is because a callsite is rarely at the start of a basic block, hence rarely used to identify a basic block. In your previous implementation, you used `state.pcPrev->inst` as the instruction, which is the callsite of the `klee_` function. The `klee_` function gets called and then its first instruction (`state.pc->inst`, which is actually `instr` of `ITreeNode::setNodeLocation`), and this is not a callsite of `klee_` function, so I think there is no point in checking that the instruction is a callsite of `klee_` (Line 544 onwards) in `ITreeNode::setNodeLocation`."}}
{"actor":{"display_login":"domainexpert"}}