Refactor call desugaring and passive command creation

[atomb]

As @keyboardDrummer points out in his review comments on #741, ConditionGeneration.TurnIntoPassiveCmd and CallCmd.ComputeDesugaring are very complex and use regions to further break down the code. They might be more understandable and maintainable if they could be broken into multiple methods, each with clear names and purposes. However, given how central that code is to the correctness of Boogie, and how complex it is, we should probably do so carefully and with the involvement of several reviewers deeply familiar with the code.

In particular, I think @shazqadeer, @RustanLeino, @zvonimir/@rakamaric, and perhaps others should have a chance to chime in before we undertake this, and be involved in the review process.

[shazqadeer]

Indeed, both methods are very long and deserve to be split up.

I noticed that TurnIntoPassiveCmd analyzes many attributes on PredicateCmd's such as "minimize", "maximize", "verified_under", etc. I examined the output of "boogie /attrHelp" and didn't find any documentation for these attributes. Does anybody know what they are supposed to do? Are they Dafny specific?

[atomb]

I don't believe Dafny uses any of those attributes, and I'm not sure what they do, either.

[shazqadeer]

Then we should delete them.

@RustanLeino , @gauravpartha , @alexanderjsummers: ok with deleting the attributes mentioned above?

[gauravpartha]

Then we should delete them.

@RustanLeino , @gauravpartha , @alexanderjsummers: ok with deleting the attributes mentioned above?

Yes, Viper doesn't use those attributes either.

[alexanderjsummers]

Sounds fine to me then! Thanks.