Fix #3452

[wadoon]

Fix #3452, loading of no_state model methods.

This is a best guess to follow the bread crumbs (exception) during the loading process.

A new test case checks the loadability, but please revise whether the contract is sound/correct.

[mattulbrich]

I have added a test case method to the Issue3452Fixture.java test case. It contains a method illegally annotated no_state, but no proof obligation is created to check this. The method could be rejected syntactically since "heap" occurs in the method.

Moreover, no_state methods should not get heap as an argument. ... I'd like to keep this branch open to implement this.
OK, @wadoon ?

[wadoon]

OK, @wadoon ?

Fine. I have assigned the issue to you.

[mattulbrich]

It seems the PR template is deactivated, at least for this PR.

Well. It repairs expected behaviour and there is a new test case to cover for added feature.

The new feature is: If a method is annotated no_state, its definition really must not refer to the heap
(This means o.f-o.f is not no_state).