{"action":"created","issue":{"url":"https://api.github.com/repos/boogie-org/boogie/issues/13","labels_url":"https://api.github.com/repos/boogie-org/boogie/issues/13/labels{/name}","comments_url":"https://api.github.com/repos/boogie-org/boogie/issues/13/comments","events_url":"https://api.github.com/repos/boogie-org/boogie/issues/13/events","html_url":"https://github.com/boogie-org/boogie/pull/13","id":85940905,"number":13,"title":"Don't force the exit code to 0 by default","user":{"login":"cpitclaudel","id":8181630,"avatar_url":"https://avatars.githubusercontent.com/u/8181630?v=3","gravatar_id":"","url":"https://api.github.com/users/cpitclaudel","html_url":"https://github.com/cpitclaudel","followers_url":"https://api.github.com/users/cpitclaudel/followers","following_url":"https://api.github.com/users/cpitclaudel/following{/other_user}","gists_url":"https://api.github.com/users/cpitclaudel/gists{/gist_id}","starred_url":"https://api.github.com/users/cpitclaudel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cpitclaudel/subscriptions","organizations_url":"https://api.github.com/users/cpitclaudel/orgs","repos_url":"https://api.github.com/users/cpitclaudel/repos","events_url":"https://api.github.com/users/cpitclaudel/events{/privacy}","received_events_url":"https://api.github.com/users/cpitclaudel/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":12,"created_at":"2015-06-07T20:46:50Z","updated_at":"2015-06-11T07:22:20Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/boogie-org/boogie/pulls/13","html_url":"https://github.com/boogie-org/boogie/pull/13","diff_url":"https://github.com/boogie-org/boogie/pull/13.diff","patch_url":"https://github.com/boogie-org/boogie/pull/13.patch"},"body":"Although it's convenient to force the exit code to zero for lit testing,\r\nit is more conventional (and better for interfacing with other systems)\r\nto return a non-zero error if verification fail: at the moment, the only\r\nway (IIUC) to find out whether verification succeeded (on the command\r\nline) was to parse the textual output of Boogie.\r\n\r\nThis patch adds a CountVerificationErrors option, and enables it by\r\ndefault. The patch also sets this option to zero for tests, lest lit get\r\nconfused in test cases where verification actually fails."},"comment":{"url":"https://api.github.com/repos/boogie-org/boogie/issues/comments/111023876","html_url":"https://github.com/boogie-org/boogie/pull/13#issuecomment-111023876","issue_url":"https://api.github.com/repos/boogie-org/boogie/issues/13","id":111023876,"user":{"login":"cpitclaudel","id":8181630,"avatar_url":"https://avatars.githubusercontent.com/u/8181630?v=3","gravatar_id":"","url":"https://api.github.com/users/cpitclaudel","html_url":"https://github.com/cpitclaudel","followers_url":"https://api.github.com/users/cpitclaudel/followers","following_url":"https://api.github.com/users/cpitclaudel/following{/other_user}","gists_url":"https://api.github.com/users/cpitclaudel/gists{/gist_id}","starred_url":"https://api.github.com/users/cpitclaudel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cpitclaudel/subscriptions","organizations_url":"https://api.github.com/users/cpitclaudel/orgs","repos_url":"https://api.github.com/users/cpitclaudel/repos","events_url":"https://api.github.com/users/cpitclaudel/events{/privacy}","received_events_url":"https://api.github.com/users/cpitclaudel/received_events","type":"User","site_admin":false},"created_at":"2015-06-11T07:22:20Z","updated_at":"2015-06-11T07:22:20Z","body":"As much as I agree that keeping the codebase free of windows-specific tricks is a reasonable goal, I don't think our design choices should be driven by mono's bugs, both because mono's importance seems to be bound to decrease in the not-too-far future, and because mono's crashes are still fairly rare. In addition, if one is afraid of such crashes, then it is always possible to parse the output of the tool to make sure of exactly what happened.\r\n\r\nI feel that limiting non-zero returns to parsing failures and other serious errors is a serious limitation, that will be hard to change in the future, should we want to make changes. If we assume that return codes are mostly going to be useful in scripted interactions with Boogie, then parse errors are probably going to be less frequent than verification issues. Supporting two distinct error codes for these two situations seems convenient, too, as it satisfies both those who just want to detect serious errors (check for code >= 2) and those who are interested in having an easy way to notice when verification errors occur.\r\n\r\nI like grep's approach here: 0 if the search failed, 1 if it succeeded, and 2 if there's a problem with the query itself.\r\n\r\nAs for emitting some sort of machine-readable report: sure! But I don't think it is the real issue at hand here. This would introduce a new Boogie textual API, in addition to the existing programmatic .Net dll API; this PR, in contrast, is about leveraging an existing API, namely error codes."}}