{"action":"created","issue":{"url":"https://api.github.com/repos/sosy-lab/benchexec/issues/392","repository_url":"https://api.github.com/repos/sosy-lab/benchexec","labels_url":"https://api.github.com/repos/sosy-lab/benchexec/issues/392/labels{/name}","comments_url":"https://api.github.com/repos/sosy-lab/benchexec/issues/392/comments","events_url":"https://api.github.com/repos/sosy-lab/benchexec/issues/392/events","html_url":"https://github.com/sosy-lab/benchexec/issues/392","id":394458973,"node_id":"MDU6SXNzdWUzOTQ0NTg5NzM=","number":392,"title":"Check input XML files against DTD","user":{"login":"dbeyer","id":2941008,"node_id":"MDQ6VXNlcjI5NDEwMDg=","avatar_url":"https://avatars3.githubusercontent.com/u/2941008?v=4","gravatar_id":"","url":"https://api.github.com/users/dbeyer","html_url":"https://github.com/dbeyer","followers_url":"https://api.github.com/users/dbeyer/followers","following_url":"https://api.github.com/users/dbeyer/following{/other_user}","gists_url":"https://api.github.com/users/dbeyer/gists{/gist_id}","starred_url":"https://api.github.com/users/dbeyer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dbeyer/subscriptions","organizations_url":"https://api.github.com/users/dbeyer/orgs","repos_url":"https://api.github.com/users/dbeyer/repos","events_url":"https://api.github.com/users/dbeyer/events{/privacy}","received_events_url":"https://api.github.com/users/dbeyer/received_events","type":"User","site_admin":false},"labels":[{"id":176834092,"node_id":"MDU6TGFiZWwxNzY4MzQwOTI=","url":"https://api.github.com/repos/sosy-lab/benchexec/labels/enhancement","name":"enhancement","color":"84b6eb","default":true}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2018-12-27T18:20:16Z","updated_at":"2019-01-03T10:48:50Z","closed_at":null,"author_association":"MEMBER","body":"This benchmark definition:\r\nhttps://github.com/sosy-lab/sv-comp/blob/svcomp19/benchmark-defs/cpa-seq-validate-violation-witnesses.xml\r\nclaims to follow the benchmark-definition format 1.4, but\r\nuses the tag `<requiredfiles>` which came only with version 1.9.\r\nShouldn't BenchExec check the XML files that it gets as input against the DTD it claims to follow\r\nbefore accepting them as input?\r\n"},"comment":{"url":"https://api.github.com/repos/sosy-lab/benchexec/issues/comments/451109852","html_url":"https://github.com/sosy-lab/benchexec/issues/392#issuecomment-451109852","issue_url":"https://api.github.com/repos/sosy-lab/benchexec/issues/392","id":451109852,"node_id":"MDEyOklzc3VlQ29tbWVudDQ1MTEwOTg1Mg==","user":{"login":"dbeyer","id":2941008,"node_id":"MDQ6VXNlcjI5NDEwMDg=","avatar_url":"https://avatars3.githubusercontent.com/u/2941008?v=4","gravatar_id":"","url":"https://api.github.com/users/dbeyer","html_url":"https://github.com/dbeyer","followers_url":"https://api.github.com/users/dbeyer/followers","following_url":"https://api.github.com/users/dbeyer/following{/other_user}","gists_url":"https://api.github.com/users/dbeyer/gists{/gist_id}","starred_url":"https://api.github.com/users/dbeyer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dbeyer/subscriptions","organizations_url":"https://api.github.com/users/dbeyer/orgs","repos_url":"https://api.github.com/users/dbeyer/repos","events_url":"https://api.github.com/users/dbeyer/events{/privacy}","received_events_url":"https://api.github.com/users/dbeyer/received_events","type":"User","site_admin":false},"created_at":"2019-01-03T10:48:50Z","updated_at":"2019-01-03T10:48:50Z","author_association":"MEMBER","body":"> This would mean that a file that is accepted for some users would be rejected for other users.\r\n\r\nWell, strictly speaking it is not 'accepted', but BenchExec just does not tell, instead it runs with undefined behavior.\r\n\r\n> That doesn't seem like good behavior.\r\n\r\nAccepting input that is not allowed by definition is called *undefined* behavior\r\nand the most appropriate action is to tell the user or stop in a defined manner.\r\nNot sure what 'good behavior' means in this situation.\r\nSo a warning in case the input is not checked against the contract\r\n(and BenchExec proceeds with possibly failing) seems appropriate.\r\n\r\n> We would need to package each and every version of the DTDs with BenchExec.\r\n\r\nWhy is that?  The XML refers to a publicly available DTD.\r\nFor offline usage, the same warning might appear."}}
{"actor":{"display_login":"dbeyer"}}