Remove assume false on inline 0 #934
Conversation
| @@ -400,7 +400,7 @@ void CheckRecursion(Implementation impl, Stack<Procedure /*!*/> /*!*/ callStack) | |||
| else if (options.ProcedureInlining == CoreOptions.Inlining.Assume) | |||
| { | |||
| // add assume | |||
| newCmds.Add(new AssumeCmd(callCmd.tok, Expr.False)); | |||
| newCmds.Add(new AssumeCmd(callCmd.tok, Expr.True)); | |||
There was a problem hiding this comment.
Adding an assume true seems pointless. Better to remove the command altogether then.
There was a problem hiding this comment.
I think assert false on inline == 0 also should be assert true or empty
Maybe you can do it? I don't have development environment set up |
|
I don't think we want to land this PR. See my comment on the associated issue. |
|
Maybe this pull request can actually change the options into: |
|
@petemud : Let us back up a bit. Are you actually blocked on anything here? Specifically, is there a Boogie inline option that you can already use to get your job done? |
|
@shazqadeer I'm not blocked on |
|
Glad to know you are not blocked. In principle I agree with your comments about soundness. Note though that Boogie is less a fixed verification backend and more verification backend infrastructure. It is typically used by many different tools to achieve custom combinations of "soundness" and "scalability". Mostly, we want Boogie to be predictable and not do surprising things. For the specific question of what do do with the inline attribute, I find that Boogie documentation is accurate and there are several options available to the user to achieve what they want. It is possible though:
I am happy to hear suggestions/PRs along these lines. In the meantime, I will focus my attention on the other issue of irreducible graphs because it sounds like you are actually blocked on it. |
#933