Generating precise modifies clauses

[zvonimir]

It would be good for SMACK to actually generate precise modifies clauses, instead of relying on a back-end verifier to support inference of modified globals.
The way I see it, there are two ways one could go about implementing this feature:

1. Gather modified variables while building Boogie ASTs
2. Gather modified variables during a separate dedicated post-processing pass
   The advantage of the first one is that we do not have to scan the code twice, but on the other hand it would introduce these cross-cutting additions all over the place. The advantage of the second one is that the code would be nice and contained, but on the other hand it would scan the code again.
   Let's discuss this a little bit and decide how to go about implementing it.

[zvonimir]

@michael-emmi : Thoughts? Thx!

[michael-emmi]

Between the two, I think the second is preferable. Don’t forget that besides a linear-time intra-procedural code scan to determine the variables modified directly by each function, you’d still need another (possibly more asymptotically expensive?) inter-procedural pass to propagate transitively-modified variables. So the possible savings with Option 1 may be insignificant in the grand scheme of things.

I am missing a basic premise though: are there back-end verifiers besides Boogie that require modifies-clause annotation? and what’s so bad about relying on Boogie to do the annotation?

[zvonimir]

UltimateAtomizer requires for modifies clauses to be there. In addition, currently we are not really generating legal Boogie programs (based on the language spec). I think it would be good to fix that, meaning that I think that SMACK should always generate legal Boogie programs.

[lzbaer]

Just wanted to bump this, currently running into this issue. Has this been implemented? If not, could you point me in the direction of where in the code I could look to start implementing it as in option 2?

[liammachado]

I implemented this over a year ago; it's currently an open pull request:
#267

[lzbaer]

Awesome, thank you!