search

boogie-org / boogie

Boogie
http://research.microsoft.com/en-us/projects/boogie/
MIT License
506 stars 111 forks source link

Remove assume false on inline 0 #934

Open petemud opened 1 month ago

petemud commented 1 month ago

933

petemud commented 1 month ago

Can you add a test-case to this PR?

Maybe you can do it? I don't have development environment set up

shazqadeer commented 1 month ago

I don't think we want to land this PR. See my comment on the associated issue.

petemud commented 1 month ago

Maybe this pull request can actually change the options into: Inlining.AssertFalse, Inlining.Requires, Inlining.Spec? All three would be consistent. See #933. What do you think, @shazqadeer?

shazqadeer commented 1 month ago

@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?

petemud commented 1 month ago

@shazqadeer I'm not blocked on /inline options. I can just not use {:inline}, or use /inline:spec. It'd just be nice for a verification backend to be sound

shazqadeer commented 1 month ago

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.